Coarse-graining support: Support.Sobolev.MatchedPair.ScaledPoincare

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

Scaled Poincaré inequalities on axis cubes

Two scaled Poincaré inequalities on axis cubes U = axisCube z L:

• scaled_meanZero_poincare — the mean-zero Poincaré inequality with the explicit C_d · L scaling;
• scaled_dirichlet_poincare — the zero-trace (Dirichlet) Poincaré inequality for MemH10 functions, with the explicit C_d · L scaling.

Both are obtained from the corresponding existential Poincaré constant on the fixed unit corner cube axisCube 0 1 (whose constant is therefore an absolute C_d), transported to axisCube z L along the affine dilation-plus-translation axisCube z L = translateSet z (L • axisCube 0 1). The H¹ weak-gradient transport and constant bookkeeping are supplied by the reusable bridges H1CoerciveEstimate.dilate / .translate, H1Function.unscale, H10Function.unscale, H10Function.untranslate.

Geometry of axis cubes under dilation and translation

theorem HCPolySupport.smul_axisCube_zero_one {d : ℕ} (L : ℝ) (hL : 0 < L) : L • axisCube 0 1 = axisCube 0 L

The corner unit cube dilates to the corner cube of side L.

theorem HCPolySupport.translateSet_axisCube_zero {d : ℕ} (z : Vec d) (L : ℝ) : translateSet z (axisCube 0 L) = axisCube z L

Translating the corner cube of side L by z gives axisCube z L.

theorem HCPolySupport.axisCube_eq_translateSet_smul {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) : axisCube z L = translateSet z (L • axisCube 0 1)

The affine identification axisCube z L = translateSet z (L • axisCube 0 1).

Finite-measure instances

instance HCPolySupport.isFiniteMeasure_volumeMeasureOn_axisCube {d : ℕ} (z : Vec d) (L : ℝ) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (axisCube z L))

The mean-zero coercive estimate, transported to axis cubes

noncomputable def HCPolySupport.unitMeanZeroPoincareConst (d : ℕ) : ℝ

The absolute mean-zero Poincaré constant of the fixed unit corner cube axisCube 0 1. It depends only on the dimension d.

Equations

• HCPolySupport.unitMeanZeroPoincareConst d = (HCPolySupport.h1CoerciveEstimateOfOpenBoundedConvexDomain ⋯).constantValue

theorem HCPolySupport.unitMeanZeroPoincareConst_nonneg (d : ℕ) : 0 ≤ unitMeanZeroPoincareConst d

noncomputable def HCPolySupport.axisCubeMeanZeroCoerciveEstimate {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) : H1CoerciveEstimate (axisCube z L)

The mean-zero coercive H¹ estimate on axisCube z L, obtained by dilating the unit corner-cube estimate by L and translating by z. Its constant is the scale-correct L · C_d.

Equations

• HCPolySupport.axisCubeMeanZeroCoerciveEstimate z hL = ⋯ ▸ (HCPolySupport.H1CoerciveEstimate.dilate hL (HCPolySupport.h1CoerciveEstimateOfOpenBoundedConvexDomain ⋯)).translate z

theorem HCPolySupport.axisCubeMeanZeroCoerciveEstimate_constant {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) : (axisCubeMeanZeroCoerciveEstimate z hL).constantValue = L * unitMeanZeroPoincareConst d

Bridges between the library's L² realizations and eLpNorm

theorem HCPolySupport.norm_toScalarL2_eq {d : ℕ} {U : Set (Vec d)} (h : H1Function U) : ‖h.toScalarL2‖ = (MeasureTheory.eLpNorm h.toFun 2 (volumeMeasureOn U)).toReal

The L² realization norm of an H¹ value is the toReal of its eLpNorm.

theorem HCPolySupport.norm_gradCoordToScalarL2_eq {d : ℕ} {U : Set (Vec d)} (h : H1Function U) (i : Fin d) : ‖h.gradCoordToScalarL2 i‖ = (MeasureTheory.eLpNorm (fun (x : Vec d) => h.grad x i) 2 (volumeMeasureOn U)).toReal

The L² realization norm of a gradient coordinate is the toReal of its eLpNorm.

