OneStepPartialReflectionCompose

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

The operator reconciliation

The closing half B ("the multi-face corner obstruction measured"): the multi-face H¹ extension of OneStepPartialReflection is reconciled with the proved partial odd reflection operator oddExtend (OddReflectionMap), so that the boundary branch's reflection apparatus takes no undischarged analytic input beyond the base competitor's data.

The reconciliation

oddExtend_eq_self_of_faceOdd_forall: any function that is pointwise odd under every met-face reflection is a fixed point of oddExtend x m k, off the met hyperplanes. This is the multi-face generalization's one-face interface atoms (oddExtend_eq_self_of_faceOdd_upper/_lower), and — like them — it needs no membership hypothesis: the proof is a strong induction on the number of coordinates at which the point lies beyond a met face, each step reflecting one such coordinate back (windowFold and windowFoldSign are invariant up to the reflected factor's sign, and the oddness pays the sign). oddExtend_ae_eq_self_of_faceOdd_forall is the global a.e. form (the met hyperplanes are Lebesgue-null).

1. Points not beyond any met face are fixed by the fold

2. The operator reconciliation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddExtend_eq_self_of_faceOdd_forall {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {O : HCPolySupport.Vec d → ℝ} (hupO : ∀ (i : Fin d), MeetsUpperFace x m k i → ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -O z) (hlowO : ∀ (i : Fin d), MeetsLowerFace x m k i → ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -O z) {y : HCPolySupport.Vec d} (hney : ∀ (i : Fin d), (MeetsUpperFace x m k i → y i ≠ 1 / 2 * 3 ^ m) ∧ (MeetsLowerFace x m k i → y i ≠ -(1 / 2) * 3 ^ m)) : oddExtend x m k O y = O y

The reconciliation, pointwise. A function pointwise odd under every met-face reflection is fixed by the partial odd reflection oddExtend x m k, at every point off the met hyperplanes. The multi-face generalization of the one-face interface atoms oddExtend_eq_self_of_faceOdd_upper/_lower; as there, no membership hypothesis appears.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oddExtend_ae_eq_self_of_faceOdd_forall {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {O : HCPolySupport.Vec d → ℝ} (hupO : ∀ (i : Fin d), MeetsUpperFace x m k i → ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -O z) (hlowO : ∀ (i : Fin d), MeetsLowerFace x m k i → ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -O z) : oddExtend x m k O =ᵐ[MeasureTheory.volume] O

The reconciliation, almost everywhere. The met hyperplanes are Lebesgue-null.