AuxiliaryScale

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

The auxiliary scale of the displacement tail bound

The tail bound on the displacement compares the maximal scale m with an auxiliary scale n, chosen so that 3^n straddles

max{ν t / (δ 3^m), (c⋆ γ^{-1})^{1/2} (t / (δ 3^m))^{1/(1-γ)}},

and the chains-of-good-cubes estimate is then applied at that n. Its hypothesis n ≤ m - Y_m(ε) is exactly what the minimal-scale condition

min{3^{2m} / (ν t), (c⋆^{-1} γ)^{1/2} ((3^m)^{2-γ} / t)^{1/(1-γ)}} ≥ S_m

delivers, through the definition S_m = δ^{-1/(1-γ)} 3^{Y_m(ε)}.

The two halves of the comparison behave differently. On the first term the powers of δ do not cancel and the argument uses δ ≤ 1: what is left over is δ^{1 - 1/(1-γ)} ≥ 1, an inequality that fails for δ > 1. On the second term every factor cancels exactly — the powers of c⋆ and γ because the two expressions are reciprocal, the powers of δ because the exponent 1/(1-γ) is the same on both sides, and the powers of three because ((3^m)^{1-γ})^{1/(1-γ)} = 3^m. This is the bookkeeping that fixes the exponent -1/(1-γ) of δ in S_m.

Main definitions

• auxiliaryScaleBound nu cstar gamma delta t m — the quantity 3^n straddles.
• displacementMinScale nu cstar gamma t m — the left side of the minimal-scale condition.

References

• ABK26, the displacement tail bound of Section 5.3.

1. The two quantities

noncomputable def Algsuperdiff.Section5.Support.auxiliaryScaleBound (nu cstar gamma delta t : ℝ) (m : ℤ) : ℝ

The quantity the auxiliary scale straddles, max{ν t / (δ 3^m), (c⋆ γ^{-1})^{1/2} (t / (δ 3^m))^{1/(1-γ)}}.

Equations

• Algsuperdiff.Section5.Support.auxiliaryScaleBound nu cstar gamma delta t m = max (nu * t / (delta * 3 ^ m)) ((cstar * gamma⁻¹) ^ (1 / 2) * (t / (delta * 3 ^ m)) ^ (1 - gamma)⁻¹)

noncomputable def Algsuperdiff.Section5.Support.displacementMinScale (nu cstar gamma t : ℝ) (m : ℤ) : ℝ

The left side of the minimal-scale condition, min{3^{2m} / (ν t), (c⋆^{-1} γ)^{1/2} ((3^m)^{2-γ} / t)^{1/(1-γ)}}.

Equations

• Algsuperdiff.Section5.Support.displacementMinScale nu cstar gamma t m = min (3 ^ (2 * m) / (nu * t)) ((cstar⁻¹ * gamma) ^ (1 / 2) * ((3 ^ m) ^ (2 - gamma) / t) ^ (1 - gamma)⁻¹)

theorem Algsuperdiff.Section5.Support.auxiliaryScaleBound_pos {nu cstar gamma delta t : ℝ} (hnu : 0 < nu) (hdelta : 0 < delta) (ht : 0 < t) (m : ℤ) : 0 < auxiliaryScaleBound nu cstar gamma delta t m

2. The choice of the auxiliary scale

theorem Algsuperdiff.Section5.Support.exists_auxiliaryScale {v : ℝ} (hv : 0 < v) : ∃ (n : ℤ), 3 ^ n ≤ v ∧ v < 3 ^ (n + 1)

Every positive quantity is straddled by two consecutive powers of three. The base-three integer logarithm is such a scale, which is the choice the displacement tail bound makes.

3. The comparison with the scale of the chains estimate

theorem Algsuperdiff.Section5.Support.auxiliaryScale_le_sub_of_displacementScale_le {nu cstar gamma delta t : ℝ} {m : ℤ} {N : ℕ} {n : ℤ} (hnu : 0 < nu) (ht : 0 < t) (hdelta : 0 < delta) (hdelta1 : delta ≤ 1) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma < 1) (hn : 3 ^ n ≤ auxiliaryScaleBound nu cstar gamma delta t m) (hmin : displacementScale delta gamma N ≤ displacementMinScale nu cstar gamma t m) : n ≤ m - ↑N

The minimal-scale condition supplies the hypothesis of the chains estimate. If 3^n is below the straddled quantity and the scale S_m = δ^{-1/(1-γ)} 3^N is below the minimal-scale quantity, then n ≤ m - N.