LocalizationOscillationBudget

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

The gamma^{15} budget of e.lower.bound.oscillations

ABK26, l.approximate.recurrence.formula, e.lower.bound.oscillations. The printed chain ends

  ... <= C 3^{-(m-h-n)} + C shom_{m-h}^{-1} 3^{-(m-h-n)} 3^{cgamma(m-h)} cgamma^{-1}
         + C 3^{-(K-m+h)/4}  <=  cgamma^{15} .

LocalizationOscillationDisplay.lean proves the first inequality of that chain, in the sharper form that carries the buffer gap N = m - h - n instead of cgamma^{-1} and has no boundary term (the interior grid carries none). This module proves the second inequality: at the corrected buffer the three surviving terms fall below cgamma^{15} once cgamma is below an explicit threshold.

Everything here is arithmetic over abstract reals or about the two scale functions of LocalizationParams; no field, no measure and no corrector appears.

Main results

• rpow_three_neg_recurrenceGap_le_gamma_pow -- the gap factor at the full gap: 3^{-a ceil|log_3 gamma|} <= gamma^a. (LocalizationParams states the quarter-gap form, which is what Step 3 consumes; Step 2's oscillation display consumes the full gap.)
• recurrenceGap_mul_gamma_le -- the log-loss bound N gamma <= 3a.
• sigmaBarInv_mul_rpow_gamma_shell_le -- the normalization shom_{m-h}^{-1} 3^{cgamma (m-h)} <= sqrt(24 . 3^18), from the deterministic head Corrector.inv_sigmaBarSq_mul_shellWidth_le and h >= 1.

The gap factor at the full gap

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rpow_three_neg_recurrenceGap_le_gamma_pow (a : ℕ) {gamma : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) : 3 ^ (-↑(recurrenceGap a gamma)) ≤ gamma ^ a

The gap factor at the full corrected gap. For every multiplier a, 3^{-a ceil|log_3 gamma|} <= gamma^a on 0 < gamma <= 1. This is the quarter-gap gate of LocalizationParams raised to the fourth power.: on hgamma0, hgamma1.

The log-loss bound

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGap_mul_gamma_le (a : ℕ) {gamma : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) : ↑(recurrenceGap a gamma) * gamma ≤ 3 * ↑a

The corrected gap loses only one power of gamma. a ceil|log_3 gamma| . gamma <= 3a on 0 < gamma <= 1. The route is the coverage estimate ceil|log_3 gamma| <= 2 sqrt(gamma^{-1}) + 1 of LocalizationParams together with gamma sqrt(gamma^{-1}) <= 1.: on hgamma0, hgamma1.

The shell normalization

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellNormalizationConst : ℝ

The absolute constant of the shell normalization: sqrt(24 . 3^18).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellNormalizationConst = √(24 * 3 ^ 18)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.shellNormalizationConst_nonneg : 0 ≤ shellNormalizationConst

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sigmaBarInv_mul_rpow_gamma_shell_le {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {m : ℤ} {h : ℕ} (hhpos : 0 < h) (hm : m - ↑h ≤ m0) (hh : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) : (↑(Annealed.sigmaBar M (m - ↑h)))⁻¹ * 3 ^ (M.gamma * ↑(m - ↑h)) ≤ shellNormalizationConst

shom_{m-h}^{-1} 3^{cgamma (m-h)} <= sqrt(24 . 3^18).

This is the deterministic head Corrector.inv_sigmaBarSq_mul_shellWidth_le (which reads shom_{m-h}^{-2} h 3^{2 cgamma m} <= 24 . 3^18) used at h >= 1 and at m - h <= m. It is the normalization the second and third terms of e.lower.bound.oscillations consume.

: on the induction state hS and the three source gates hhpos : 0 < h, hm : m - h <= m0, hh : h <= 6 cstar cgamma^{-1}.