Coarse-graining support: Support.Sobolev.NormalizedLp

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Normalized L^p quantities on bounded measurable domains

The normalized measure of a BoundedMeasurableDomain is the mathematical meaning of the manuscript notation fint_U. Extended norms are kept in ℝ≥0∞; a finite real value is exposed only together with a MemLp witness. The ambient Vec d norm remains untouched: the Euclidean vector lane below uses the explicit function euclideanNorm.

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedLpENorm {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [ENorm E] [TopologicalSpace E] (p : ENNReal) (f : Vec d → E) : ENNReal

The extended normalized L^p seminorm, with respect to normalized volume.

Equations

• U.normalizedLpENorm p f = MeasureTheory.eLpNorm f p U.normalizedVolume

theorem HCPolySupport.BoundedMeasurableDomain.memLp_normalizedVolume_iff {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) : MeasureTheory.MemLp f p U.normalizedVolume ↔ MeasureTheory.MemLp f p U.restrictedVolume

Membership in L^p is unchanged by the strictly positive finite volume normalization.

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedLpFiniteENorm {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.MemLp f p U.normalizedVolume) : { q : ENNReal // q ≠ ⊤ }

The normalized extended norm, packaged with the finiteness supplied by MemLp.

Equations

• U.normalizedLpFiniteENorm p f hf = ⟨U.normalizedLpENorm p f, ⋯⟩

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedLpNorm {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.MemLp f p U.normalizedVolume) : ℝ

The finite real normalized L^p value certified by a MemLp witness.

Equations

• U.normalizedLpNorm p f hf = (↑(U.normalizedLpFiniteENorm p f hf)).toReal

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpENorm_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [ENorm E] [TopologicalSpace E] (p : ENNReal) {f g : Vec d → E} (hfg : f =ᵐ[U.normalizedVolume] g) : U.normalizedLpENorm p f = U.normalizedLpENorm p g

The extended normalized L^p value depends only on the normalized-volume almost-everywhere representative.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpNorm_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) {f g : Vec d → E} (hf : MeasureTheory.MemLp f p U.normalizedVolume) (hg : MeasureTheory.MemLp g p U.normalizedVolume) (hfg : f =ᵐ[U.normalizedVolume] g) : U.normalizedLpNorm p f hf = U.normalizedLpNorm p g hg

A proof-carrying finite normalized L^p value depends only on the normalized-volume almost-everywhere representative.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpFiniteENorm_value {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.MemLp f p U.normalizedVolume) : ↑(U.normalizedLpFiniteENorm p f hf) = U.normalizedLpENorm p f

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpFiniteENorm_ne_top {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.MemLp f p U.normalizedVolume) : ↑(U.normalizedLpFiniteENorm p f hf) ≠ ⊤

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedLpMoment {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] (p : ENNReal) (f : Vec d → E) : ℝ

The p-moment with respect to normalized volume. Its use in the finite- p characterization below is justified by the accompanying MemLp witness.

Equations

• U.normalizedLpMoment p f = ∫ (x : HCPolySupport.Vec d), ‖f x‖ ^ p.toReal ∂U.normalizedVolume

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpMoment_congr_ae {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] (p : ENNReal) {f g : Vec d → E} (hfg : f =ᵐ[U.normalizedVolume] g) : U.normalizedLpMoment p f = U.normalizedLpMoment p g

The normalized p-moment depends only on the normalized-volume almost-everywhere representative.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpNorm_eq_normalizedLpMoment_rpow {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [NormedAddCommGroup E] (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (f : Vec d → E) (hf : MeasureTheory.MemLp f p U.normalizedVolume) : U.normalizedLpNorm p f hf = U.normalizedLpMoment p f ^ p.toReal⁻¹

For finite p ≥ 1, the normalized real norm is exactly the manuscript quantity (fint_U ‖f‖^p)^(1/p).

theorem HCPolySupport.BoundedMeasurableDomain.normalizedLpENorm_top_eq_essSup {d : ℕ} (U : BoundedMeasurableDomain d) {E : Type u_1} [ENorm E] [TopologicalSpace E] (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f U.normalizedVolume) : U.normalizedLpENorm ⊤ f = essSup (fun (x : Vec d) => ‖f x‖ₑ) U.normalizedVolume

At p = ∞, the normalized extended norm is Mathlib's essential supremum.

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedEuclideanLpENorm {d n : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (f : Vec d → Vec n) : ENNReal

The explicit Euclidean extended L^p value of a vector-valued function. This does not change the global norm instance on Vec d.

Equations

• U.normalizedEuclideanLpENorm p f = U.normalizedLpENorm p fun (x : HCPolySupport.Vec d) => HCPolySupport.euclideanNorm (f x)

noncomputable def HCPolySupport.BoundedMeasurableDomain.normalizedEuclideanLpNorm {d n : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (f : Vec d → Vec n) (hf : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (f x)) p U.normalizedVolume) : ℝ

The finite Euclidean normalized L^p value certified by MemLp.

Equations

• U.normalizedEuclideanLpNorm p f hf = U.normalizedLpNorm p (fun (x : HCPolySupport.Vec d) => HCPolySupport.euclideanNorm (f x)) hf

theorem HCPolySupport.BoundedMeasurableDomain.normalizedEuclideanLpENorm_congr_ae {d n : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) {f g : Vec d → Vec n} (hfg : f =ᵐ[U.normalizedVolume] g) : U.normalizedEuclideanLpENorm p f = U.normalizedEuclideanLpENorm p g

The extended Euclidean normalized L^p value depends only on the normalized-volume almost-everywhere representative.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedEuclideanLpNorm_congr_ae {d n : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) {f g : Vec d → Vec n} (hf : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (f x)) p U.normalizedVolume) (hg : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (g x)) p U.normalizedVolume) (hfg : f =ᵐ[U.normalizedVolume] g) : U.normalizedEuclideanLpNorm p f hf = U.normalizedEuclideanLpNorm p g hg

A proof-carrying finite Euclidean normalized L^p value depends only on the normalized-volume almost-everywhere representative.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedEuclideanLpNorm_eq_integral_rpow {d n : ℕ} (U : BoundedMeasurableDomain d) (p : ENNReal) (hp_one : 1 ≤ p) (hp_top : p ≠ ⊤) (f : Vec d → Vec n) (hf : MeasureTheory.MemLp (fun (x : Vec d) => euclideanNorm (f x)) p U.normalizedVolume) : U.normalizedEuclideanLpNorm p f hf = (∫ (x : Vec d), euclideanNorm (f x) ^ p.toReal ∂U.normalizedVolume) ^ p.toReal⁻¹

For finite p ≥ 1, the Euclidean vector lane has the exact normalized moment formula from the manuscript.

theorem HCPolySupport.BoundedMeasurableDomain.normalizedEuclideanLpENorm_top_eq_essSup {d n : ℕ} (U : BoundedMeasurableDomain d) (f : Vec d → Vec n) (hf : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => euclideanNorm (f x)) U.normalizedVolume) : U.normalizedEuclideanLpENorm ⊤ f = essSup (fun (x : Vec d) => ENNReal.ofReal (euclideanNorm (f x))) U.normalizedVolume

At p = ∞, the Euclidean vector lane is the essential supremum of the explicit Euclidean magnitude.