OddReflectionMap

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

The partial odd reflection operator, and the odd affine class

The fold and its sign

Each met face contributes one coordinate reflection, and by not_meetsLowerFace_of_meetsUpperFace a coordinate meets at most one face, so the whole group action is realized by a single coordinatewise fold

  foldCoord i t = min t (3^m - t)     if the upper i-face is met,
                = max t (-3^m - t)    if the lower i-face is met,
                = t                   otherwise,

with the matching odd sign foldSignCoord i t = ±1 (negative exactly on the reflected side), and windowFoldSign y = ∏ᵢ foldSignCoord i (y i).

oddExtend f is y ↦ windowFoldSign y · f (windowFold y), and oddExtendGrad G carries the extra per-coordinate sign that the chain rule produces.

The odd affine class 𝕃_odd(V)

IsOddAffineData x m k c A says the affine function ℓ(y) = c + A·(y-x) vanishes on every hyperplane containing a met face — the paper's 𝕃_odd(V). Two structural facts are proved:

• if the i-face is met then A j = 0 for every j ≠ i (slope_eq_zero_of_ne_of_meets), so at one met face the class is the single line ℝ·(y_i - a_i);
• if two different coordinates meet a face then ℓ ≡ 0 (affineLift_eq_zero_of_two_met) — at an edge or corner of □_m the class 𝕃_odd(V) collapses to {0}.

oddExtend_affineLift is the paper's "if ℓ ∈ 𝕃_odd(V), then ℓ is odd under each of these reflections": the odd extension of such an ℓ is ℓ itself, so the extension of v₀ - ℓ is the odd extension of v₀ - ℓ.

What is not done here

No H¹ statement, no weak harmonicity, no measure-theoretic change of variables.

References

• CoarseGraining Homogenization.Sobolev.Foundations.CubeDirichletH2.OddReflection (the all-faces construction adapted here) and Homogenization.Sobolev.Foundations.CubeReflection.Reflections (coordFaceReflection, the one-face affine map).

1. The coordinatewise fold and its sign

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

The fold of one coordinate into the window's side of the met face.

Equations

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

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

The odd sign attached to one coordinate: -1 exactly on the reflected side of a met face.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldCoord_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : MeetsUpperFace x m k i) (t : ℝ) : foldCoord x m k i t = min t (3 ^ m - t)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldCoord_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : ¬MeetsUpperFace x m k i) (h : MeetsLowerFace x m k i) (t : ℝ) : foldCoord x m k i t = max t (-3 ^ m - t)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldCoord_of_unmet {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : ¬MeetsUpperFace x m k i) (hlow : ¬MeetsLowerFace x m k i) (t : ℝ) : foldCoord x m k i t = t

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldSignCoord_of_meetsUpperFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (h : MeetsUpperFace x m k i) (t : ℝ) : foldSignCoord x m k i t = if 1 / 2 * 3 ^ m < t then -1 else 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldSignCoord_of_meetsLowerFace {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : ¬MeetsUpperFace x m k i) (h : MeetsLowerFace x m k i) (t : ℝ) : foldSignCoord x m k i t = if t < -(1 / 2) * 3 ^ m then -1 else 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.foldSignCoord_of_unmet {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hup : ¬MeetsUpperFace x m k i) (hlow : ¬MeetsLowerFace x m k i) (t : ℝ) : foldSignCoord x m k i t = 1

2. The fold, the global sign, and the odd extension

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

The coordinatewise fold of Vec d onto the window's side of every met face: the composite of the reflections in the met faces, applied to whichever of the 2^{#S} cells the point lies in.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.windowFold x m k y i = Algsuperdiff.Section4.Provider.ExcessDecay.foldCoord x m k i (y i)

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

