BoundaryPoincareCore

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The zero-set Poincaré inequality on an axis cube

This is the analytic core of the funded unit: a coefficient-free Poincaré inequality for an H¹ function that vanishes on a subset of the cube whose volume is a definite fraction of the cube's.

  ‖u‖_{L²(A)} ≤ (1 + √K) · C(d) · L · Σᵢ ‖∂ᵢu‖_{L²(A)}
      whenever  u = 0 on E ⊆ A  and  |A| ≤ K |E| ,   A = axisCube z L .

The proof is the classical two-line argument on top of the mean-zero Poincaré inequality (CoarseGraining's scaled_meanZero_poincare, whose constant unitMeanZeroPoincareConst d · L is the absolute constant of the fixed unit corner cube times the side): the mean is read off on E, where u vanishes, so |E|^{1/2} |(u)_A| = ‖u - (u)_A‖_{L²(E)} ≤ ‖u - (u)_A‖_{L²(A)}, and the triangle inequality then pays (1 + (|A|/|E|)^{1/2}).

This is the trace-measure half of the boundary Poincaré in the only sense the development's carriers support: no surface measure exists anywhere in CoarseGraining or Mathlib, and none is needed — the boundary datum enters through the volume of the part of the cube lying outside the domain, where the zero extension of an H¹₀ function vanishes identically. See BoundaryTraceMeasure for that extension and for the geometric input |A| ≤ 3 |E|.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_le_of_zeroSet_of_volume_le {d : ℕ} (z : HCPolySupport.Vec d) {L K : ℝ} (hL : 0 < L) (hK : 0 ≤ K) (u : HCPolySupport.H1Function (HCPolySupport.axisCube z L)) {E : Set (HCPolySupport.Vec d)} (hEsub : E ⊆ HCPolySupport.axisCube z L) (hEmeas : MeasurableSet E) (hzero : ∀ y ∈ E, u.toFun y = 0) (hvol : MeasureTheory.volume (HCPolySupport.axisCube z L) ≤ ENNReal.ofReal K * MeasureTheory.volume E) : (MeasureTheory.eLpNorm u.toFun 2 (HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L))).toReal ≤ (1 + √K) * (HCPolySupport.unitMeanZeroPoincareConst d * L) * ∑ i : Fin d, (MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.grad x i) 2 (HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L))).toReal

The zero-set Poincaré inequality on an axis cube.

An H¹ function on axisCube z L that vanishes on a measurable subset E carrying at least a K⁻¹ fraction of the cube's volume obeys the un-subtracted L² Poincaré inequality at the cube's own scale, with the coefficient-free constant (1 + √K) · C(d) · L.