MeanFinalCore

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

(A), step 2: the doubled-window transfer for a face-odd function

  ⨍_D G² ≤ 3 ⨍_K G² + 8β² ,   hence   ‖G‖_{L²(D)} ≤ 2‖G‖_{L²(K)} + 3|β| .

The β-term is unavoidable and is the reason the final assembly of (A) is an absorption: G is not odd, only W is, and G ∘ ρ = −(G + 2β). In the assembly this term is multiplied by the quadratically small Hessian factor, so it is absorbed rather than iterated.

The proof is a measure-preserving change of variables (ρ is an involutive measurable embedding preserving Lebesgue measure) plus the observation that the face hyperplane is null.

1. The face hyperplane is null

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.volume_coordHyperplane_eq_zero {d : ℕ} (i : Fin d) (a : ℝ) : MeasureTheory.volume {y : HCPolySupport.Vec d | y i = a} = 0

A coordinate hyperplane has Lebesgue measure zero.

2. The doubled-window transfer

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_doubled_le {d : ℕ} {i : Fin d} {a : ℝ} {K D : Set (HCPolySupport.Vec d)} {W : HCPolySupport.Vec d → ℝ} {beta : ℝ} (hodd : ∀ (z : HCPolySupport.Vec d), W (HCPolySupport.coordFaceReflection a i z) = -W z) (hKm : MeasurableSet K) (hDm : MeasurableSet D) (hKD : K ⊆ D) (hDsplit : ∀ y ∈ D, y ∈ K ∨ HCPolySupport.coordFaceReflection a i y ∈ K ∨ y i = a) (hKpos : 0 < (MeasureTheory.volume K).toReal) (hDpos : 0 < (MeasureTheory.volume D).toReal) (hKleD : (MeasureTheory.volume K).toReal ≤ (MeasureTheory.volume D).toReal) (hDtop : MeasureTheory.volume D ≠ ⊤) (hGD : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => W y - beta) 2 (MeasureTheory.volume.restrict D)) : (Support.normalizedL2On D fun (y : HCPolySupport.Vec d) => W y - beta) ≤ (2 * Support.normalizedL2On K fun (y : HCPolySupport.Vec d) => W y - beta) + 3 * |beta|

The oscillation on the doubled window, transferred back to the cube.

For W odd about {yᵢ = a} and D covered — up to that hyperplane — by K and the reflection of K, the normalized seminorm of G = W − β on D is controlled by the one on K plus a multiple of |β|.