OddReflectionSobolevL2

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

The cellwise change of variables for the partial odd reflection

OddReflectionMap supplies the pointwise half (abs_oddExtend: |oddExtend f| = |f ∘ windowFold|) and OddReflectionVolume the volume half (volume_reflectedWindow_le); what is missing is the change of variables that turns an integral over the partially reflected window into 2^{#S} copies of the integral over the window.

The route

windowFold acts coordinatewise, and in each coordinate it is either the identity or the reflection through the met face. Hence for every point y there is a subset S ⊆ Fin d with

  windowFold y = cellMap S y ,   cellMap S y i = if i ∈ S then 2·pᵢ - yᵢ else yᵢ ,

pᵢ the met-face level of coordinate i (foldPivot). Each cellMap S is an involutive homeomorphism and — being a product of one-dimensional reflections and identities — measure preserving (volume_preserving_pi). Splitting the reflected window along the 2^d sets

  B S = (reflectedWindow \ N) ∩ {y : windowFold y = cellMap S y} ,

N the (Lebesgue null) union of the interface hyperplanes {yᵢ = pᵢ}, and using windowFold_mem_truncatedWindow off N, one gets cellMap S '' (B S) ⊆ truncatedWindow and therefore

  ∫⁻_{reflected V} g ∘ windowFold  ≤  2^d · ∫⁻_V g .

Only a cover by the B S is needed, never a partition, so no disjointness bookkeeping appears. The exact factor is 2^{#S} for the met set; the stated 2^d is the two-sided form the analytic layer consumes (matching volume_reflectedWindow_le).

What is not done here

No harmonicity, no H¹ statement: this module is pure measure theory.

References

• CoarseGraining Homogenization.Sobolev.Foundations.CubeReflection.Reflections (realFaceReflection, measurePreserving_realFaceReflection).
• Mathlib MeasureTheory.volume_preserving_pi, MeasureTheory.MeasurePreserving.lintegral_comp_emb, MeasureTheory.lintegral_iUnion_le.

1. The pivot of a coordinate and the cell maps

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.foldPivot {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : ℝ

The reflection level of coordinate i: the met face of ∂□_m, or 0 if that coordinate meets no face.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.cellMap {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) : HCPolySupport.Vec d → HCPolySupport.Vec d

The reflection of exactly the coordinates in S through their pivots.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.cellMap x m k S y i = if i ∈ S then HCPolySupport.realFaceReflection (Algsuperdiff.Section4.Provider.ExcessDecay.foldPivot x m k i) (y i) else y i

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cellMap_apply {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) (y : HCPolySupport.Vec d) (i : Fin d) : cellMap x m k S y i = if i ∈ S then HCPolySupport.realFaceReflection (foldPivot x m k i) (y i) else y i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cellMap_involutive {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) (y : HCPolySupport.Vec d) : cellMap x m k S (cellMap x m k S y) = y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cellMap_injective {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) : Function.Injective (cellMap x m k S)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.continuous_cellMap {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) : Continuous (cellMap x m k S)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurableEmbedding_cellMap {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) : MeasurableEmbedding (cellMap x m k S)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.measurePreserving_cellMap {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (S : Finset (Fin d)) : MeasureTheory.MeasurePreserving (cellMap x m k S) MeasureTheory.volume MeasureTheory.volume

2. The fold is a cell map at every point

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldCoord_eq_or {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) (t : ℝ) : foldCoord x m k i t = t ∨ foldCoord x m k i t = HCPolySupport.realFaceReflection (foldPivot x m k i) t

theorem Algsuperdiff.Section4.Provider.ExcessDecay.continuous_windowFold {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : Continuous (windowFold x m k)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_cellMap_eq {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (y : HCPolySupport.Vec d) : ∃ (S : Finset (Fin d)), windowFold x m k y = cellMap x m k S y

Every point lies in some cell. The coordinatewise fold agrees, at each point, with the reflection of the coordinates it actually moves.

3. The interface hyperplanes are null

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

def Algsuperdiff.Section4.Provider.ExcessDecay.foldInterface {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : Set (HCPolySupport.Vec d)

The union of the interface hyperplanes: the null set the change of variables discards.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.foldInterface x m k = ⋃ (i : Fin d), {y : HCPolySupport.Vec d | y i = Algsuperdiff.Section4.Provider.ExcessDecay.foldPivot x m k i}

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_foldInterface_eq_zero {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : MeasureTheory.volume (foldInterface x m k) = 0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.notMem_foldInterface_apply {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {y : HCPolySupport.Vec d} (hy : y ∉ foldInterface x m k) (i : Fin d) : y i ≠ foldPivot x m k i

4. The cellwise change of variables

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setLIntegral_comp_windowFold_le {d : ℕ} (x : HCPolySupport.Vec d) {m k : ℤ} (hkm : k < m) (g : HCPolySupport.Vec d → ENNReal) : ∫⁻ (y : HCPolySupport.Vec d) in reflectedWindow x m k, g (windowFold x m k y) ≤ 2 ^ d * ∫⁻ (y : HCPolySupport.Vec d) in truncatedWindow x m k, g y

: the cellwise change of variables. Folding the partially reflected window onto the window costs at most the factor 2^d (the exact factor is 2^{#S} for the met set S).

5. The L² cost of the odd extension

theorem Algsuperdiff.Section4.Provider.ExcessDecay.enorm_oddExtend {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (f : HCPolySupport.Vec d → ℝ) (y : HCPolySupport.Vec d) : ‖oddExtend x m k f y‖ₑ = ‖f (windowFold x m k y)‖ₑ

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setLIntegral_enorm_rpow_oddExtend_le {d : ℕ} (x : HCPolySupport.Vec d) {m k : ℤ} (hkm : k < m) (f : HCPolySupport.Vec d → ℝ) (q : ℝ) : ∫⁻ (y : HCPolySupport.Vec d) in reflectedWindow x m k, ‖oddExtend x m k f y‖ₑ ^ q ≤ 2 ^ d * ∫⁻ (y : HCPolySupport.Vec d) in truncatedWindow x m k, ‖f y‖ₑ ^ q

, in the shape the Lᵖ layer consumes.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_oddExtend_le {d : ℕ} (x : HCPolySupport.Vec d) {m k : ℤ} (hkm : k < m) (f : HCPolySupport.Vec d → ℝ) : MeasureTheory.eLpNorm (oddExtend x m k f) 2 (MeasureTheory.volume.restrict (reflectedWindow x m k)) ≤ 2 ^ d * MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict (truncatedWindow x m k))

: the odd extension costs at most C(d) = 2^d in L².