OddReflectionVolume

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

Volume comparability of the window and its partial reflection

Since the normalized norm divides by the volume, that step needs the two volumes to be comparable.

  |V| = ∏ᵢ (windowHi i - windowLo i)₊ ,
  |reflected V| = ∏ᵢ (reflectedHi i - reflectedLo i)₊ ,

and using the per-coordinate edge identity of OddReflectionWindow (each met coordinate doubles, each unmet coordinate is unchanged):

  |V| ≤ |reflected V| ≤ 2^d · |V| .

The exact factor is 2^{#S} for the met set S; the two-sided bound above is the form the estimate consumes (the surplus 2^{d - #S} is absorbed by the dimensional constant C(d)), and it avoids carrying a Finset cardinality through the analytic layer.

What is not done here

The cellwise change of variables — that ∫_{reflected V} |oddExtend f|² = 2^{#S} ∫_V |f|² — is not proved here.

References

• Mathlib MeasureTheory.volume_pi_pi, Real.volume_Ioo.

1. The volume of a coordinate box

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_coordBox {d : ℕ} (lo hi : Fin d → ℝ) : MeasureTheory.volume (coordBox lo hi) = ∏ i : Fin d, ENNReal.ofReal (hi i - lo i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurableSet_coordBox {d : ℕ} (lo hi : Fin d → ℝ) : MeasurableSet (coordBox lo hi)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurableSet_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasurableSet (reflectedWindow x m k)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_truncatedWindow_eq {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasureTheory.volume (truncatedWindow x m k) = ∏ i : Fin d, ENNReal.ofReal (windowHi x m k i - windowLo x m k i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_reflectedWindow_eq {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasureTheory.volume (reflectedWindow x m k) = ∏ i : Fin d, ENNReal.ofReal (reflectedHi x m k i - reflectedLo x m k i)

2. The two-sided volume comparison

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_truncatedWindow_le_volume_reflectedWindow {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasureTheory.volume (truncatedWindow x m k) ≤ MeasureTheory.volume (reflectedWindow x m k)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_reflectedWindow_le {d : ℕ} (x : HCPolySupport.Vec d) {m k : ℤ} (hkm : k < m) : MeasureTheory.volume (reflectedWindow x m k) ≤ 2 ^ d * MeasureTheory.volume (truncatedWindow x m k)

The partial reflection multiplies the volume by at most 2^d. The exact factor is 2^{#S}, S the met set; the doubling happens exactly in the met coordinates (reflectedHi_sub_reflectedLo_of_*).