OneStepCornerSeamCore #

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

The a.e. seam of the boundary branch: a globally met-face-odd representative #

The odd-class apparatus of the boundary branch (OneStepEvenBoundFinal's (★) and OneStepOddClassCornerFinal's (★★)) consumes the global pointwise oddness binders

  ∀ z : Vec d,  V (r_l z) = − V z          (r_l the reflection in a met face)

while the competitor the chain actually produces is a Weyl representative V, which is only almost everywhere equal to the pointwise-odd H¹ datum w delivered by the reflection chain (OneStepPartialReflection.exists_h1_oddReflection_reflectedWindow). This module closes that seam in two steps.

Step 1: a.e. oddness becomes pointwise oddness on the doubled window #

The doubled window R = reflectedWindow x m k is open and invariant under every met-face reflection (mem_reflectedWindow_coordFaceReflection_iff), a Weyl representative is continuous on it (continuousOn_of_harmonicOnNhd), and the reflection is measure preserving; so V ∘ r_l and −V are two functions continuous on the open set R which agree a.e. there, hence agree pointwise there (MeasureTheory.Measure.eqOn_open_of_ae_eq).

Step 2: the piecewise globally odd representative #

Pointwise oddness on R is still not the binder (★)/(★★) want. But R is reflection invariant, so the piecewise function

  W := fun y => if y ∈ R then V y else O y

is odd about every met face globally: inside R the oddness is Step 1's, and outside R it is the a.e. datum's own pointwise oddness — the two cases never mix, precisely because r_l maps R onto R and its complement onto its complement. And W = V on R, so every quantity the odd-class apparatus reads (normalizedL2On, affineDistOn, affineExcessRaw, oddClassDefect, classical harmonicity on R, MemLp on R, the affine-minimizer datum on U₂ ⊆ R) is unchanged. No symmetrization, no reflection-group average and no new analytic input is needed.

1. Classical harmonicity is an `EqOn` invariant on an open set #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.harmonicOnNhd_congr_eqOn {d : ℕ} {S : Set (HCPolySupport.Vec d)} (hS : IsOpen S) {V W : HCPolySupport.Vec d → ℝ} (h : Set.EqOn W V S) (hV : InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' S)) :

InnerProductSpace.HarmonicOnNhd (W ∘ ⇑toEuc.symm) (⇑toEuc '' S)

Harmonicity transfers along an equality on an open set. Both sides are germs at each point of the set, and the set is open, so the germs agree.

2. From an almost-everywhere odd datum to oddness on the doubled window #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.eqOn_faceOdd_upper_of_ae_eq {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hup : MeetsUpperFace x m k i) {V O : HCPolySupport.Vec d → ℝ} (hVcont : ContinuousOn V (reflectedWindow x m k)) (hae : V =ᵐ[MeasureTheory.volume.restrict (reflectedWindow x m k)] O) (hOodd : ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -O z) (y : HCPolySupport.Vec d) :

y ∈ reflectedWindow x m k → V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i y) = -V y

The upper-face seam. A function continuous on the doubled window and almost everywhere equal there to a globally odd datum is pointwise odd about the met upper face at every point of the doubled window.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.eqOn_faceOdd_lower_of_ae_eq {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {i : Fin d} (hlow : MeetsLowerFace x m k i) {V O : HCPolySupport.Vec d → ℝ} (hVcont : ContinuousOn V (reflectedWindow x m k)) (hae : V =ᵐ[MeasureTheory.volume.restrict (reflectedWindow x m k)] O) (hOodd : ∀ (z : HCPolySupport.Vec d), O (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -O z) (y : HCPolySupport.Vec d) :

y ∈ reflectedWindow x m k → V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i y) = -V y

The lower-face seam, the twin of eqOn_faceOdd_upper_of_ae_eq.

3. The piecewise globally odd representative #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_faceOdd_forall_eqOn_reflectedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hkm : k < m) {V O : HCPolySupport.Vec d → ℝ} (hupV : ∀ (i : Fin d), MeetsUpperFace x m k i → ∀ y ∈ reflectedWindow x m k, V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i y) = -V y) (hlowV : ∀ (i : Fin d), MeetsLowerFace x m k i → ∀ y ∈ reflectedWindow x m k, V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i y) = -V y) (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) :

∃ (W : HCPolySupport.Vec d → ℝ), (∀ (i : Fin d), MeetsUpperFace x m k i → ∀ (z : HCPolySupport.Vec d), W (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -W z) ∧ (∀ (i : Fin d), MeetsLowerFace x m k i → ∀ (z : HCPolySupport.Vec d), W (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -W z) ∧ Set.EqOn W V (reflectedWindow x m k)

The seam, closed. From a representative V odd about every met face at the points of the doubled window and an a.e. datum O odd about every met face globally, the piecewise function W = V on the doubled window, = O off it, is odd about every met face globally and agrees with V on the doubled window.

The proof is the reflection invariance of the doubled window: a met-face reflection maps the window onto itself and its complement onto its complement, so the two branches of the if never mix.