OneStepCornerTransportFace

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

The one-met-face regime at the lower face

OneStepCornerTransport removed the orientation restriction from the corner pricing (★★). This module does the same for the one-met-face pricing (★) and its producer, which the proved OneStepEvenBoundFinal and the one-met-face producer state at a met upper face only.

What travels, and what the datum becomes

The negation σ_i carries a window meeting the lower i-face to one meeting the upper i-face, so (★) transports verbatim except for the affine datum, which is read at the reflected parameters: the normal slope oddAffineSlope i (σ_i A) = σ_i (oddAffineSlope i A) and the normal intercept

  oddAffineIntercept (σ_i x) m i (σ_i A) = A_i (x_i + ½·3^m) ,

the lower normal intercept oddAffineInterceptLower, whose ramp vanishes on the lower face exactly as oddAffineIntercept's vanishes on the upper one. With that datum the odd-class membership isOddAffineData_oddAffineDatumLower and the pricing exists_oddClassDefect_le_affineExcessRaw_lower are the mirror images of the proved upper-face statements, and the producer exists_gradientHolder_boundary_faceOdd_lower is the upper-face producer's proof run at those data.

1. The lower normal datum

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddAffineInterceptLower {d : ℕ} (x : HCPolySupport.Vec d) (m : ℤ) (i : Fin d) (A : HCPolySupport.Vec d) : ℝ

The intercept of the normal part of (c, A) at a met lower i-face: the ramp A_i (y_i + ½·3^m), which vanishes on that face.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddAffineInterceptLower x m i A = A i * (x i + 1 / 2 * 3 ^ m)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddAffineIntercept_comp_coordFaceReflection_zero {d : ℕ} (x : HCPolySupport.Vec d) (m : ℤ) (i : Fin d) (A : HCPolySupport.Vec d) : oddAffineIntercept (HCPolySupport.coordFaceReflection 0 i x) m i (HCPolySupport.coordFaceReflection 0 i A) = oddAffineInterceptLower x m i A

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.oddAffineSlope_comp_coordFaceReflection_zero {d : ℕ} (i : Fin d) (A : HCPolySupport.Vec d) : oddAffineSlope i (HCPolySupport.coordFaceReflection 0 i A) = HCPolySupport.coordFaceReflection 0 i (oddAffineSlope i A)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.isOddAffineData_oddAffineDatumLower {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {i : Fin d} (hkm : k < m) (hlow : MeetsLowerFace x m k i) (hother : ∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m k j ∧ ¬MeetsLowerFace x m k j) (A : HCPolySupport.Vec d) : IsOddAffineData x m k (oddAffineInterceptLower x m i A) (oddAffineSlope i A)

The lower normal datum lies in the odd affine class. The lower-face twin of OneStepDatumPriceOdd.isOddAffineData_oddAffineDatum.

2. The one-met-face pricing at the lower face

theorem Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.exists_oddClassDefect_le_affineExcessRaw_lower (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (m n : ℤ) (x : HCPolySupport.Vec d) (i : Fin d) (V : HCPolySupport.Vec d → ℝ) (c : ℝ) (A : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 2 < m → MeetsLowerFace x m (n - 2) i → (∀ (j : Fin d), j ≠ i → ¬MeetsUpperFace x m (n - 2) j ∧ ¬MeetsLowerFace x m (n - 2) j) → (∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) i 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 (oddAffineInterceptLower x m i A) (oddAffineSlope i A) ≤ C * Support.affineExcessRaw (truncatedWindow x m (n - 2)) V

(★) at a met lower face. The odd-class defect at the lower normal datum is priced by the excess.