OneStepOddClassCornerMoments

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

Affine box-moment comparisons, and the full-met-set fold

Two L² transfer tools for the corner pricing.

1. The controlled box comparison (normalizedL2On_coordBox_affineEval_le_of_controlled): for an affine function and two nondegenerate boxes, if in every coordinate carrying a nonzero slope the first box's edge and centre offset are within κ edges of the second box, then the first seminorm is at most √((24d+1)κ² + 2) times the second. Proof: the proved sharp moment identity normalizedL2On_coordBox_affineEval_sq on both boxes, the centre shift by affineEval_eq_center_add, and Cauchy–Schwarz (sq_sum_le_card_mul_sum_sq). This generalizes the proved reverse Chebyshev (normalizedL2On_coordBox_affineEval_half_le) to boxes that are neither concentric nor nested, which is what the window-hugging corner slabs need.

2. The full-met-set fold (normalizedL2On_reflectedWindow_le_of_faceOdd_forall): a competitor odd under every met-face reflection has doubled-window seminorm at most 2^d times its window seminorm — 's operator reconciliation composed with the proved cellwise L² cost of the odd extension. The companion normalizedL2On_reflectedWindow_affineEval_le prices an arbitrary affine function on the doubled window against the window (instance of 1 at κ = 2: each reflected edge is at most doubled and each centre moves by at most half an edge).

1. L² data of an affine function on a box

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.memLp_affineEval_coordBox {d : ℕ} (lo hi : Fin d → ℝ) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict (coordBox lo hi))

An affine function is square integrable on every coordinate box.

2. The controlled box comparison

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_coordBox_affineEval_le_of_controlled {d : ℕ} {lo₁ hi₁ lo₂ hi₂ : Fin d → ℝ} (hlt₁ : ∀ (l : Fin d), lo₁ l < hi₁ l) (hlt₂ : ∀ (l : Fin d), lo₂ l < hi₂ l) {κ c : ℝ} {g : HCPolySupport.Vec d} (hctrl : ∀ (l : Fin d), g l = 0 ∨ hi₁ l - lo₁ l ≤ κ * (hi₂ l - lo₂ l) ∧ |boxCenter lo₁ hi₁ l - boxCenter lo₂ hi₂ l| ≤ κ * (hi₂ l - lo₂ l)) : Support.normalizedL2On (coordBox lo₁ hi₁) (Support.affineEval c g) ≤ √((24 * ↑d + 1) * κ ^ 2 + 2) * Support.normalizedL2On (coordBox lo₂ hi₂) (Support.affineEval c g)

The controlled box comparison for affine functions. If every nonzero-slope coordinate of B₁ has edge and centre offset within κ edges of B₂, then ‖ℓ‖_{L²(B₁)} ≤ √((24d+1)κ²+2) ‖ℓ‖_{L²(B₂)}.

3. The doubled window against the window, for affine functions

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_reflectedWindow_affineEval_le {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) (c : ℝ) (g : HCPolySupport.Vec d) : Support.normalizedL2On (reflectedWindow x m k) (Support.affineEval c g) ≤ √((24 * ↑d + 1) * 2 ^ 2 + 2) * Support.normalizedL2On (truncatedWindow x m k) (Support.affineEval c g)

An affine function's doubled-window seminorm is controlled by its window seminorm: the instance of the controlled comparison at κ = 2.

4. The full-met-set fold

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_reflectedWindow_le_of_faceOdd_forall {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k < m) {V : HCPolySupport.Vec d → ℝ} (hupV : ∀ (l : Fin d), MeetsUpperFace x m k l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l z) = -V z) (hlowV : ∀ (l : Fin d), MeetsLowerFace x m k l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l z) = -V z) (hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m k))) : Support.normalizedL2On (reflectedWindow x m k) V ≤ 2 ^ d * Support.normalizedL2On (truncatedWindow x m k) V

The fold: a competitor odd under every met-face reflection has doubled-window seminorm at most 2^d times its window seminorm.

5. A seminorm triangle for differences

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_sub_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict W)) : (Support.normalizedL2On W fun (y : HCPolySupport.Vec d) => f y - g y) ≤ Support.normalizedL2On W f + Support.normalizedL2On W g

‖f − g‖_{L²(W)} ≤ ‖f‖_{L²(W)} + ‖g‖_{L²(W)}.