OneStepCornerTransportGeom

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

Coordinate-negation transport of the §4.3 boundary-window geometry

The domain cube □_m is origin-symmetric, so the involution

  σ := σ_i := coordFaceReflection (0 : ℝ) i

which negates the i-th coordinate and fixes every other one, maps □_m onto itself. Consequently it carries the truncated window (x + □_k) ∩ □_m onto (σ x + □_k) ∩ □_m — equivalently, the window centred at σ x is the σ-preimage of the window centred at x — and it exchanges the upper and the lower i-face of ∂□_m while fixing the met/unmet status of every other face.

This is exactly what lets the proved upper-face-only odd-class apparatus of OddReflectionWindow be read at every met configuration: a lower i-face configuration at x is an upper i-face configuration at σ x, and the two window geometries are related by the single change of variables σ.

Concretely the module transports, one by one, every piece of the OddReflectionWindow geometry across σ:

  MeetsUpperFace (σ x) m k i ↔ MeetsLowerFace x m k i      (faces swap at `i`)
  MeetsUpperFace (σ x) m k l ↔ MeetsUpperFace x m k l      (l ≠ i: unchanged)
  windowLo   (σ x) m k i = -windowHi   x m k i
  windowHi   (σ x) m k i = -windowLo   x m k i
  reflectedLo (σ x) m k i = -reflectedHi x m k i
  reflectedHi (σ x) m k i = -reflectedLo x m k i
  truncatedWindow  (σ x) m k = σ ⁻¹' truncatedWindow  x m k
  reflectedWindow  (σ x) m k = σ ⁻¹' reflectedWindow  x m k

Since σ is an involution (coordFaceReflection_involutive) the preimage form is also the image form; the preimage form is the one the change-of-variables consumers want.

References

• ABK26, l.excess.decay.good.scales; the odd-reflection step replaced.
• CoarseGraining Homogenization.Sobolev.Foundations.CubeReflection.Reflections (coordFaceReflection, coordFaceReflection_involutive).

1. The coordinate-negation involution

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_openCubeSet_coordFaceReflection_zero_iff {d : ℕ} {m : ℤ} (i : Fin d) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection 0 i y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) ↔ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The domain cube □_m is origin-symmetric, hence σ_i-invariant.

2. The met faces: the i-faces swap, the others are fixed

theorem Algsuperdiff.Section4.Provider.ExcessDecay.meetsUpperFace_coordFaceReflection_zero_self {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (i : Fin d) : MeetsUpperFace (HCPolySupport.coordFaceReflection 0 i x) m k i ↔ MeetsLowerFace x m k i

Negating the i-th coordinate turns the lower i-face into the upper one.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.meetsLowerFace_coordFaceReflection_zero_self {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (i : Fin d) : MeetsLowerFace (HCPolySupport.coordFaceReflection 0 i x) m k i ↔ MeetsUpperFace x m k i

Negating the i-th coordinate turns the upper i-face into the lower one.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.meetsUpperFace_coordFaceReflection_zero_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i l : Fin d} (hli : l ≠ i) : MeetsUpperFace (HCPolySupport.coordFaceReflection 0 i x) m k l ↔ MeetsUpperFace x m k l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.meetsLowerFace_coordFaceReflection_zero_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i l : Fin d} (hli : l ≠ i) : MeetsLowerFace (HCPolySupport.coordFaceReflection 0 i x) m k l ↔ MeetsLowerFace x m k l

3. The window endpoints

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowLo_coordFaceReflection_zero_self {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : windowLo (HCPolySupport.coordFaceReflection 0 i x) m k i = -windowHi x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowHi_coordFaceReflection_zero_self {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : windowHi (HCPolySupport.coordFaceReflection 0 i x) m k i = -windowLo x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowLo_coordFaceReflection_zero_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i l : Fin d} (hli : l ≠ i) : windowLo (HCPolySupport.coordFaceReflection 0 i x) m k l = windowLo x m k l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.windowHi_coordFaceReflection_zero_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i l : Fin d} (hli : l ≠ i) : windowHi (HCPolySupport.coordFaceReflection 0 i x) m k l = windowHi x m k l

4. The reflected-window endpoints

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedLo_coordFaceReflection_zero_self {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : reflectedLo (HCPolySupport.coordFaceReflection 0 i x) m k i = -reflectedHi x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_coordFaceReflection_zero_self {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : reflectedHi (HCPolySupport.coordFaceReflection 0 i x) m k i = -reflectedLo x m k i

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedLo_coordFaceReflection_zero_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i l : Fin d} (hli : l ≠ i) : reflectedLo (HCPolySupport.coordFaceReflection 0 i x) m k l = reflectedLo x m k l

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedHi_coordFaceReflection_zero_ne {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i l : Fin d} (hli : l ≠ i) : reflectedHi (HCPolySupport.coordFaceReflection 0 i x) m k l = reflectedHi x m k l

5. The two window identities

theorem Algsuperdiff.Section4.Provider.ExcessDecay.truncatedWindow_coordFaceReflection_zero {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : truncatedWindow (HCPolySupport.coordFaceReflection 0 i x) m k = HCPolySupport.coordFaceReflection 0 i ⁻¹' truncatedWindow x m k

The truncated window transports. The window centred at σ_i x is the σ_i-preimage of the window centred at x; equivalently (as σ_i is an involution) its σ_i-image.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.reflectedWindow_coordFaceReflection_zero {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (i : Fin d) : reflectedWindow (HCPolySupport.coordFaceReflection 0 i x) m k = HCPolySupport.coordFaceReflection 0 i ⁻¹' reflectedWindow x m k

The partially reflected window transports. This is the statement that lets the upper-face-only odd-class apparatus be read at a lower-face configuration, by the change of variables σ_i.