OneStepCornerTransport

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

The odd-class pricing at every met orientation

The proved odd-class apparatus is stated at upper met faces: (★) (OneStepEvenBoundFinal.exists_oddClassDefect_le_affineExcessRaw) at one met upper face, (★★) (OneStepOddClassCornerFinal.exists_oddClassDefect_le_affineExcessRaw_corner) at a pair of met upper faces. The covering the excess-decay consumption runs over meets lower and mixed configurations too. This module removes the orientation restriction, by transport rather than by duplication.

The transport

The domain cube □_m is origin-symmetric, so the coordinate negation σ_l = coordFaceReflection (0 : ℝ) l is a linear isometric involution of the ambient space carrying

  (x + □_k) ∩ □_m  ↦  (σ_l x + □_k) ∩ □_m ,

exchanging the upper and lower l-faces and fixing every other face (OneStepCornerTransportGeom). Every quantity the odd-class apparatus reads is invariant: normalizedL2On, affineDistOn, affineExcessRaw, affineExcess, IsAffineMinimizer, MemLp (OneStepCornerTransportNorms), classical harmonicity (OneStepCornerTransportHarmonic), the met-face oddness binders and IsOddAffineData (§1--§2 here) and hence oddClassDefect (§3 here).

So a window meeting a lower l-face is carried by one negation to a window meeting the upper l-face, and a corner in an arbitrary orientation is carried by at most two negations to an upper-upper corner. §4 and §5 run those negations.

1. The met-face oddness binders under a coordinate negation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordFaceReflection_zero_comm_self {d : ℕ} (a : ℝ) (l : Fin d) (y : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection 0 l (HCPolySupport.coordFaceReflection a l y) = HCPolySupport.coordFaceReflection (-a) l (HCPolySupport.coordFaceReflection 0 l y)

A coordinate negation turns the reflection in the upper l-face into the reflection in the lower l-face.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordFaceReflection_zero_zero {d : ℕ} (l : Fin d) : HCPolySupport.coordFaceReflection 0 l 0 = 0

The negation fixes the origin.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.coordFaceReflection_zero_sub {d : ℕ} (l : Fin d) (u v : HCPolySupport.Vec d) : HCPolySupport.coordFaceReflection 0 l (u - v) = HCPolySupport.coordFaceReflection 0 l u - HCPolySupport.coordFaceReflection 0 l v

The negation of a difference.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.faceOddUpper_comp_coordFaceReflection_zero {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (l : Fin d) {V : HCPolySupport.Vec d → ℝ} (hupV : ∀ (i : Fin d), MeetsUpperFace x m k i → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) (hlowV : ∀ (i : Fin d), MeetsLowerFace x m k i → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -V z) (i : Fin d) (hi : MeetsUpperFace (HCPolySupport.coordFaceReflection 0 l x) m k i) (z : HCPolySupport.Vec d) : V (HCPolySupport.coordFaceReflection 0 l (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z)) = -V (HCPolySupport.coordFaceReflection 0 l z)

Upper-face oddness travels. If V is odd about every met face of the window at x, then V ∘ σ_l is odd about every met upper face of the window at σ_l x.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.faceOddLower_comp_coordFaceReflection_zero {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (l : Fin d) {V : HCPolySupport.Vec d → ℝ} (hupV : ∀ (i : Fin d), MeetsUpperFace x m k i → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) i z) = -V z) (hlowV : ∀ (i : Fin d), MeetsLowerFace x m k i → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z) = -V z) (i : Fin d) (hi : MeetsLowerFace (HCPolySupport.coordFaceReflection 0 l x) m k i) (z : HCPolySupport.Vec d) : V (HCPolySupport.coordFaceReflection 0 l (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i z)) = -V (HCPolySupport.coordFaceReflection 0 l z)

Lower-face oddness travels, the twin of faceOddUpper_comp_coordFaceReflection_zero.

