Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.Seminorms

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

Mean-zero W^{1,p} Poincare scaffolding

This file is the public landing zone for the finite-p extension of the bounded-open-convex mean-zero Poincare theorem.

The completed p = 2 endpoint in PoincareMeanZero.lean is bundled as an H1CoerciveEstimate, because it feeds the Hilbert/Hodge layer. The finite-p surface here stays in terms of eLpNorm seminorms attached to the witness-based W1pFunction API.

theorem HCPolySupport.toReal_eLpNorm_ofReal_eq_integral_rpow_norm_rpow_inv {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p : ℝ} (hp : 0 < p) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) : (MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ).toReal = (∫ (x : α), ‖f x‖ ^ p ∂μ) ^ (1 / p)

For a finite positive real exponent, the real value of the eLpNorm is the usual integral power expression.

theorem HCPolySupport.toReal_eLpNorm_ofReal_rpow_eq_integral_rpow_norm {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p : ℝ} (hp : 0 < p) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) : (MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ).toReal ^ p = ∫ (x : α), ‖f x‖ ^ p ∂μ

Powered form of toReal_eLpNorm_ofReal_eq_integral_rpow_norm_rpow_inv.

theorem HCPolySupport.W1pFunction.memLp_fderiv_of_contDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MeasureTheory.MemLp (fderiv ℝ f) p (volumeMeasureOn U)

noncomputable def HCPolySupport.W1pFunction.valueLpSeminorm {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : ℝ

The scalar L^p(U) seminorm of a W^{1,p} witness, as a real number.

Equations

• u.valueLpSeminorm = (MeasureTheory.eLpNorm u.toFun p (HCPolySupport.volumeMeasureOn U)).toReal

noncomputable def HCPolySupport.W1pFunction.subAverageLpSeminorm {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : ℝ

The scalar L^p(U) seminorm after subtracting the integral average.

Equations

• u.subAverageLpSeminorm = (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.toFun x - HCPolySupport.integralAverage U u.toFun) p (HCPolySupport.volumeMeasureOn U)).toReal

noncomputable def HCPolySupport.W1pFunction.gradCoordLpSeminorm {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (i : Fin d) : ℝ

The ith coordinate L^p(U) seminorm of the weak gradient.

Equations

• u.gradCoordLpSeminorm i = (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.grad x i) p (HCPolySupport.volumeMeasureOn U)).toReal

noncomputable def HCPolySupport.W1pFunction.gradientCoordLpSeminormSum {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : ℝ

Coordinate-sum gradient seminorm used by the finite-p Poincare API.

This avoids introducing a vector-valued Lp wrapper for every exponent at this stage, while matching the data already stored in W1pFunction.gradMemLp.

Equations

• u.gradientCoordLpSeminormSum = ∑ i : Fin d, u.gradCoordLpSeminorm i

theorem HCPolySupport.W1pFunction.valueLpSeminorm_nonneg {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : 0 ≤ u.valueLpSeminorm

theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_nonneg {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : 0 ≤ u.subAverageLpSeminorm

theorem HCPolySupport.W1pFunction.gradCoordLpSeminorm_nonneg {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) (i : Fin d) : 0 ≤ u.gradCoordLpSeminorm i

theorem HCPolySupport.W1pFunction.gradientCoordLpSeminormSum_nonneg {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (u : W1pFunction U p) : 0 ≤ u.gradientCoordLpSeminormSum

theorem HCPolySupport.W1pFunction.fderivLpNorm_le_gradientCoordLpSeminormSum_ofContDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (hU : IsOpenBoundedConvexDomain U) (hp1 : 1 ≤ p) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) : have u := ofContDiffOnIsOpenBoundedConvexDomain hU ⋯; (MeasureTheory.eLpNorm (fderiv ℝ f) p (volumeMeasureOn U)).toReal ≤ u.gradientCoordLpSeminormSum