IntrinsicScale

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

The intrinsic length scale, the effective diffusivity, and the scale arithmetic

The superdiffusive displacement bounds are stated in terms of the length scale

R(t) = ((ν t)^{2-γ} + c⋆ γ^{-1} t²)^{1/(2(2-γ))}

associated with a time t, and are proved at a scale 3^m above it. The comparison that carries the proof from the time variable to the scale variable is between R(t)² and σ_m t, where σ_m is the effective diffusivity at scale 3^m. This file proves that comparison.

The deterministic profile of the effective diffusivity is

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

and the argument has two halves. The first is exact and needs no smallness at all: whenever R(t) ≤ r,

|R(t)² - ν_eff(r) t| ≤ γ r².

Two elementary facts drive it. The defining identity of R(t), multiplied by R(t)^{2γ}, gives the exact gap

R(t)⁴ - (ν_eff(R(t)) t)² = R(t)^{2γ} (ν t)^{2-γ} - (ν t)²,

and that gap is between 0 and γ R(t)⁴ because ν t ≤ R(t)² and because u^γ - 1 ≤ γ u² for every u ≥ 1. The same inequality u^γ - 1 ≤ γ u², applied to u = r / R(t), is what lets the scale r be arbitrarily far above R(t) at the cost of the factor r² on the right.

The second half replaces ν_eff(3^m) by the effective diffusivity σ_m of the renormalization theorem, which is within a relative error C γ^{1/2} |log γ| of the profile. Since γ ≤ γ^{1/2} |log γ| throughout the admissible range of γ, the two halves combine into

|R(t)² - σ_m t| ≤ (1 + 2C) γ^{1/2} |log γ| 3^{2m},

which is the displayed comparison, with the constant made explicit.

Main definitions

• intrinsicScale — the length scale R(t).
• effectiveDiffusivity — the profile ν_eff(r).

Main results

• mul_le_intrinsicScale_sq — ν t ≤ R(t)².
• abs_intrinsicScale_sq_sub_effectiveDiffusivity_mul_le — the exact half, |R(t)² - ν_eff(r) t| ≤ γ r² for every r ≥ R(t).
• effectiveDiffusivity_mul_le_sq — ν_eff(r) t ≤ r², the same statement read as a comparison of the time t with the time scale of r.
• abs_intrinsicScale_sq_sub_mul_le — the displayed comparison with the effective diffusivity of the renormalization theorem in place of the profile.
• effectiveDiffusivity_three_zpow — the profile at a triadic scale, in the form in which the renormalization theorem states it.

References

• ABK26, the superdiffusive displacement bounds of Section 5.4.

1. The two length-scale profiles

noncomputable def Algsuperdiff.Section5.Support.intrinsicScale (nu cstar gamma t : ℝ) : ℝ

The intrinsic length scale associated with a time t, R(t) = ((ν t)^{2-γ} + c⋆ γ^{-1} t²)^{1/(2(2-γ))}.

Equations

• Algsuperdiff.Section5.Support.intrinsicScale nu cstar gamma t = ((nu * t) ^ (2 - gamma) + cstar * gamma⁻¹ * t ^ 2) ^ (2 * (2 - gamma))⁻¹

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

The effective diffusivity profile at a length scale r, ν_eff(r) = (ν² + c⋆ γ^{-1} r^{2γ})^{1/2}.

Equations

• Algsuperdiff.Section5.Support.effectiveDiffusivity nu cstar gamma r = √(nu ^ 2 + cstar * gamma⁻¹ * r ^ (2 * gamma))

theorem Algsuperdiff.Section5.Support.effectiveDiffusivity_three_zpow (nu cstar gamma : ℝ) (m : ℤ) : effectiveDiffusivity nu cstar gamma (3 ^ m) = √(nu ^ 2 + cstar * gamma⁻¹ * 3 ^ (2 * gamma * ↑m))

The profile at a triadic scale, written with the exponent in the form used by the renormalization theorem.

