SigmaBarProfile

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

The running diffusivity against the effective diffusivity profile

The running diffusivity σ_n of the coefficient cutoff at scale n lies within the relative distance C γ^{1/2} |log γ| of the effective diffusivity profile

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

for every scale n, with a constant C = C(d) c⋆^{-2}. This is the induction estimate for the running diffusivity of Section 3, read at a triadic scale through effectiveDiffusivity_three_zpow.

The amplitude γ^{1/2}|log γ| tends to 0 with γ, so the relative distance is at most 1/2 as soon as the disorder parameter lies below an explicit threshold. Both halves are packaged together here, which turns the two comparisons of LengthTimeScale between

  T(3^n) = 3^{2n} ν_eff(3^n)⁻¹    and    exitTimeScale M n = 3^{2n} σ_n⁻¹

into statements with no remaining premise beyond the threshold on γ.

Main results

• exists_sqrt_mul_abs_log_le — any multiple of the amplitude γ^{1/2}|log γ| is below any prescribed positive bound once γ is below an explicit threshold.
• exists_sigmaBar_close_to_effectiveDiffusivity — the relative bound between the running diffusivity and the profile, at every triadic scale, together with the smallness of its amplitude.
• exists_lengthTimeScale_conversions — the resulting comparison of the two time scales, with the explicit factors 2 and 3/2.

References

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

1. The disorder threshold

theorem Algsuperdiff.Section5.Support.exists_sqrt_mul_abs_log_le {K eps : ℝ} (hK : 0 < K) (heps : 0 < eps) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (gamma : ℝ), 0 < gamma → gamma ≤ gamma0 → K * (√gamma * |Real.log gamma|) ≤ eps

The amplitude γ^{1/2}|log γ| is uniformly small for small disorder. For every positive multiplier K and every prescribed positive bound eps there is a threshold below which K γ^{1/2}|log γ| ≤ eps.

The threshold is explicit: with A = max 1 (4 K / eps) it is A⁻⁴, because γ^{1/2}|log γ| ≤ 4 γ^{1/4}.

2. The running diffusivity against the profile

theorem Algsuperdiff.Section5.Support.exists_sigmaBar_close_to_effectiveDiffusivity (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → C * √M.gamma * |Real.log M.gamma| ≤ 1 / 2 ∧ ∀ (n : ℤ), |↑(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)

The running diffusivity is within a small relative distance of the effective diffusivity profile. For a fixed value c⋆ of the disorder strength there are a threshold γ₀ and a constant C such that every model with that disorder strength and with γ ≤ γ₀ satisfies both

  C γ^{1/2}|log γ| ≤ 1/2

and, at every triadic scale 3^n,

  |σ_n − ν_eff(3^n)| ≤ C γ^{1/2}|log γ| σ_n .

The constant is C = C(d) c⋆^{-2} and the threshold is the smaller of the disorder threshold of the induction estimate and the threshold that makes the amplitude at most 1/2.

3. The two time scales are comparable

theorem Algsuperdiff.Section5.Support.exists_lengthTimeScale_conversions (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (n : ℤ), 0 < lengthTimeScale M.nu cstar M.gamma (3 ^ n) ∧ lengthTimeScale M.nu cstar M.gamma (3 ^ n) ≤ 2 * exitTimeScale M n ∧ exitTimeScale M n ≤ 3 / 2 * lengthTimeScale M.nu cstar M.gamma (3 ^ n)

The time scale of the length scale 3^n and the running scale 3^{2n} σ_n⁻¹ are comparable, with no premise beyond a threshold on the disorder parameter. For a fixed value c⋆ of the disorder strength there is a threshold γ₀ such that every model with that disorder strength and with γ ≤ γ₀ satisfies, at every scale n,

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