StepFiveDeltaFamily

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

t.regularity Step 5: the concrete δ_j family

The target

ABK26 t.regularity Step 5, — the δ_j slot of the iteration lemma at the Step-5 instantiation:

  δ_j := C 3^{j/2} σ_j^{-1} [g]_{W^{1/2,∞}(□_m)}
         + C ( 3^{j/2} [∇h]_{W^{1/2,∞}(□_m)}
               + ε_j ‖∇h‖_{L^∞(□_m)} ) 1_{z ∉ □_{m-1}} .

The ℝ≥0∞ → ℝ layer, and where toReal's convention is load-bearing

[·]_{W^{1/2,∞}(□_m)} is an ℝ≥0∞-valued essential supremum, while l.iteration.lemma demands δ: ℤ → ℝ. The junk value (⊤).toReal = 0 is therefore in play, and its status is settled here once and for all:

• Guarded (inert) in everything this tree proves. Every inequality of this module and of StepFiveDeltaSum carries the SAME toReal atoms on both sides — the family is bounded above by an expression built from its own seminorm values. A ⊤ seminorm makes both sides 0; no statement becomes false, and no statement becomes vacuous.
• Nor is that corner waved at: the root anchor already types the three cube-level data of δ_j by real scalars,

  Support.HolderSeminormBoundOn (openCubeSet (originCube d m)) (1 / 2) Kg g
  Support.HolderSeminormBoundOn (openCubeSet (originCube d m)) (1 / 2) Kh h.grad
  ∀ x ∈ openCubeSet (originCube d m), ‖h.grad x‖ ≤ KhInf

so the finiteness the toReal layer needs is data the roots already carry; nothing new is assumed.

Readings of the printed list

• D3 (the ε inside δ_j). The manuscript's Step-5 list sets ε_j:= C ε_j(z) and then writes δ_j's boundary leg as C (… + ε_j ‖∇h‖_{L^∞}) 1, i.e. C² ε_j(z) ‖∇h‖_{L^∞} 1. The proved tree pins the iteration lemma's ε slot at the ε_j(z) (e.sum.eps.j.bound is proved at C = 1), so the family below reads C ε_j(z) ‖∇h‖_{L^∞} 1. The two differ by one factor of the generic C = C(d,c⋆).

References

• ABK26, t.regularity Step 5.

1. The two geometric ratios

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioG {d : ℕ} (M : Section3.ABKModel d) : ℝ

The geometric ratio for the gradient contribution in the fifth regularity step.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioG M = 3 ^ (-(1 / 2 - M.gamma))

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioH : ℝ

r₂ := 3^{-1/2}, the geometric ratio of δ_j's ∇h-leg.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioH = 3 ^ (-(1 / 2))

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioG_pos {d : ℕ} (M : Section3.ABKModel d) : 0 < stepFiveRatioG M

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioG_lt_one {d : ℕ} {M : Section3.ABKModel d} (hgamma : M.gamma < 1 / 2) : stepFiveRatioG M < 1

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioH_pos : 0 < stepFiveRatioH

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveRatioH_lt_one : stepFiveRatioH < 1

theorem Algsuperdiff.Section4.Provider.Regularity.three_rpow_half_eq_mul_ratioH_zpow (m j : ℤ) : 3 ^ (↑j / 2) = 3 ^ (↑m / 2) * stepFiveRatioH ^ (m - j)

The exact scale identity behind the ∇h-leg's domination: 3^{j/2} = 3^{m/2} · (3^{-1/2})^{m-j}, with the (m-j)-power an integer power of the fixed ratio — the shape StepFiveGeometricTail sums.