theorem Algsuperdiff.Section5.Support.intrinsicScale_pos {nu cstar gamma t : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (ht : 0 < t) : 0 < intrinsicScale nu cstar gamma t

The intrinsic scale is positive.

theorem Algsuperdiff.Section5.Support.effectiveDiffusivity_nonneg (nu cstar gamma r : ℝ) : 0 ≤ effectiveDiffusivity nu cstar gamma r

The effective diffusivity profile is nonnegative.

theorem Algsuperdiff.Section5.Support.intrinsicScale_sq_rpow {nu cstar gamma t : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma2 : gamma < 2) (ht : 0 < t) : (intrinsicScale nu cstar gamma t ^ 2) ^ (2 - gamma) = (nu * t) ^ (2 - gamma) + cstar * gamma⁻¹ * t ^ 2

The defining identity of the intrinsic scale, read on its square: (R(t)²)^{2-γ} = (ν t)^{2-γ} + c⋆ γ^{-1} t².

2. The elementary inequality behind both halves

3. The comparison at the intrinsic scale itself

theorem Algsuperdiff.Section5.Support.mul_le_intrinsicScale_sq {nu cstar gamma t : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma2 : gamma < 2) (ht : 0 < t) : nu * t ≤ intrinsicScale nu cstar gamma t ^ 2

ν t ≤ R(t)²: the intrinsic scale is above the diffusive scale.

4. The comparison at a scale above the intrinsic scale

theorem Algsuperdiff.Section5.Support.abs_intrinsicScale_sq_sub_effectiveDiffusivity_mul_le {nu cstar gamma t : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) (ht : 0 < t) {r : ℝ} (hr : intrinsicScale nu cstar gamma t ≤ r) : |intrinsicScale nu cstar gamma t ^ 2 - effectiveDiffusivity nu cstar gamma r * t| ≤ gamma * r ^ 2

The scale arithmetic, exact half. At every length scale r above the intrinsic scale, the square of the intrinsic scale and the displacement ν_eff(r) t differ by at most γ r².

theorem Algsuperdiff.Section5.Support.effectiveDiffusivity_mul_le_sq {nu cstar gamma t : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma1 : gamma ≤ 1) (ht : 0 < t) {r : ℝ} (hr : intrinsicScale nu cstar gamma t ≤ r) : effectiveDiffusivity nu cstar gamma r * t ≤ r ^ 2

The displacement never exceeds the square of the scale. At every length scale r above the intrinsic scale, ν_eff(r) t ≤ r².

5. The comparison with the effective diffusivity of the renormalization

theorem Algsuperdiff.Section5.Support.one_le_abs_log {gamma : ℝ} (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) : 1 ≤ |Real.log gamma|

On the admissible range of the coupling, 1 ≤ |log γ|.

theorem Algsuperdiff.Section5.Support.one_le_sqrt_abs_log {gamma : ℝ} (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) : 1 ≤ √|Real.log gamma|

On the admissible range of the coupling, 1 ≤ |log γ|^{1/2}.

theorem Algsuperdiff.Section5.Support.abs_intrinsicScale_sq_sub_mul_le {nu cstar gamma t : ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hgamma4 : gamma ≤ 1 / 4) (ht : 0 < t) {r : ℝ} (hr : intrinsicScale nu cstar gamma t ≤ r) {sigmaBar C : ℝ} (hsigma : 0 < sigmaBar) (hC : 0 ≤ C) (hsmall : C * √gamma * |Real.log gamma| ≤ 1 / 2) (hprofile : |sigmaBar - effectiveDiffusivity nu cstar gamma r| ≤ C * √gamma * |Real.log gamma| * sigmaBar) : |intrinsicScale nu cstar gamma t ^ 2 - sigmaBar * t| ≤ (1 + 2 * C) * √gamma * |Real.log gamma| * r ^ 2

The scale arithmetic. Let σ be an effective diffusivity within the relative error C γ^{1/2} |log γ| of the profile at a length scale r above the intrinsic scale. Then the square of the intrinsic scale and the displacement σ t differ by at most (1 + 2C) γ^{1/2} |log γ| r².

The relative error of the renormalization theorem is exactly the hypothesis hprofile, and the smallness hypothesis hsmall is the statement that the relative error is at most one half, so that σ and the profile are comparable. The γ produced by the exact half is absorbed into the displayed factor by γ ≤ γ^{1/2} |log γ|.