Core

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Matched-pair Poincaré on axis cubes

Assembles the zero-set lower bound and the matched-pair Poincaré inequality (the high-moment paper's e.doubled.poincare, Armstrong–Kuusi–Loher, to appear) from the scaled Poincaré inequalities of ScaledPoincare. All L² bookkeeping is carried out on the Lebesgue L² realizations H1Function.toScalarL2, whose triangle inequality is free, and converted to the eLpNorm spelling at the interface.

Generic L²-realization helpers

theorem HCPolySupport.toScalarL2_sub {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u - v).toScalarL2 = u.toScalarL2 - v.toScalarL2

The L² realization is subtractive.

theorem HCPolySupport.toScalarL2_congr {d : ℕ} {U : Set (Vec d)} {u v : H1Function U} (h : u.toFun = v.toFun) : u.toScalarL2 = v.toScalarL2

The L² realization depends only on the underlying function.

theorem HCPolySupport.norm_toScalarL2_add_le {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : ‖(u + v).toScalarL2‖ ≤ ‖u.toScalarL2‖ + ‖v.toScalarL2‖

Triangle inequality for the L² realization of a sum.

theorem HCPolySupport.norm_toScalarL2_sub_le {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : ‖(u - v).toScalarL2‖ ≤ ‖u.toScalarL2‖ + ‖v.toScalarL2‖

Triangle inequality for the L² realization of a difference.

theorem HCPolySupport.l2_normSq_eq_integral {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ‖u.toScalarL2‖ ^ 2 = ∫ (x : Vec d) in U, u.toFun x ^ 2

The squared L²-realization norm is the integral of the square.

F2: the zero-set lower bound

theorem HCPolySupport.matchedPair_zeroSet {d : ℕ} (z : Vec d) {L : ℝ} (f g : H1Function (axisCube z L)) (c : ℝ) (hfm : Measurable f.toFun) (hgm : Measurable g.toFun) (hzero : MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ f.toFun x ≠ 0} + MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ g.toFun x ≠ 0} ≤ MeasureTheory.volume (axisCube z L)) : ‖(H1Function.const c).toScalarL2‖ ≤ ‖(f.addConst (-c)).toScalarL2‖ + ‖(g.addConst (-c)).toScalarL2‖

Zero-set lower bound. If the value sets of f and g together cover at most |U|, then for every level c the L² norm of the constant c on U = axisCube z L is dominated by the two centered L² norms ‖f − c‖ and ‖g − c‖. (Requires measurable representatives, satisfied by the level-set truncations fed in downstream.)

Gradient uniqueness and the H¹-input Dirichlet Poincaré

theorem HCPolySupport.gradCoord_ae_eq_of_toFun_eq {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (p q : H1Function U) (h : p.toFun = q.toFun) (i : Fin d) : (fun (x : Vec d) => p.grad x i) =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => q.grad x i

Two H¹ witnesses with the same value have a.e. equal gradient coordinates on an open domain.

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

Scaled Dirichlet Poincaré for H¹ inputs. If w ∈ H¹(axisCube z L) has a zero-trace representative (MemH10 U w.toFun), then w obeys the scaled Dirichlet Poincaré with its own gradient on the right-hand side.

theorem HCPolySupport.gradCoordToScalarL2_sub {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) (i : Fin d) : (u - v).gradCoordToScalarL2 i = u.gradCoordToScalarL2 i - v.gradCoordToScalarL2 i

The ith gradient L² realization is subtractive.

theorem HCPolySupport.gradientCoordL2NormSum_sub_le {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u - v).gradientCoordL2NormSum ≤ u.gradientCoordL2NormSum + v.gradientCoordL2NormSum

The coordinate-sum gradient norm is subadditive under differences.

F3: the matched-pair Poincaré inequality

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

The matched-pair Poincaré constant 3 (2 C₁ + C₂), with C₁ the mean-zero and C₂ the Dirichlet unit-cube constants.

Equations

• HCPolySupport.matchedPairPoincareConst d = 3 * (2 * HCPolySupport.unitMeanZeroPoincareConst d + HCPolySupport.unitDirichletPoincareConst d)

theorem HCPolySupport.matchedPairPoincareConst_nonneg (d : ℕ) [NeZero d] : 0 ≤ matchedPairPoincareConst d

theorem HCPolySupport.matchedPair_poincare {d : ℕ} [NeZero d] (z : Vec d) {L : ℝ} (hL : 0 < L) (f g : H1Function (axisCube z L)) (hfm : Measurable f.toFun) (hgm : Measurable g.toFun) (hfg : MemH10 (axisCube z L) fun (x : Vec d) => f.toFun x - g.toFun x) (hzero : MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ f.toFun x ≠ 0} + MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ g.toFun x ≠ 0} ≤ MeasureTheory.volume (axisCube z L)) : ‖f.toScalarL2‖ + ‖g.toScalarL2‖ ≤ matchedPairPoincareConst d * L * (f.gradientCoordL2NormSum + g.gradientCoordL2NormSum)

Matched-pair Poincaré (norm form; the high-moment paper's e.doubled.poincare).

If f, g ∈ H¹(axisCube z L) share a boundary trace (f − g ∈ H¹₀) and their value sets together cover at most |U|, then ‖f‖_{L²} + ‖g‖_{L²} ≤ C_d · L · (‖∇f‖ + ‖∇g‖).