OneStepOddClassCornerRamp #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Corner pricing: the normal ramp and the residual fold #
The L² bookkeeping of the corner absorption, split off from the assembly
for elaboration budget:
abs_slope_mul_delta_le— the box-moment lower bound: the normal rampoddᵢ = Aᵢ(yᵢ − a)satisfies|Aᵢ|·delta ≤ 7t·‖oddᵢ‖_{L²(U₂)}at depthdelta = t·3^{n−2}, because the window'si-edge exceeds half the triadic side and the sharp moment identity gives‖oddᵢ‖ ≥ |Aᵢ|·edge/√12.normalizedL2On_oddRamp_cornerPairSlab_le/..._cornerPairSlabPushed_le— on the corner slab (and its inwardj-translate) the ramp is pointwise at most|Aᵢ|·delta.normalizedL2On_reflected_residual_le— the fold: the residualV − ℓon the doubled window is priced by(2^d + Crefl)·(E + P), via the full-met-set odd fold of the competitor and the affine moment comparison of the doubled window against the window.
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.abs_slope_mul_delta_le
{d : ℕ}
{m n : ℤ}
{x : HCPolySupport.Vec d}
{i : Fin d}
{A : HCPolySupport.Vec d}
{tt delta : ℝ}
(hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hmn : n - 2 < m)
(htt0 : 0 < tt)
(hdeltadef : delta = tt * 3 ^ (n - 2))
:
|A i| * delta ≤ 7 * tt * Support.normalizedL2On (truncatedWindow x m (n - 2)) (oddAffinePart x m i A)
The moment lower bound for the normal ramp:
|Aᵢ|·delta ≤ 7t·‖oddᵢ‖_{L²(U₂)} at delta = t·3^{n−2}.
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_oddRamp_cornerPairSlab_le
{d : ℕ}
{m k : ℤ}
{x : HCPolySupport.Vec d}
{i j : Fin d}
{A : HCPolySupport.Vec d}
{delta : ℝ}
(hdelta0 : 0 < delta)
(hQpos : 0 < (MeasureTheory.volume (coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j))).toReal)
:
Support.normalizedL2On (coordBox (cornerPairSlabLo x m k i j delta) (cornerPairSlabHi x m k i j))
(oddAffinePart x m i A) ≤ |A i| * delta
The ramp on the corner slab is pointwise small:
‖oddᵢ‖_{L²(Q)} ≤ |Aᵢ|·delta.
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_oddRamp_cornerPairSlabPushed_le
{d : ℕ}
{m k : ℤ}
{x : HCPolySupport.Vec d}
{i j : Fin d}
{A : HCPolySupport.Vec d}
{delta : ℝ}
(hij : i ≠ j)
(hdelta0 : 0 < delta)
(hD3pos :
0 < (MeasureTheory.volume
(coordBox (fun (l : Fin d) => cornerPairSlabLo x m k i j delta l - (delta • HCPolySupport.basisVec j) l)
fun (l : Fin d) => cornerPairSlabHi x m k i j l - (delta • HCPolySupport.basisVec j) l)).toReal)
:
Support.normalizedL2On
(coordBox (fun (l : Fin d) => cornerPairSlabLo x m k i j delta l - (delta • HCPolySupport.basisVec j) l)
fun (l : Fin d) => cornerPairSlabHi x m k i j l - (delta • HCPolySupport.basisVec j) l)
(oddAffinePart x m i A) ≤ |A i| * delta
The ramp on the j-pushed corner slab is pointwise small.
theorem
Algsuperdiff.Section4.Provider.ExcessDecay.Schauder.normalizedL2On_reflected_residual_le
{d : ℕ}
{m n : ℤ}
{x : HCPolySupport.Vec d}
{V : HCPolySupport.Vec d → ℝ}
{c : ℝ}
{A : HCPolySupport.Vec d}
(hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hmn : n - 2 < m)
(hupV :
∀ (l : Fin d),
MeetsUpperFace x m (n - 2) l →
∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l z) = -V z)
(hlowV :
∀ (l : Fin d),
MeetsLowerFace x m (n - 2) l →
∀ (z : HCPolySupport.Vec d), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l z) = -V z)
(hVR : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))))
:
(Support.normalizedL2On (reflectedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) =>
V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) ≤ (2 ^ d + √((24 * ↑d + 1) * 2 ^ 2 + 2)) * ((Support.normalizedL2On (truncatedWindow x m (n - 2)) fun (y : HCPolySupport.Vec d) =>
V y - Support.affineEval (c - HCPolySupport.vecDot A x) A y) + Support.normalizedL2On (truncatedWindow x m (n - 2)) (Support.affineEval (c - HCPolySupport.vecDot A x) A))
The fold of the residual onto the window:
‖V − ℓ‖_{L²(R)} ≤ (2^d + Crefl)(E + P) for a competitor odd under every met
reflection.