OneStepEvenBoundBox

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

Affine moments on an open coordinate box (the unequal-sided cube moment)

CubeMoments.lean computes the moments of an affine function on the equal-sided open cube axisCube z L = ∏ᵢ (zᵢ, zᵢ + L). The boundary branch of the one-step even-part bound (★) never sees an exact cube: it sees the open coordinate box coordBox lo hi = ∏ᵢ (loᵢ, hiᵢ) with unequal sides, because a truncated window, a reflected window, and a transverse halving all change the sides coordinate by coordinate. This module is the side-by-side box analogue of CubeMoments.

The sharp identity is, with x = boxCenter lo hi the centre xᵢ = (loᵢ + hiᵢ)/2,

⨍_B 1 = 1,   ⨍_B (xᵢ − xᵢ) = 0,   ⨍_B (xᵢ − xᵢ)(x_j − x_j) = δ_{ij} · (hiᵢ − loᵢ)²/12 ,

and hence, for the affine function ℓ(x) = c + g·x,

⨍_B ℓ² = ℓ(x)² + ∑ᵢ gᵢ² (hiᵢ − loᵢ)²/12          (`volumeAverage_coordBox_affineEval_sq`).

Unlike the cube case the second term is not proportional to |g|²: each coordinate carries its own side length, and that anisotropy is exactly what the boundary branch exploits. The two comparison corollaries (★) consumes are read straight off the identity:

• normalizedL2On_coordBox_affineEval_congr_of_slope_zero --- sliding (or stretching) the box in a direction i where the slope vanishes, gᵢ = 0, changes nothing: neither the centre value (the i-th term of g·x is 0) nor the i-th summand (gᵢ² = 0).
• normalizedL2On_coordBox_affineEval_half_le --- reverse Chebyshev: halving the transverse sides of a concentric box costs at most the factor two, because each transverse summand loses at most the factor 4 inside the square root while the centre value is unchanged.

The route is the same as in CubeMoments: Fubini via MeasureTheory.Measure.restrict_pi_pi and MeasureTheory.integral_fintype_prod_eq_prod (setIntegral_coordBox_prod), then three one-dimensional moments on Set.Ioo a b, obtained from CubeMoments' moments on Set.Ioo a (a + L) at L = b - a. Normalization goes once through CubeMoments.volumeAverage_eq_of_setIntegral, so that no step reads positivity out of the local context via field_simp.

Three ambient facts about the seminorm are proved alongside, because the boundary branch moves the box before it measures: translation invariance (normalizedL2On_comp_sub_right, through measurePreserving_sub_right), pointwise domination (normalizedL2On_mono_of_abs_le), and the seminorm of a constant (normalizedL2On_const_of_toReal_pos).

References

• Algsuperdiff/Section4/Provider/ExcessDecay/OddReflectionWindow.lean (coordBox).
• Algsuperdiff/Section4/Provider/ExcessDecay/OddReflectionVolume.lean (volume_coordBox).

The centre of a box, and measure-theoretic basics

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.boxCenter {d : ℕ} (lo hi : Fin d → ℝ) : HCPolySupport.Vec d

The centre of the open coordinate box ∏ᵢ (loᵢ, hiᵢ).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.boxCenter lo hi i = (lo i + hi i) / 2

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.boxCenter_apply {d : ℕ} (lo hi : Fin d → ℝ) (i : Fin d) : boxCenter lo hi i = (lo i + hi i) / 2

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_coordBox_ne_top {d : ℕ} (lo hi : Fin d → ℝ) : MeasureTheory.volume (coordBox lo hi) ≠ ⊤

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_coordBox_toReal {d : ℕ} {lo hi : Fin d → ℝ} (hle : ∀ (i : Fin d), lo i ≤ hi i) : (MeasureTheory.volume (coordBox lo hi)).toReal = ∏ i : Fin d, (hi i - lo i)

|B| = ∏ᵢ (hiᵢ − loᵢ).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.integrableOn_coordBox_of_continuous {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Continuous f) (lo hi : Fin d → ℝ) : MeasureTheory.IntegrableOn f (coordBox lo hi) MeasureTheory.volume

A box sits inside the corresponding closed box, which is compact; hence continuous functions are integrable on it.

Fubini: the integral of a coordinate-wise product over a box

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_coordBox_prod {d : ℕ} (lo hi : Fin d → ℝ) (h : Fin d → ℝ → ℝ) : ∫ (x : HCPolySupport.Vec d) in coordBox lo hi, ∏ i : Fin d, h i (x i) = ∏ i : Fin d, ∫ (t : ℝ) in Set.Ioo (lo i) (hi i), h i t

The product formula on a box. ∫_B ∏ᵢ hᵢ(xᵢ) = ∏ᵢ ∫_{(loᵢ,hiᵢ)} hᵢ.

The one-dimensional moments on Set.Ioo a b

