Coarse-graining support: Support.Sobolev.Foundations.PoincareMeanZero

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

Mean-zero L² Poincare on bounded open convex domains

This file packages the bounded-open-convex Poincare development on the mean-zero H¹ layer.

The proof combines the smooth convex-domain Poincare theorem, convex smoothing of rough H¹ witnesses, and the closed-graph continuity lemmas for subtracting averages. The public output is the bundled coercive estimate consumed by the Hodge layer.

theorem HCPolySupport.H1Function.fderivL2Norm_le_gradientCoordL2NormSum_ofContDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) : have u := ofContDiffOnIsOpenBoundedConvexDomain hU ⋯; (MeasureTheory.eLpNorm (fderiv ℝ f) 2 (volumeMeasureOn U)).toReal ≤ u.gradientCoordL2NormSum

noncomputable def HCPolySupport.H1Function.smoothPoincareSqConst {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : ℝ

The explicit squared smooth Poincare constant formed from the domain volume, a chosen coordinate bound, the dimension, and the unit-ball volume.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.H1Function.smoothPoincareConst {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : ℝ

The nonnegative square root of the explicit squared smooth Poincare constant.

Equations

• HCPolySupport.H1Function.smoothPoincareConst hU = √(HCPolySupport.H1Function.smoothPoincareSqConst hU)

theorem HCPolySupport.H1Function.smoothPoincareConst_nonneg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : 0 ≤ smoothPoincareConst hU

noncomputable def HCPolySupport.H1Function.h1CoerciveEstimateChosenBound {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : ℝ

Public formula bounding the chosen coercive constant in h1CoerciveEstimate_of_isOpenBoundedConvexDomain.

The formula is intentionally the square root of the smooth squared Poincare constant times the coordinate-to-vector comparison factor. It exposes the geometric scale of the chosen proof without exposing the private smooth proof names.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.H1Function.h1CoerciveEstimateChosenBound_nonneg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : 0 ≤ h1CoerciveEstimateChosenBound hU

theorem HCPolySupport.H1Function.unitConvexApproxScale_pos (n : ℕ) : 0 < unitConvexApproxScale n

noncomputable def HCPolySupport.H1Function.convexApproxSmoothH1 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (x0 : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : H1Function U

The H¹ smoothing of u obtained by convolving its zero extension at scale r / (n + 1) and evaluating at the affine contraction toward x0.

Equations

• HCPolySupport.H1Function.convexApproxSmoothH1 hU u x0 hr n = HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain hU ⋯

theorem HCPolySupport.H1Function.convexApproxSmoothH1_toFun {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (x0 : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : (convexApproxSmoothH1 hU u x0 hr n).toFun = convexApproxSmoothRepresentative U unitConvexApproxKernel u.toFun x0 r (unitConvexApproxScale n)

theorem HCPolySupport.H1Function.convexApproxSmoothH1_grad {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (x0 : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : (convexApproxSmoothH1 hU u x0 hr n).grad = fun (x : Vec d) (i : Fin d) => (fderiv ℝ (convexApproxSmoothRepresentative U unitConvexApproxKernel u.toFun x0 r (unitConvexApproxScale n)) x) (basisVec i)

theorem HCPolySupport.H1Function.tendsto_convexApproxSmoothH1_toScalarL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) : Filter.Tendsto (fun (n : ℕ) => (convexApproxSmoothH1 hU u x0 hr n).toScalarL2) Filter.atTop (nhds u.toScalarL2)

theorem HCPolySupport.H1Function.tendsto_convexApproxSmoothH1_gradCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => (convexApproxSmoothH1 hU u x0 hr n).gradCoordToScalarL2 i) Filter.atTop (nhds (u.gradCoordToScalarL2 i))

theorem HCPolySupport.H1Function.h1MeanZero_valueL2Norm_le_smoothPoincareConst_mul_gradientL2Norm {d : ℕ} {U : Set (Vec d)} [NeZero d] [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) (hvol : 0 < (MeasureTheory.volume U).toReal) (u : H1MeanZeroFunction U) : u.valueL2Norm ≤ smoothPoincareConst hU * ↑d * u.gradientL2Norm

Positive-dimensional, positive-volume bounded open convex domains satisfy the mean-zero L² Poincare estimate.

theorem HCPolySupport.H1Function.h1MeanZero_valueL2Norm_eq_zero_of_volume_toReal_eq_zero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hvol : (MeasureTheory.volume U).toReal = 0) (u : H1MeanZeroFunction U) : u.valueL2Norm = 0

theorem HCPolySupport.H1Function.h1MeanZero_valueL2Norm_eq_zero_of_dim_zero {U : Set (Vec 0)} (hvol : 0 < (MeasureTheory.volume U).toReal) (u : H1MeanZeroFunction U) : u.valueL2Norm = 0

noncomputable def HCPolySupport.h1CoerciveEstimateOfOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) : H1CoerciveEstimate U

Bounded open convex domains satisfy the mean-zero L² Poincare inequality, packaged as an H1CoerciveEstimate.

Equivalently, there exists C ≥ 0 such that every u : H1MeanZeroFunction U satisfies u.valueL2Norm ≤ C * u.gradientL2Norm.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.h1CoerciveEstimate_of_isOpenBoundedConvexDomain_constant_le_chosenBound {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) : (h1CoerciveEstimateOfOpenBoundedConvexDomain hU).constantValue ≤ H1Function.h1CoerciveEstimateChosenBound hU

theorem HCPolySupport.exists_poincare_constant_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : H1MeanZeroFunction U), u.valueL2Norm ≤ C * u.gradientL2Norm

Unbundled existential form of h1CoerciveEstimate_of_isOpenBoundedConvexDomain.