ConfinementScaleMoments

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

The moments of the widened scale, and the existence of the confinement scale

Widening the displacement scales costs a constant factor in the moments: since

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

a bound E[S_k^p] ≤ C^p valid at every scale gives

E[S_n^p] ≤ C^p Σ_{j ≥ 0} 3^{-2pj} ≤ (9/8) C^p ≤ ((9/8) C)^p for p ≥ 1,

uniformly in n. The geometric series is what the exponent -2(k-n) of the widening is there for: at p ≥ 1 its ratio is at most 1/9.

That uniform bound is also what makes the confinement scale exist. Its defining set is empty only if L (1 + S_n) > 3^n at every scale n, and the probability of that is at most the probability of the single event at one scale, which Chebyshev's inequality bounds by (C'/λ_n)^p with λ_n = 3^n/L - 1. Taking n large makes this arbitrarily small, so the set is almost surely nonempty and, being bounded below, has a least element.

Main results

• measurable_widenedScale — the widened scale is a measurable function of the sample, being a countable supremum.
• lintegral_widenedScale_rpow_le — the moment bound, uniform in the scale.
• ae_nonempty_confinementSet, ae_exists_isConfinementScale — the defining set is almost surely nonempty, so the confinement scale almost surely exists.

References

• ABK26, the superdiffusive displacement bounds of Section 5.4.

1. Three arithmetic steps

2. Measurability and the moments of the widened scale

theorem Algsuperdiff.Section5.Support.measurable_widenedScale {Omega : Type u_1} [MeasurableSpace Omega] {S : ℤ → Omega → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) (n : ℤ) : Measurable fun (omega : Omega) => widenedScale (fun (k : ℤ) => S k omega) n

The widened scale is measurable: reindexed by ℕ it is a countable supremum.

theorem Algsuperdiff.Section5.Support.lintegral_widenedScale_rpow_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) {S : ℤ → Omega → ℝ} (hmeas : ∀ (k : ℤ), Measurable (S k)) {C p : ℝ} (hp : 1 ≤ p) (n : ℤ) (hmom : ∀ (k : ℤ), ∫⁻ (omega : Omega), ENNReal.ofReal (S k omega) ^ p ∂mu ≤ ENNReal.ofReal C ^ p) : ∫⁻ (omega : Omega), widenedScale (fun (k : ℤ) => S k omega) n ^ p ∂mu ≤ ENNReal.ofReal (C * (9 / 8)) ^ p

The moments of the widened scale. A moment bound valid at every scale is inherited by the widened scale, uniformly in the scale, at the cost of the factor 9/8 coming from the geometric series of the widening.

3. The confinement scale exists almost surely

theorem Algsuperdiff.Section5.Support.ae_nonempty_confinementSet {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, (confinementSet (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L).Nonempty

The defining set of the confinement scale is almost surely nonempty. At one scale the failure probability is bounded by Chebyshev's inequality through the uniform moment bound of the widened scale, and it tends to zero as the scale grows.

theorem Algsuperdiff.Section5.Support.ae_exists_isConfinementScale {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, ∃ (m : ℤ), IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L m

The confinement scale almost surely exists. Combining the almost-sure nonemptiness with the attainment of the infimum.