LengthTimeScale

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

The time scale of a length scale

The time scale attached to a length scale r is

  T(r) = r² ν_eff(r)⁻¹ ,      ν_eff(r) = (ν² + c⋆ γ⁻¹ r^{2γ})^{1/2} ,

and it is the quantity in which the exit-time estimates of Section 5.2 are written. The exit-time comparison is proved at the running scale exitTimeScale M n = 3^{2n} σ_n⁻¹, where σ_n is the running diffusivity of the coefficient cutoff at scale n.

The two scales agree up to a factor 1 ± C γ^{1/2} |log γ|, because the running diffusivity is within that relative distance of the profile ν_eff(3^n). This file defines T(r) and converts that relative distance into the two explicit inequalities

  T(3^n) ≤ 2 · exitTimeScale M n ,     exitTimeScale M n ≤ (3/2) · T(3^n) ,

which hold as soon as the relative distance is at most 1/2.

The relative distance is a hypothesis of every statement below, so that this file depends on nothing but the two scales it compares. It is a theorem: it is the second conclusion of Algsuperdiff.Frozen.Section3.induction_bounds, read at a triadic scale, and Algsuperdiff.Section5.Support.SigmaBarProfile discharges it there in exists_sigmaBar_close_to_effectiveDiffusivity, together with the smallness of its amplitude. The premise-free forms of the two conversions below are exists_lengthTimeScale_conversions in that module.

Main definitions

• lengthTimeScale nu cstar gamma r — the time scale T(r) = r² ν_eff(r)⁻¹.

Main results

• lengthTimeScale_le_two_mul_exitTimeScale and exitTimeScale_le_three_halves_mul_lengthTimeScale — the two conversions.
• lengthTimeScale_pos_of_profile — positivity of T(3^n) under the same premise.

References

• ABK26, the time scale of a length scale in Section 5.3, and the induction bounds for the running diffusivity of Section 3.

1. The time scale

noncomputable def Algsuperdiff.Section5.Support.lengthTimeScale (nu cstar gamma r : ℝ) : ℝ

The time scale attached to a length scale, T(r) = r² ν_eff(r)⁻¹.

Equations

• Algsuperdiff.Section5.Support.lengthTimeScale nu cstar gamma r = r ^ 2 / Algsuperdiff.Section5.Support.effectiveDiffusivity nu cstar gamma r

2. The elementary comparison

3. The conversion at a triadic scale

theorem Algsuperdiff.Section5.Support.lengthTimeScale_pos_of_profile {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {cstar C : ℝ} (hsmall : C * √M.gamma * |Real.log M.gamma| ≤ 1 / 2) (hprofile : |↑(Section3.Annealed.sigmaBar M n) - effectiveDiffusivity M.nu cstar M.gamma (3 ^ n)| ≤ C * √M.gamma * |Real.log M.gamma| * ↑(Section3.Annealed.sigmaBar M n)) : 0 < lengthTimeScale M.nu cstar M.gamma (3 ^ n)

The time scale of the length scale 3^n is positive.

theorem Algsuperdiff.Section5.Support.lengthTimeScale_le_two_mul_exitTimeScale {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {cstar C : ℝ} (hsmall : C * √M.gamma * |Real.log M.gamma| ≤ 1 / 2) (hprofile : |↑(Section3.Annealed.sigmaBar M n) - effectiveDiffusivity M.nu cstar M.gamma (3 ^ n)| ≤ C * √M.gamma * |Real.log M.gamma| * ↑(Section3.Annealed.sigmaBar M n)) : lengthTimeScale M.nu cstar M.gamma (3 ^ n) ≤ 2 * exitTimeScale M n

The time scale of the length scale 3^n is at most twice the running scale 3^{2n} σ_n⁻¹.

theorem Algsuperdiff.Section5.Support.exitTimeScale_le_three_halves_mul_lengthTimeScale {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {cstar C : ℝ} (hsmall : C * √M.gamma * |Real.log M.gamma| ≤ 1 / 2) (hprofile : |↑(Section3.Annealed.sigmaBar M n) - effectiveDiffusivity M.nu cstar M.gamma (3 ^ n)| ≤ C * √M.gamma * |Real.log M.gamma| * ↑(Section3.Annealed.sigmaBar M n)) : exitTimeScale M n ≤ 3 / 2 * lengthTimeScale M.nu cstar M.gamma (3 ^ n)

The running scale 3^{2n} σ_n⁻¹ is at most three halves of the time scale of the length scale 3^n.