StepSevenFlushLegBounds #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The pinned s-weights and the scalar helpers #
s^{-2} = 16 at the pin s = 1/4.
s^{-3} = 64 at the pin.
s^{-6} = 4096 at the pin.
s^{-7} = 16384 at the pin.
theorem
Algsuperdiff.Section4.Provider.Regularity.sqrt_rootClauseBTopKs_le_budget
{gamma alpha : ℝ}
{n j m : ℤ}
(hgamma0 : 0 ≤ gamma)
(h2gamma : 2 * gamma ≤ 1 - alpha)
(hnj : n ≤ j)
(hjm : j ≤ m)
:
The σ-bridge budget absorption. At the regime 2γ ≤ 1-α, the fine
σ-comparison factor is inside the quarter budget: √(rootClauseBTopKs γ m j) ≤ 2·3^{(1/4)(1-α)(m-n)} for n ≤ j ≤ m.
2. The ∇h flat and coordinate legs, by the printed sup binder #
theorem
Algsuperdiff.Section4.Provider.Regularity.eLpNorm_grad_window_le_sup
{d : ℕ}
{m j : ℤ}
{z : HCPolySupport.Vec d}
{Kh : ℝ}
(hKh : 0 ≤ Kh)
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(hsup : ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh)
:
(MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m j))).toReal ≤ Real.rpow 3 (↑m / 2) * Kh
theorem
Algsuperdiff.Section4.Provider.Regularity.eLpNorm_grad_coord_window_le_sup
{d : ℕ}
{m j : ℤ}
{z : HCPolySupport.Vec d}
{Kh : ℝ}
(hKh : 0 ≤ Kh)
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(hsup : ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh)
(i : Fin d)
:
(MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => hdat.grad y i) 2
(Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m j))).toReal ≤ Real.rpow 3 (↑m / 2) * Kh
theorem
Algsuperdiff.Section4.Provider.Regularity.sum_eLpNorm_grad_coord_window_le_sup
{d : ℕ}
{m j : ℤ}
{z : HCPolySupport.Vec d}
{Kh : ℝ}
(hKh : 0 ≤ Kh)
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(hsup : ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖hdat.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh)
:
∑ i : Fin d,
(MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => hdat.grad y i) 2
(Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m j))).toReal ≤ ↑d * (Real.rpow 3 (↑m / 2) * Kh)
3. The two Gagliardo legs, by the C^{0,1/2} data #
theorem
Algsuperdiff.Section4.Provider.Regularity.gagliardo_window_toReal_le
{d : ℕ}
{m j : ℤ}
{z : HCPolySupport.Vec d}
{Kf : ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
(hd : 1 ≤ d)
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(hKf : 0 ≤ Kf)
(hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kf f)
:
(Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow z m j) stepOneS f).toReal ≤ Kf * stepFourGagliardoConst d stepOneS * 3 ^ (↑j / 4)
A Gagliardo window leg at the pin, toReal form. The Step-4 comparison at
s = stepOneS = 1/4 on the truncated window.
4. The oscillation bridge #
theorem
Algsuperdiff.Section4.Provider.Regularity.oscE_toReal_eq_normalizedL2On
{d : ℕ}
{m j : ℤ}
{z : HCPolySupport.Vec d}
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
(uglob : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(c : ℝ)
:
(MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => uglob.toFun y - c) 2
(Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow z m j))).toReal = Support.normalizedL2On (ExcessDecay.truncatedWindow z m j) fun (y : HCPolySupport.Vec d) => uglob.toFun y - c
The window oscillation's carrier bridge: the anchor-side eLpNorm reading
IS the boundary lane's ‖·‖_{L²} reading.