ConfinementScaleMinimality

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

Minimality at the confinement scale, and the level sets of the random scale

The confinement scale m_t is the least scale n with L (1 + S_n) ≤ 3^n. Its defining inequality bounds the widened scale from above; what bounds the confinement scale itself from above is minimality, the failure of the same inequality one scale lower. This file turns that failure into a usable estimate and then into a bound on the probability of each level set of the random scale.

The first step is the recursion

S_{n-1} ≤ S_{n-1} + (1/9) S_n,

which holds because the widening weight 3^{-2(k-n)} loses exactly a factor of nine when the base scale drops by one. Combining it with the defining inequality at m_t itself, which bounds L S_{m_t} by 3^{m_t}, the failure one scale lower reads

3^{m_t - 1} < L (1 + S_{m_t-1} + (1/9) S_{m_t}) ≤ L (1 + S_{m_t-1}) + (1/9) 3^{m_t},

and hence 3^{m_t} ≤ (9/2) L (1 + S_{m_t-1}): the confinement scale is controlled by a single displacement scale, not by the widened supremum.

The scale index is random, so this is not yet a moment bound. What it gives is a bound on the probability of the level set {m_t = n}: on that event a single displacement scale is at least (2/27) 3^{n - m_0} - 1, where 3^{m_0} ≤ L is the deterministic lower bound for the scale, and Chebyshev's inequality at a uniform moment of the displacement scales turns this into a geometric decay in n - m_0. That decay is what makes the moments of 3^{m_t} and of any family indexed by the random scale summable.

References

• ABK26, the superdiffusive displacement bounds of Section 5.4.

1. The recursion for the widened scale

theorem Algsuperdiff.Section5.Support.widenedScale_pred_le (S : ℤ → ℝ) (n : ℤ) : widenedScale S (n - 1) ≤ ENNReal.ofReal (S (n - 1)) + ENNReal.ofReal 9⁻¹ * widenedScale S n

The widening recursion. Lowering the base scale by one adds the scale at the new index and divides the previous widened scale by nine.

2. Minimality

theorem Algsuperdiff.Section5.Support.three_zpow_le_of_isConfinementScale {S : ℤ → ℝ} (hSnn : ∀ (k : ℤ), 0 ≤ S k) {L : ℝ} (hL : 0 < L) {m : ℤ} (hm : IsConfinementScale (fun (n : ℤ) => widenedScale S n) L m) : 3 ^ m ≤ 9 / 2 * L * (1 + S (m - 1))

Minimality at the confinement scale. Since the scale one below the confinement scale fails the defining inequality, and the widening recursion reduces the widened scale there to the single scale S_{m-1} plus a ninth of the widened scale at m, the confinement scale obeys 3^m ≤ (9/2) L (1 + S_{m-1}).

3. Measurability of the confinement scale

theorem Algsuperdiff.Section5.Support.measurableSet_mem_confinementSet {Omega : Type u_1} [MeasurableSpace Omega] {S : ℤ → Omega → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) (L : ℝ) (n : ℤ) : MeasurableSet {omega : Omega | n ∈ confinementSet (fun (j : ℤ) => widenedScale (fun (k : ℤ) => S k omega) j) L}

The defining set of the confinement scale is measurable at every fixed scale.

4. The level sets of the confinement scale

theorem Algsuperdiff.Section5.Support.intLog_le_of_isConfinementScale {S : ℤ → ℝ} {L : ℝ} (hL : 0 < L) {m : ℤ} (hm : IsConfinementScale (fun (n : ℤ) => widenedScale S n) L m) : Int.log 3 L ≤ m

The deterministic lower bound for the confinement scale.

theorem Algsuperdiff.Section5.Support.measure_isConfinementScale_eq_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {S : ℤ → Omega → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) (hSnn : ∀ (k : ℤ) (omega : Omega), 0 ≤ S k omega) {L : ℝ} (hL : 0 < L) {m : Omega → ℤ} (hm : ∀ᵐ (omega : Omega) ∂mu, IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L (m omega)) {C q : ℝ} (hC : 1 ≤ C) (hq : 0 < q) (hmom : ∀ (k : ℤ), ∫⁻ (omega : Omega), ENNReal.ofReal (S k omega) ^ q ∂mu ≤ ENNReal.ofReal C ^ q) (k : ℕ) : mu {omega : Omega | m omega = Int.log 3 L + ↑k} ≤ ENNReal.ofReal (C * 3 ^ (3 - ↑k)) ^ q

The probability of a level set of the confinement scale. Writing the scale as m_0 + k with 3^{m_0} ≤ L < 3^{m_0+1}, on the event {m_t = m_0 + k} a single displacement scale is at least 3^{k-3}, so a uniform moment bound of order q for the displacement scales gives a geometric bound of ratio 3^{-q} for the probability of the event.

5. The measurable choice of the confinement scale

noncomputable def Algsuperdiff.Section5.Support.confinementScale {Omega : Type u_1} (S : ℤ → Omega → ℝ) (L : ℝ) (omega : Omega) : ℤ

The confinement scale as a function of the sample. Where a confinement scale exists it is unique, and this is that scale; where none exists the value is 0.

The value off the existence event is immaterial. Every statement below about confinementScale is either conditioned on the existence of a confinement scale at the sample or holds almost surely, and the existence event has full measure whenever the displacement scales have one uniform moment bound (ae_exists_isConfinementScale); nothing in this development reads the value on its complement.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Support.isConfinementScale_confinementScale {Omega : Type u_1} {S : ℤ → Omega → ℝ} {L : ℝ} {omega : Omega} (h : ∃ (m : ℤ), IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L m) : IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L (confinementScale S L omega)

Where a confinement scale exists, the chosen value is one.

theorem Algsuperdiff.Section5.Support.confinementScale_eq {Omega : Type u_1} {S : ℤ → Omega → ℝ} {L : ℝ} {omega : Omega} {m : ℤ} (hm : IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L m) : confinementScale S L omega = m

The chosen value is the confinement scale, wherever there is one.

theorem Algsuperdiff.Section5.Support.confinementScale_eq_zero {Omega : Type u_1} {S : ℤ → Omega → ℝ} {L : ℝ} {omega : Omega} (h : ¬∃ (m : ℤ), IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L m) : confinementScale S L omega = 0

Where no confinement scale exists the chosen value is 0.

theorem Algsuperdiff.Section5.Support.measurable_confinementScale {Omega : Type u_1} [MeasurableSpace Omega] {S : ℤ → Omega → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) (L : ℝ) : Measurable (confinementScale S L)

The chosen confinement scale is measurable. Each level set is the event that the scale is admissible intersected with countably many complements, and the level set at 0 carries in addition the event that no scale is admissible.

theorem Algsuperdiff.Section5.Support.ae_isConfinementScale_confinementScale {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {S : ℤ → Omega → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) {C p L : ℝ} (hC : 0 ≤ C) (hp : 1 ≤ p) (hL : 0 < L) (hmom : ∀ (k : ℤ), ∫⁻ (omega : Omega), ENNReal.ofReal (S k omega) ^ p ∂mu ≤ ENNReal.ofReal C ^ p) : ∀ᵐ (omega : Omega) ∂mu, IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L (confinementScale S L omega)

The chosen confinement scale is almost surely a confinement scale. One uniform moment bound for the displacement scales makes the defining set almost surely nonempty, and the infimum is then attained.