ConfinementScale

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

The widened scale and the confinement scale

The superdiffusive displacement bounds are stated at a random confinement scale m_t, built from the displacement scales S_k of the tail bound in two steps. First the scales are widened,

S_n = sup_{k ≥ n} S_k 3^{-2(k-n)},

which is what makes the tail bound available at every scale above n and not only at n itself. Then the confinement scale is the smallest integer above the logarithm of K (1 + S_n) |log γ|^{1/2} R(t):

m_t = inf {n ∈ ℤ : n ≥ ⌈log₃ (K (1 + S_n) |log γ|^{1/2} R(t))⌉}.

Two points of the reading. The widened scale is ℝ≥0∞-valued: the supremum is over an infinite family and can be infinite, and the value ⊤ is the honest one there — no truncation and no fallback. The infimum is an infimum of a set of integers, which the source takes without comment; it is attained as soon as the set is nonempty, because the set is bounded below by log₃ of the deterministic factor, and that is the content of exists_isConfinementScale. A scale at which the widened scale is infinite is never in the set, so the definition needs no side condition.

Main definitions

• widenedScale S n — the widened scale S_n, in ℝ≥0∞.
• confinementSet Stilde L — the set the confinement scale is the infimum of.
• IsConfinementScale Stilde L m — m is that infimum, attained.

References

• ABK26, the superdiffusive displacement bounds of Section 5.4.

1. The widened scale

noncomputable def Algsuperdiff.Section5.Support.widenedScale (S : ℤ → ℝ) (n : ℤ) : ENNReal

The widened scale S_n = sup_{k ≥ n} S_k 3^{-2(k-n)}. The supremum is taken in ℝ≥0∞, where an unbounded family has the value ⊤.

Equations

• Algsuperdiff.Section5.Support.widenedScale S n = ⨆ (k : { k : ℤ // n ≤ k }), ENNReal.ofReal (S ↑k * 3 ^ (-2 * (↑k - n)))

theorem Algsuperdiff.Section5.Support.widenedScale_eq_iSup_nat (S : ℤ → ℝ) (n : ℤ) : widenedScale S n = ⨆ (j : ℕ), ENNReal.ofReal (S (n + ↑j) * 3 ^ (-2 * ↑j))

The supremum over the scales k ≥ n, reindexed by k = n + j with j : ℕ. This is the countable form used for measurability and for the moments.

2. The confinement scale

def Algsuperdiff.Section5.Support.confinementSet (Stilde : ℤ → ENNReal) (L : ℝ) : Set ℤ

The set the confinement scale is the infimum of: the scales n with L (1 + S_n) ≤ 3^n, where L is the deterministic factor K |log γ|^{1/2} R(t).

Equations

• Algsuperdiff.Section5.Support.confinementSet Stilde L = {n : ℤ | ENNReal.ofReal L * (1 + Stilde n) ≤ ENNReal.ofReal (3 ^ n)}

theorem Algsuperdiff.Section5.Support.int_log_le_of_mem_confinementSet {Stilde : ℤ → ENNReal} {L : ℝ} (hL : 0 < L) {n : ℤ} (hn : n ∈ confinementSet Stilde L) : Int.log 3 L ≤ n

The set is bounded below, by the integer logarithm of the deterministic factor: the widened scale is nonnegative, so every admissible scale already satisfies L ≤ 3^n.

def Algsuperdiff.Section5.Support.IsConfinementScale (Stilde : ℤ → ENNReal) (L : ℝ) (m : ℤ) : Prop

The confinement scale: the least admissible scale, that is, the attained infimum of confinementSet.

Equations

• Algsuperdiff.Section5.Support.IsConfinementScale Stilde L m = IsLeast (Algsuperdiff.Section5.Support.confinementSet Stilde L) m

theorem Algsuperdiff.Section5.Support.exists_isConfinementScale {Stilde : ℤ → ENNReal} {L : ℝ} (hL : 0 < L) (hne : (confinementSet Stilde L).Nonempty) : ∃ (m : ℤ), IsConfinementScale Stilde L m

The infimum is attained. The set of admissible scales is bounded below by log₃ L, so as soon as it is nonempty it has a least element.

theorem Algsuperdiff.Section5.Support.isConfinementScale_unique {Stilde : ℤ → ENNReal} {L : ℝ} {m m' : ℤ} (hm : IsConfinementScale Stilde L m) (hm' : IsConfinementScale Stilde L m') : m = m'

There is only one confinement scale.

theorem Algsuperdiff.Section5.Support.le_three_zpow_of_isConfinementScale' {Stilde : ℤ → ENNReal} {L Rt : ℝ} {m : ℤ} (hRt : Rt ≤ L) (hm : IsConfinementScale Stilde L m) : Rt ≤ 3 ^ m

The confinement scale is above the intrinsic scale. Any real below the deterministic factor — in the source, R(t), which is L divided by K |log γ|^{1/2} ≥ 1 — is below 3^{m_t}.