The global odd sign: (-1)^{#\{i : y \text{ is beyond the met } i\text{-face}\}}.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.windowFoldSign x m k y = ∏ i : Fin d, Algsuperdiff.Section4.Provider.ExcessDecay.foldSignCoord x m k i (y i)

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowFold_apply {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (y : HCPolySupport.Vec d) (i : Fin d) : windowFold x m k y i = foldCoord x m k i (y i)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_foldSignCoord {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) (t : ℝ) : |foldSignCoord x m k i t| = 1

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_windowFoldSign {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (y : HCPolySupport.Vec d) : |windowFoldSign x m k y| = 1

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.oddExtend {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d → ℝ

The partial odd reflection of a scalar.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.oddExtendGrad {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) : HCPolySupport.Vec d → HCPolySupport.Vec d

The partial odd reflection of a gradient field. The chain rule for the coordinate fold contributes the extra per-coordinate sign.

Equations

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

@[simp]

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

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddExtendGrad_apply {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (G : HCPolySupport.Vec d → HCPolySupport.Vec d) (y : HCPolySupport.Vec d) (i : Fin d) : oddExtendGrad x m k G y i = windowFoldSign x m k y * foldSignCoord x m k i (y i) * G (windowFold x m k y) i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddExtend_sub {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (f g : HCPolySupport.Vec d → ℝ) : (oddExtend x m k fun (y : HCPolySupport.Vec d) => f y - g y) = fun (y : HCPolySupport.Vec d) => oddExtend x m k f y - oddExtend x m k g y

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_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)|

4. The fold maps the reflected window onto the window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowFold_mem_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {y : HCPolySupport.Vec d} (hkm : k < m) (hy : y ∈ reflectedWindow x m k) (hup : ∀ (i : Fin d), MeetsUpperFace x m k i → y i ≠ 1 / 2 * 3 ^ m) (hlow : ∀ (i : Fin d), MeetsLowerFace x m k i → y i ≠ -(1 / 2) * 3 ^ m) : windowFold x m k y ∈ truncatedWindow x m k

The fold is onto the window, off the interfaces. Every point of the partially reflected window that avoids the reflection hyperplanes is carried into the window itself by windowFold. (The excluded set is a finite union of hyperplanes, hence Lebesgue-null; the null set is what the downstream change of variables discards.)

5. The odd affine class 𝕃_odd(V)

def Algsuperdiff.Section4.Provider.ExcessDecay.IsOddAffineData {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (c : ℝ) (A : HCPolySupport.Vec d) : Prop

The odd affine class of the paper's e.v0.hessian: the affine functions ℓ(y) = c + A·(y-x) that vanish on every hyperplane containing a face of ∂□_m meeting the closure of the window.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isOddAffineData_of_no_met_face {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (c : ℝ) (A : HCPolySupport.Vec d) (hup : ∀ (i : Fin d), ¬MeetsUpperFace x m k i) (hlow : ∀ (i : Fin d), ¬MeetsLowerFace x m k i) : IsOddAffineData x m k c A

In the interior regime — no face met — the odd class is all of 𝕃.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.slope_eq_zero_of_ne_of_meets {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {c : ℝ} {A : HCPolySupport.Vec d} (hodd : IsOddAffineData x m k c A) {i : Fin d} (hi : MeetsUpperFace x m k i ∨ MeetsLowerFace x m k i) {j : Fin d} (hji : j ≠ i) : A j = 0

The tangential slopes vanish. If the i-face is met then every coordinate j ≠ i of the slope of an odd affine function is zero, so at a single met face 𝕃_odd(V) is the one-dimensional space ℝ·(y_i - a_i).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.affineLift_eq_zero_of_two_met {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {c : ℝ} {A : HCPolySupport.Vec d} (hodd : IsOddAffineData x m k c A) {i j : Fin d} (hij : i ≠ j) (hi : MeetsUpperFace x m k i ∨ MeetsLowerFace x m k i) (hj : MeetsUpperFace x m k j ∨ MeetsLowerFace x m k j) : affineLift x c A = fun (x : HCPolySupport.Vec d) => 0

At an edge or corner the odd class collapses. If two different coordinates each meet a face of ∂□_m, the only odd affine function is 0.

6. Odd affine functions are fixed by the odd extension

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddExtend_affineLift {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {c : ℝ} {A : HCPolySupport.Vec d} (hodd : IsOddAffineData x m k c A) : oddExtend x m k (affineLift x c A) = affineLift x c A

The oddness step. An affine function in 𝕃_odd(V) is odd under every met-face reflection, hence is its own partial odd extension. Consequently the odd extension of v₀ - ℓ is the odd extension of v₀ minus ℓ, which is what the free parameter ℓ of e.v0.hessian is for.