KickingAssembly

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

e.good.scale.kicking: the assembly

ABK26, §4.2. KickingLemma.lean supplies the bridges, the finiteness and the ℝ≥0∞ → ℝ conversion; this module performs the three-term addition of l.minimal.scale.sep and states the lemma.

• exists_cesaro_dTwo_bound — e.D2k.kicked read at the D-decomposition's own D₂ and at the lemma's envelopes (s^{−7/2} deterministic, s^{−9/2} fluctuation).
• exists_cesaro_dThree_bound — the same for D₃, with stepThree_det_closed / stepThree_fluc_closed supplying the two closed s-powers.
• exists_goodScaleKicking — the kicking lemma.

The three Γ₂ fluctuations are added by isBigO_gammaSigma_add3 (l.Gamma.sigma.triangle, three-term form) at the constant (1 + log 3)^{1/2} ≤ 2 (triangleConstThree_le), which is the manuscript's "adding the previous three displays".

The single output constant

C = C_dec + C_end + C_dec·(C_end + 2·stepTwoDetConst + 2·stepThreeDetConst d + 1) + C_dec·2·(C_end + 2·stepTwoConst + 2·stepThreeFlucConst d),

a function of d alone: C_dec is the D-decomposition's constant, C_end the D₁ endpoint's, and the four Step-2/Step-3 constants are the proved absolute / dimensional ones. It dominates C_dec and C_end so that the lemma's own regime clause passes down to both inputs, and the factors 2 are the two prefactor conversions (c⋆^{−1/2} ≤ 2c⋆^{−1} and the triangle constant).

References

• ABK26, l.minimal.scale.sep; l.Gamma.sigma.triangle.

1. The D₂ Cesàro bound at the lemma's envelopes

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_cesaro_dTwo_bound {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (hs1 : ↑s ≤ 1) {n m : ℤ} (hnm : n < m) : ∃ (Xdet : Section3.Cutoff.CutoffSample d → ℝ) (Xfluc : Section3.Cutoff.CutoffSample d → ℝ), (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Probability.cesaroAvg (fun (k : ℤ) => (dTwo M s k omega).toReal) n m ≤ Xdet omega + Xfluc omega) ∧ (∀ (omega : Section3.Cutoff.CutoffSample d), Xdet omega ≤ 2 * stepTwoDetConst * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)) ∧ HCPolySupport.IndependentSums.IsBigO (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (2 * stepTwoConst * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma) * ↑(m - n) ^ (-1 / 2))

e.D2k.kicked at the D-decomposition's own D₂. The Cesàro average of D₂ over the window splits into a deterministic level below 2·stepTwoDetConst·c⋆^{−1}s^{−7/2}√γ and a Γ₂ fluctuation of scale 2·stepTwoConst·c⋆^{−1}s^{−9/2}√γ(m−n)^{−1/2}. Both readings pay the single absolute factor 2 of sqrt_cstar_inv_le.

2. The D₃ Cesàro bound at the lemma's envelopes

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_cesaro_dThree_bound {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (hs2 : ↑s ≤ 1 / 2) {n m : ℤ} (hnm : n < m) : ∃ (Xdet : Section3.Cutoff.CutoffSample d → ℝ) (Xfluc : Section3.Cutoff.CutoffSample d → ℝ), (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Probability.cesaroAvg (fun (k : ℤ) => (dThree M s k omega).toReal) n m ≤ Xdet omega + Xfluc omega) ∧ (∀ (omega : Section3.Cutoff.CutoffSample d), Xdet omega ≤ 2 * stepThreeDetConst d * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)) ∧ HCPolySupport.IndependentSums.IsBigO (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (2 * stepThreeFlucConst d * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma) * ↑(m - n) ^ (-1 / 2))

The almost-sure convergence of that channel is proved, not assumed.

3. The kicking lemma

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_goodScaleKicking (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≤ ↑s → ↑s ≤ 1 / 4 → ∀ (n m : ℤ), n < m → ∃ (Xdet : Section3.Cutoff.CutoffSample d → ℝ) (Xfluc : Section3.Cutoff.CutoffSample d → ℝ), (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m, (Support.goodEventBase M (Support.cgEllipLowerConstant d) k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ ENNReal.ofReal (Xdet omega + Xfluc omega)) ∧ (∀ (omega : Section3.Cutoff.CutoffSample d), Xdet omega ≤ C * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)) ∧ HCPolySupport.IndependentSums.IsBigO (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (C * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma) * ↑(m - n) ^ (-1 / 2))

l.minimal.scale.sep / e.good.scale.kicking.

There is a dimensional constant C such that, in the printed regime γ ≤ C^{−10}c⋆^{10} and on the window s ∈ [8γ, 1/4], for every window [n, m] with n < m,

avsum_{k=n}^m sup_{L ≥ k} 𝓔_{s,∞,2}(□_k; a_L − (k_L − k_k)_{□_k}, σ_k) 1_{𝒢(k;s,1)}
  ≤ C c⋆^{−1}s^{−7/2}√γ + 𝒪_{Γ₂}( C c⋆^{−1}s^{−9/2}√γ (m−n)^{−1/2} ) ,

the left side being the frozen statement's own ℝ≥0∞ window average at the origin centre and the additive 𝒪_{Γ₂} being unfolded into the explicit ∃ Xdet Xfluc split (the reading the proved apparatus consumes).

s^{−7/2} = ((√s)⁷)⁻¹ and s^{−9/2} = ((√s)⁹)⁻¹, so no rpow appears in either envelope.