ConfinementScaleRandomMoments

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

Moments at the random confinement scale

The displacement bounds are stated at the random confinement scale m_t, so every quantity that enters them is evaluated at a random index. Two such quantities need moment bounds: the scale 3^{m_t} itself, and the error random variable of the renormalization theorem read at that scale. Neither is a moment of any single deterministic object, and this file supplies both, by summing over the level sets of the random index.

The mechanism is the same in both cases. Writing m_0 for the deterministic lower bound ⌊log₃ L⌋ of the confinement scale, the level sets {m_t = m_0 + k}, k ∈ ℕ, cover the sample space up to a null set, they are disjoint, and the probability of the k-th one decays like 3^{-2pk} by the minimality estimate. For the scale itself the value on the level set is the deterministic number 3^{m_0+k}, so the integral is a geometric series with ratio 3^{-p}. For a family indexed by the scales, the level set is coupled to the value by the Cauchy--Schwarz inequality, which spends the moment of order 2p of the family and half of the decay of the level set; the remaining half is again a geometric series with ratio 3^{-p}.

Both bounds therefore need the moments of the displacement scales at the exponent 2p rather than at p: halving the admissible range of exponents is the price of the random index, and it changes only the constant in front of the range p ≤ C^{-1} γ^{-1} |log γ|^{-6}.

References

• ABK26, the superdiffusive displacement bounds of Section 5.4.

1. Two arithmetic steps

2. The level sets of the random scale

3. The moments of the confinement scale

theorem Algsuperdiff.Section5.Support.lintegral_three_zpow_isConfinementScale_rpow_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 → ℤ} (hmmeas : Measurable m) (hm : ∀ᵐ (omega : Omega) ∂mu, IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L (m omega)) {C p : ℝ} (hC : 1 ≤ C) (hp : 1 ≤ p) (hmom : ∀ (k : ℤ), ∫⁻ (omega : Omega), ENNReal.ofReal (S k omega) ^ (2 * p) ∂mu ≤ ENNReal.ofReal C ^ (2 * p)) : ∫⁻ (omega : Omega), ENNReal.ofReal (3 ^ m omega) ^ p ∂mu ≤ ENNReal.ofReal (2187 / 2 * C ^ 2 * L) ^ p

The moments of the confinement scale. Minimality bounds 3^{m_t} by a single displacement scale, and summing the level sets of the random index against a uniform moment bound of order 2p for the displacement scales gives a moment bound of order p for 3^{m_t}, proportional to the deterministic factor L.

4. Moments of a family at the random scale

theorem Algsuperdiff.Section5.Support.lintegral_atConfinementScale_rpow_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 → ℤ} (hmmeas : Measurable m) (hm : ∀ᵐ (omega : Omega) ∂mu, IsConfinementScale (fun (n : ℤ) => widenedScale (fun (k : ℤ) => S k omega) n) L (m omega)) {C p : ℝ} (hC : 1 ≤ C) (hp : 1 ≤ p) (hmom : ∀ (k : ℤ), ∫⁻ (omega : Omega), ENNReal.ofReal (S k omega) ^ (2 * p) ∂mu ≤ ENNReal.ofReal C ^ (2 * p)) {F : ℤ → Omega → ℝ} (hFmeas : ∀ (n : ℤ), Measurable (F n)) {D : ℝ} (hD : 0 ≤ D) (hFmom : ∀ (n : ℤ), ∫⁻ (omega : Omega), ENNReal.ofReal (F n omega) ^ (2 * p) ∂mu ≤ ENNReal.ofReal D ^ (2 * p)) : ∫⁻ (omega : Omega), ENNReal.ofReal (F (m omega) omega) ^ p ∂mu ≤ ENNReal.ofReal (81 / 2 * C * D) ^ p

The moments of a family at the confinement scale. A family of nonnegative random variables indexed by the scales, with a moment bound of order 2p uniform in the scale, has at the random confinement scale a moment bound of order p with the same profile, at the cost of an explicit constant.