2. The odd affine class under a coordinate negation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.affineLift_comp_coordFaceReflection_zero {d : ℕ} (x : HCPolySupport.Vec d) (c : ℝ) (A : HCPolySupport.Vec d) (l : Fin d) (y : HCPolySupport.Vec d) : affineLift (HCPolySupport.coordFaceReflection 0 l x) c (HCPolySupport.coordFaceReflection 0 l A) y = affineLift x c A (HCPolySupport.coordFaceReflection 0 l y)

The affine lift travels with the negation.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.isOddAffineData_of_comp_coordFaceReflection_zero {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (l : Fin d) {c : ℝ} {A : HCPolySupport.Vec d} (h : IsOddAffineData (HCPolySupport.coordFaceReflection 0 l x) m k c (HCPolySupport.coordFaceReflection 0 l A)) : IsOddAffineData x m k c A

The odd affine class travels. A datum odd for the negated window is odd for the original one.

3. The window quantities under a coordinate negation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.affineExcessRaw_truncatedWindow_comp_coordFaceReflection_zero {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) (l : Fin d) (V : HCPolySupport.Vec d → ℝ) : (Support.affineExcessRaw (truncatedWindow (HCPolySupport.coordFaceReflection 0 l x) m k) fun (y : HCPolySupport.Vec d) => V (HCPolySupport.coordFaceReflection 0 l y)) = Support.affineExcessRaw (truncatedWindow x m k) V

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.vecDot_coordFaceReflection_zero_pair {d : ℕ} (l : Fin d) (A x : HCPolySupport.Vec d) : HCPolySupport.vecDot (HCPolySupport.coordFaceReflection 0 l A) (HCPolySupport.coordFaceReflection 0 l x) = HCPolySupport.vecDot A x

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.isAffineMinimizer_truncatedWindow_comp_coordFaceReflection_zero {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (l : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d) : Support.IsAffineMinimizer (truncatedWindow (HCPolySupport.coordFaceReflection 0 l x) m k) (fun (y : HCPolySupport.Vec d) => V (HCPolySupport.coordFaceReflection 0 l y)) (c - HCPolySupport.vecDot (HCPolySupport.coordFaceReflection 0 l A) (HCPolySupport.coordFaceReflection 0 l x)) (HCPolySupport.coordFaceReflection 0 l A) ↔ Support.IsAffineMinimizer (truncatedWindow x m k) V (c - HCPolySupport.vecDot A x) A

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddClassDefect_comp_coordFaceReflection_zero {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) (l : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d) : oddClassDefect (HCPolySupport.coordFaceReflection 0 l x) m n (fun (y : HCPolySupport.Vec d) => V (HCPolySupport.coordFaceReflection 0 l y)) c (HCPolySupport.coordFaceReflection 0 l A) = oddClassDefect x m n V c A

4. The corner pricing at every orientation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_oddClassDefect_le_affineExcessRaw_corner_any (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i j : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → i ≠ j → MeetsUpperFace x m (n - 2) i ∨ MeetsLowerFace x m (n - 2) i → MeetsUpperFace x m (n - 2) j ∨ MeetsLowerFace x m (n - 2) j → (∀ (l : Fin d), MeetsUpperFace x m (n - 2) l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l z) = -V z) → (∀ (l : Fin d), MeetsLowerFace x m (n - 2) l → ∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l z) = -V z) → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑toEuc.symm) (⇑toEuc '' reflectedWindow x m (n - 2)) → MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))) → Support.IsAffineMinimizer (truncatedWindow x m (n - 2)) V (c - HCPolySupport.vecDot A x) A → oddClassDefect x m n V 0 0 ≤ C * Support.affineExcessRaw (truncatedWindow x m (n - 2)) V

(★★) at every met orientation. The corner pricing with the upper-upper restriction removed: the two distinguished met faces may be upper or lower in any combination (the remaining met faces are arbitrary, as in the proved statement).