SharpTailGrowth

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

From sharp shell rates to the quantitative growth budget

For an admissible ABK exponent, the all-crossover sharp bounds imply the two-leg partial-sum estimate used by the original field construction. The polynomial crossover weight is absorbed twice: geometrically in the shell gap and geometrically in the observation scale.

noncomputable def Algsuperdiff.Section5.Field.sharpSpatialRatio : ℝ

The fixed spatial decay ratio in the sharp stream-tail estimate.

Equations

• Algsuperdiff.Section5.Field.sharpSpatialRatio = Real.rpow 3 (-(3 / 4))

noncomputable def Algsuperdiff.Section5.Field.sharpLowerRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The low-frequency geometric ratio in the sharp stream-tail estimate.

Equations

• Algsuperdiff.Section5.Field.sharpLowerRatio M = Real.rpow 3 (-M.gamma)

noncomputable def Algsuperdiff.Section5.Field.sharpUpperRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The high-frequency geometric ratio in the sharp stream-tail estimate.

Equations

• Algsuperdiff.Section5.Field.sharpUpperRatio M = Real.rpow 3 (M.gamma - 1)

theorem Algsuperdiff.Section5.Field.exists_streamGrowthBounded_of_sharpTailGood {d : ℕ} (M : Section3.ABKModel d) {omega : Section3.Cutoff.CutoffSample d} (h : SharpTailGood M.gamma omega) : ∃ (C : ℕ), StreamGrowthBounded C omega

The sharp all-crossover bounds imply the original quantitative growth condition at every exponent admitted by an ABKModel.