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

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

theorem HCPolySupport.exists_overlapCube_meanZero_poincare_constant {d : ℕ} {q : ℝ} (hq : 1 < q) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (S : TriadicCube d) (u : W1pMeanZeroFunction (openOverlapCubeSet S) (ENNReal.ofReal q)), u.valueLpSeminorm ≤ C * overlapCubeScaleFactor S * u.gradientCoordLpSeminormSum

One finite-p Poincare constant, selected on the unit centered cube, controls every open overlap cube after its explicit scale factor.

theorem HCPolySupport.exists_overlapCube_meanZero_poincare_constant_finite {d : ℕ} (q : FiniteLpExponent) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (S : TriadicCube d) (u : W1pMeanZeroFunction (openOverlapCubeSet S) q.exponent), u.valueLpSeminorm ≤ C * overlapCubeScaleFactor S * u.gradientCoordLpSeminormSum

The overlap-cube Poincare estimate in the finite-exponent carrier used by the finite-p Sobolev and Calderon--Zygmund layers.

The following reverse-translation package is deliberately private: it is the one local transport needed to retain the source-facing subaverage form of Poincare on overlap cubes.

noncomputable def HCPolySupport.castW1pDomain {d : ℕ} {U V : Set (Vec d)} {p : ENNReal} (hUV : U = V) (u : W1pFunction U p) : W1pFunction V p

Transport a W^{1,p} function along equality of its domains, preserving its value and gradient.

Equations

• HCPolySupport.castW1pDomain hUV u = hUV ▸ u

noncomputable def HCPolySupport.untranslateForOverlapPoincare {d : ℕ} {U : Set (Vec d)} {p : ENNReal} (z : Vec d) (u : W1pFunction (translateSet z U) p) : W1pFunction U p

Return a function on translateSet z U to U by translation through -z; its value and gradient at x are those of the original function at x + z.

Equations

• HCPolySupport.untranslateForOverlapPoincare z u = HCPolySupport.castW1pDomain ⋯ (u.translate (-z))

theorem HCPolySupport.exists_overlapCube_subAverage_poincare_constant_finite {d : ℕ} [NeZero d] (q : FiniteLpExponent) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (S : TriadicCube d) (u : W1pFunction (openOverlapCubeSet S) q.exponent), u.subAverageLpSeminorm ≤ C * overlapCubeScaleFactor S * u.gradientCoordLpSeminormSum

One finite-p Poincare constant controls the subaverage seminorm on every open overlap cube. This is the scalar form consumed by normalized vector interfaces.