BoundaryTraceMeasure

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

The trace measure of the boundary window: the zero extension and the slab

The unit needs two things beyond the analytic core of BoundaryPoincareCore:

1. the trace carrier — an H¹₀(□_m) datum, read on a cube A that pokes out of □_m, is an H¹(A) function that vanishes identically on the part of A outside □_m. That part is the development's stand-in for the trace measure: the zero-trace hypothesis is converted into a volume statement, which is the only form the carriers support (no surface measure exists in CoarseGraining or Mathlib). zeroExtendH1 builds the H¹(A) function and eLpNorm_zeroExtend_eq / eLpNorm_zeroExtendGrad_eq say that its norms are the datum's own norms on A ∩ □_m.
2. the slab bound — a quantitative lower bound on the volume of that part. volume_le_three_mul_slab is the sharp form we need: if a set is a "box in the direction e" whose g-range (lo, hi) reaches at least a third of the way past a level a, then the whole set is at most three times the slab {a ≤ g}. The proof is a covering by three translates of the slab — no product-measure computation, only translation invariance and subadditivity.

1. The zero extension as an H¹ function on an arbitrary set

theorem Algsuperdiff.Section4.Provider.ExcessDecay.fderiv_apply_eq_zero_of_notMem_tsupport {d : ℕ} {φ : HCPolySupport.Vec d → ℝ} {x : HCPolySupport.Vec d} (hx : x ∉ tsupport φ) (i : Fin d) : (fderiv ℝ φ x) (HCPolySupport.basisVec i) = 0

Off its topological support a function has vanishing derivative.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.hasWeakGradientOn_of_univ {d : ℕ} {V : Set (HCPolySupport.Vec d)} {u : HCPolySupport.Vec d → ℝ} {Du : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : HCPolySupport.HasWeakGradientOn Set.univ u Du) : HCPolySupport.HasWeakGradientOn V u Du

A global weak-gradient graph restricts to every set: the test functions of the smaller set are test functions of the ambient space, and both integrands vanish off their support.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendH1 {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) (A : Set (HCPolySupport.Vec d)) : HCPolySupport.H1Function A

The zero extension of an H¹₀(V) datum, read on an arbitrary set A.

The value and the gradient are the literal zero extensions of OddReflectionGlue; the weak-gradient identity is its global one, restricted.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendH1_toFun {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) (A : Set (HCPolySupport.Vec d)) : (zeroExtendH1 hV u A).toFun = zeroExtend V u.toFun

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendH1_grad {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) (A : Set (HCPolySupport.Vec d)) : (zeroExtendH1 hV u A).grad = zeroExtendGrad V u.grad

theorem Algsuperdiff.Section4.Provider.ExcessDecay.zeroExtendH1_eq_zero_of_notMem {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (u : HCPolySupport.H10Function V) (A : Set (HCPolySupport.Vec d)) {y : HCPolySupport.Vec d} (hy : y ∉ V) : (zeroExtendH1 hV u A).toFun y = 0

The zero extension vanishes off V.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_zeroExtend_eq {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (f : HCPolySupport.Vec d → ℝ) (A : Set (HCPolySupport.Vec d)) : MeasureTheory.eLpNorm (zeroExtend V f) 2 (MeasureTheory.volume.restrict A) = MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict (A ∩ V))

The L² norm of the zero extension over A is the datum's own norm over A ∩ V.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_zeroExtendGrad_eq {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (A : Set (HCPolySupport.Vec d)) (i : Fin d) : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => zeroExtendGrad V G y i) 2 (MeasureTheory.volume.restrict A) = MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => G y i) 2 (MeasureTheory.volume.restrict (A ∩ V))

The L² norm of a coordinate of the zero-extended gradient over A is the datum's own norm over A ∩ V.

2. The slab: three translates cover the box

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_le_three_mul_slab {d : ℕ} {A : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → ℝ} {e : HCPolySupport.Vec d} {lo hi a : ℝ} (hg : ∀ (y : HCPolySupport.Vec d) (s : ℝ), g (y + s • e) = g y + s) (hrange : ∀ y ∈ A, lo < g y ∧ g y < hi) (hshift : ∀ y ∈ A, ∀ (s : ℝ), lo < g y + s → g y + s < hi → y + s • e ∈ A) (hah : a < hi) (halo : a - 2 * (hi - a) ≤ lo) : MeasureTheory.volume A ≤ 3 * MeasureTheory.volume (A ∩ {y : HCPolySupport.Vec d | a ≤ g y})

The slab covering bound.

If A is a box in the direction e — every point has g-value in (lo, hi), and shifting a point along e keeps it in A as long as the g-value stays in (lo, hi) — and the level a sits within hi of the top and at least a third of the g-range from the bottom (a - 2(hi - a) ≤ lo), then A is covered by three translates of the slab A ∩ {a ≤ g}.

No measurability is required: the proof is measure_mono plus subadditivity plus translation invariance.