F0(i): scaled mean-zero Poincaré

theorem HCPolySupport.scaled_meanZero_poincare {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) (u : H1Function (axisCube z L)) : (MeasureTheory.eLpNorm u.subAverage.toFun 2 (volumeMeasureOn (axisCube z L))).toReal ≤ unitMeanZeroPoincareConst d * L * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) 2 (volumeMeasureOn (axisCube z L))).toReal

Scaled mean-zero Poincaré on axis cubes.

For u ∈ H¹(axisCube z L), the L² norm of the mean-subtracted u − ⨍u is controlled by C_d · L times the coordinate-sum L² norm of ∇u.

Translation- and cast-invariance of the L² realizations

theorem HCPolySupport.norm_toScalarL2_untranslate_eq {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1Function (translateSet z U)) : ‖(H1Function.untranslate z u).toScalarL2‖ = ‖u.toScalarL2‖

Translation preserves the L² value norm of an H¹ witness.

theorem HCPolySupport.gradientCoordL2NormSum_untranslate_eq {d : ℕ} {U : Set (Vec d)} (z : Vec d) (u : H1Function (translateSet z U)) : (H1Function.untranslate z u).gradientCoordL2NormSum = u.gradientCoordL2NormSum

Translation preserves the coordinate-sum gradient L² norm.

theorem HCPolySupport.norm_toScalarL2_h10_congr {d : ℕ} {U V : Set (Vec d)} (h : U = V) (w : H10Function U) : ‖(h ▸ w).toScalarL2‖ = ‖w.toScalarL2‖

Rewriting the domain along a set equality preserves the L² value norm.

theorem HCPolySupport.gradientCoordL2NormSum_h10_congr {d : ℕ} {U V : Set (Vec d)} (h : U = V) (w : H10Function U) : (h ▸ w).gradientCoordL2NormSum = w.gradientCoordL2NormSum

Rewriting the domain along a set equality preserves the coordinate-sum gradient norm.

F0(ii): scaled Dirichlet (zero-trace) Poincaré

noncomputable def HCPolySupport.unitDirichletPoincareConst (d : ℕ) [NeZero d] : ℝ

The absolute zero-trace Poincaré constant of the fixed unit corner cube.

Equations

• HCPolySupport.unitDirichletPoincareConst d = ⋯.choose

theorem HCPolySupport.unitDirichletPoincareConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ unitDirichletPoincareConst d

theorem HCPolySupport.unitDirichletPoincareConst_bound {d : ℕ} [NeZero d] (w : H10Function (axisCube 0 1)) : ‖w.toScalarL2‖ ≤ unitDirichletPoincareConst d * w.gradientCoordL2NormSum

theorem HCPolySupport.scaled_dirichlet_poincare_norm {d : ℕ} [NeZero d] (z : Vec d) {L : ℝ} (hL : 0 < L) (w : H10Function (axisCube z L)) : ‖w.toScalarL2‖ ≤ unitDirichletPoincareConst d * L * w.gradientCoordL2NormSum

Scaled Dirichlet Poincaré on axis cubes (norm form).

For w ∈ H¹₀(axisCube z L), the L² realization norm of w is controlled by C_d · L times the coordinate-sum gradient norm of ∇w.

theorem HCPolySupport.gradientCoordL2NormSum_eq_sum_eLpNorm {d : ℕ} {U : Set (Vec d)} (h : H1Function U) : h.gradientCoordL2NormSum = ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => h.grad x i) 2 (volumeMeasureOn U)).toReal

The coordinate-sum gradient norm as a sum of eLpNorm toReals.

theorem HCPolySupport.scaled_dirichlet_poincare {d : ℕ} [NeZero d] (z : Vec d) {L : ℝ} (hL : 0 < L) (w : H10Function (axisCube z L)) : (MeasureTheory.eLpNorm w.toFun 2 (volumeMeasureOn (axisCube z L))).toReal ≤ unitDirichletPoincareConst d * L * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => w.grad x i) 2 (volumeMeasureOn (axisCube z L))).toReal

Scaled Dirichlet Poincaré on axis cubes (eLpNorm form).