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

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

Zero-trace Poincare on bounded open convex domains

This file is the public theorem wrapper for the bounded-open-convex zero-trace Poincare development.

We freeze the general finite-p theorem surface on W^{1,p}_0 here so downstream PDE files can target the correct statement while the Sobolev proof is completed separately. The existing L² estimate from CoerciveH10 is then repackaged in the same style as the mean-zero wrapper file.

theorem HCPolySupport.W10pFunction.exists_poincare_constant_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) (hU : IsOpenBoundedConvexDomain U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : W10pFunction U p), (MeasureTheory.eLpNorm u.toFun p (volumeMeasureOn U)).toReal ≤ C * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) p (volumeMeasureOn U)).toReal

Bounded open convex domains satisfy the zero-trace W^{1,p} Poincare inequality.

Equivalently, there exists C ≥ 0 such that every u : W10pFunction U p satisfies an L^p bound of the function by the sum of the L^p norms of its weak gradient coordinates. Lean keeps the exponent on the W^{1,p} layer as an ENNReal.

noncomputable def HCPolySupport.H10Function.toW10pFunction {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : W10pFunction U 2

The same zero-trace H¹ function and supported smooth approximation viewed in W^{1,2}_0.

Equations

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

theorem HCPolySupport.H10Function.exists_poincare_constant_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : H10Function U), ‖u.toScalarL2‖ ≤ C * u.gradientCoordL2NormSum

Existential constant form of the bounded-open-convex zero-trace L² Poincare inequality. This is the H¹₀ wrapper parallel to the mean-zero public theorem file.

theorem HCPolySupport.H10Function.toScalarL2_eq_zero_of_gradToVectorL2_eq_zero_of_exists_poincare_constant {d : ℕ} {U : Set (Vec d)} (hP : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : H10Function U), ‖u.toScalarL2‖ ≤ C * u.gradientCoordL2NormSum) (u : H10Function U) (hgrad : u.gradToVectorL2 = 0) : u.toScalarL2 = 0

Any zero-trace coercive estimate implies that an H¹₀ function with zero gradient L² class has zero value L² class. This isolates the only use of the scalar Poincare inequality needed in the current RHS Dirichlet theory.