The box moments

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_coordBox_centered {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (i : Fin d) : ∫ (x : HCPolySupport.Vec d) in coordBox lo hi, x i - boxCenter lo hi i = 0

First moment: the centre is the barycentre. ∫_B (xᵢ − xᵢ) dx = 0.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_coordBox_centered_mul {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (i j : Fin d) : ∫ (x : HCPolySupport.Vec d) in coordBox lo hi, (x i - boxCenter lo hi i) * (x j - boxCenter lo hi j) = if i = j then (∏ k : Fin d, (hi k - lo k)) * ((hi i - lo i) ^ 2 / 12) else 0

The box second moment, unnormalized. ∫_B (xᵢ − xᵢ)(x_j − x_j) dx = δ_{ij} · |B| · (hiᵢ − loᵢ)²/12.

Affine functions on a box: the sharp L² identity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_coordBox_coordSum {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (a : Fin d → ℝ) : ∫ (x : HCPolySupport.Vec d) in coordBox lo hi, ∑ i : Fin d, a i * (x i - boxCenter lo hi i) = 0

The linear part of an affine function integrates to zero over a box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setIntegral_coordBox_coordQuad {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (g : HCPolySupport.Vec d) : ∫ (x : HCPolySupport.Vec d) in coordBox lo hi, ∑ i : Fin d, ∑ j : Fin d, g i * g j * ((x i - boxCenter lo hi i) * (x j - boxCenter lo hi j)) = (∏ k : Fin d, (hi k - lo k)) * ∑ i : Fin d, g i ^ 2 * ((hi i - lo i) ^ 2 / 12)

The quadratic part: the box second moment, summed against g ⊗ g.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volumeAverage_coordBox_affineEval_sq {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (c : ℝ) (g : HCPolySupport.Vec d) : (HCPolySupport.volumeAverage (coordBox lo hi) fun (y : HCPolySupport.Vec d) => Support.affineEval c g y ^ 2) = Support.affineEval c g (boxCenter lo hi) ^ 2 + ∑ i : Fin d, g i ^ 2 * ((hi i - lo i) ^ 2 / 12)

The sharp L² identity for an affine function on a box. ⨍_B (c + g·x)² = (c + g·x)² + ∑ᵢ gᵢ² (hiᵢ − loᵢ)²/12, with x = boxCenter lo hi.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coordBox_affineEval_sq {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (c : ℝ) (g : HCPolySupport.Vec d) : Support.normalizedL2On (coordBox lo hi) (Support.affineEval c g) ^ 2 = Support.affineEval c g (boxCenter lo hi) ^ 2 + ∑ i : Fin d, g i ^ 2 * ((hi i - lo i) ^ 2 / 12)

The seminorm form of the identity, before taking the square root.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coordBox_affineEval {d : ℕ} {lo hi : Fin d → ℝ} (hlt : ∀ (i : Fin d), lo i < hi i) (c : ℝ) (g : HCPolySupport.Vec d) : Support.normalizedL2On (coordBox lo hi) (Support.affineEval c g) = √(Support.affineEval c g (boxCenter lo hi) ^ 2 + ∑ i : Fin d, g i ^ 2 * ((hi i - lo i) ^ 2 / 12))

The seminorm form of the identity, as a square root.

The two comparison corollaries

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coordBox_affineEval_congr_of_slope_zero {d : ℕ} {lo hi lo' hi' : Fin d → ℝ} (hlt : ∀ (j : Fin d), lo j < hi j) (hlt' : ∀ (j : Fin d), lo' j < hi' j) {i : Fin d} {c : ℝ} {g : HCPolySupport.Vec d} (hg : g i = 0) (hsame : ∀ (j : Fin d), j ≠ i → lo' j = lo j ∧ hi' j = hi j) : Support.normalizedL2On (coordBox lo' hi') (Support.affineEval c g) = Support.normalizedL2On (coordBox lo hi) (Support.affineEval c g)

Sliding the box along a direction of vanishing slope changes nothing.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_coordBox_affineEval_half_le {d : ℕ} {lo hi lo' hi' : Fin d → ℝ} (hlt : ∀ (j : Fin d), lo j < hi j) (hlt' : ∀ (j : Fin d), lo' j < hi' j) {i : Fin d} {c : ℝ} {g : HCPolySupport.Vec d} (hg : g i = 0) (hcen : ∀ (j : Fin d), j ≠ i → lo' j + hi' j = lo j + hi j) (hside : ∀ (j : Fin d), j ≠ i → hi j - lo j ≤ 2 * (hi' j - lo' j)) : 1 / 2 * Support.normalizedL2On (coordBox lo hi) (Support.affineEval c g) ≤ Support.normalizedL2On (coordBox lo' hi') (Support.affineEval c g)

Reverse Chebyshev for affine functions: halving the transverse sides of a concentric box costs at most the factor two.

Translation, domination, constants

theorem Algsuperdiff.Section4.Provider.ExcessDecay.image_sub_coordBox {d : ℕ} (lo hi : Fin d → ℝ) (v : HCPolySupport.Vec d) : (fun (z : HCPolySupport.Vec d) => z - v) '' coordBox lo hi = coordBox (fun (j : Fin d) => lo j - v j) fun (j : Fin d) => hi j - v j

The image of a box under a translation is a box.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_comp_sub_right {d : ℕ} (W : Set (HCPolySupport.Vec d)) (v : HCPolySupport.Vec d) (f : HCPolySupport.Vec d → ℝ) : (Support.normalizedL2On W fun (y : HCPolySupport.Vec d) => f (y - v)) = Support.normalizedL2On ((fun (z : HCPolySupport.Vec d) => z - v) '' W) f

Translation invariance of the normalized seminorm.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_mono_of_abs_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) {f g : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => f y ^ 2) W MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => g y ^ 2) W MeasureTheory.volume) (h : ∀ y ∈ W, |f y| ≤ g y) : Support.normalizedL2On W f ≤ Support.normalizedL2On W g

Pointwise domination.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_const_of_toReal_pos {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hpos : 0 < (MeasureTheory.volume W).toReal) (c : ℝ) : (Support.normalizedL2On W fun (x : HCPolySupport.Vec d) => c) = |c|

The seminorm of a constant.