MatchedPair

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

The matched-pair Sobolev inequality

This module re-exports the scaled Poincaré inequalities, the zero-set lower bound, and the matched-pair Poincaré inequality from the MatchedPair submodules, and proves the top-level matched-pair Sobolev inequality (the high-moment paper's Lemma 3.2, l.doubled.sobolev / e.doubled.sobolev, Armstrong–Kuusi–Loher, to appear):

For f, g ∈ H¹(axisCube z L) sharing a boundary trace (f − g ∈ H¹₀) whose value sets together cover at most |U|, ‖f‖_{L^{2*}} + ‖g‖_{L^{2*}} ≤ C_d (∑ᵢ‖∂ᵢf‖_{L²} + ∑ᵢ‖∂ᵢg‖_{L²}), in the split eLpNorm spelling aligned with cube_sobolev_embedding.

The proof combines the cube Sobolev embedding for f and g with the matched-pair Poincaré inequality to absorb the lower-order L⁻¹‖·‖_{L²} terms.

theorem HCPolySupport.matchedPair_sobolev {d : ℕ} (hd : 3 ≤ d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : Vec d) (L : ℝ), 0 < L → ∀ (f g : H1Function (axisCube z L)), Measurable f.toFun → Measurable g.toFun → (MemH10 (axisCube z L) fun (x : Vec d) => f.toFun x - g.toFun x) → 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) → (MeasureTheory.eLpNorm f.toFun (↑(twoStar d)) (volumeMeasureOn (axisCube z L))).toReal + (MeasureTheory.eLpNorm g.toFun (↑(twoStar d)) (volumeMeasureOn (axisCube z L))).toReal ≤ C * (∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => f.grad x i) 2 (volumeMeasureOn (axisCube z L))).toReal + ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => g.grad x i) 2 (volumeMeasureOn (axisCube z L))).toReal)

Matched-pair Sobolev inequality (the high-moment paper's Lemma 3.2, split eLpNorm form).

For d ≥ 3 there is an absolute constant C = C(d) ≥ 0 such that for every axis cube U = axisCube z L of side L > 0 and every pair f, g ∈ H¹(U) with f − g ∈ H¹₀(U) and |{f ≠ 0}| + |{g ≠ 0}| ≤ |U| (measurable representatives), ‖f‖_{L^{2*}(U)} + ‖g‖_{L^{2*}(U)} ≤ C (∑ᵢ‖∂ᵢf‖_{L²(U)} + ∑ᵢ‖∂ᵢg‖_{L²(U)}).