DisplacementScale

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

The displacement scale S_m and its moments

The tail bound on the displacement is stated at a random scale

S_m = δ^{-1/(1-γ)} 3^{Y_m(ε)},

where Y_m(ε) is the ℕ-valued scale of the chains-of-good-cubes estimate and δ ∈ (0, 1] is the separation parameter of the argument. The scale is a genuine positive real at every sample: Y is ℕ-valued, so 3^{Y} is a natural power of three and no fallback value is involved.

The moment bound is one integration of the tail of Y. If

P[Y ≥ N] ≤ exp(-a 3^N) for N ≥ 1,

then, for every exponent p with 2 p log 3 ≤ a,

E[S_m^p] ≤ (δ^{-1/(1-γ)} (1 - e^{-a/2})^{-1})^p,

so E[S_m^p]^{1/p} is bounded by a constant. The two steps are: the summand 3^{pN} exp(-a 3^N) is at most exp(-aN/2) because 3^N ≥ N, and the resulting geometric series is summed. The admissible exponents are exactly those below a / (2 log 3): with the rate a = c ε² γ^{-1} |log γ|^{-6} of the chains estimate this is (c ε² / (2 log 3)) γ^{-1} |log γ|^{-6}, the shape the source uses.

The constants of the bound are uniform over the model: ε is bounded below by C γ^{1/2} |log γ|^{7/2}, which makes the rate at least c C² |log γ|, and γ ≤ 1/4 makes δ^{-1/(1-γ)} at most δ^{-4/3}.

The admissible exponents are nonempty only when the rate exceeds 2 log 3, and at the bottom ε = C γ^{1/2}|log γ|^{7/2} of the accuracy range the rate is c C² |log γ|, whose size is governed by constants that nothing here pins. The way out is the top of the range: at ε = 1/4 the rate is (c/16) γ^{-1}|log γ|^{-6}, which is large for small γ. The last section makes that quantitative, with an explicit threshold γ_1(c, C) below which ε = 1/4 is an admissible accuracy and the exponent p = 1 is admissible with it.

Main definitions

• displacementScale delta gamma N — the value δ^{-1/(1-γ)} 3^N of S_m at Y = N.

References

• ABK26, the displacement tail bound of Section 5.3.

1. The scale

noncomputable def Algsuperdiff.Section5.Support.displacementScale (delta gamma : ℝ) (N : ℕ) : ℝ

The displacement scale S_m = δ^{-1/(1-γ)} 3^{Y_m(ε)}, as a function of the value N of Y_m(ε).

Equations

• Algsuperdiff.Section5.Support.displacementScale delta gamma N = delta ^ (-(1 - gamma)⁻¹) * 3 ^ N

theorem Algsuperdiff.Section5.Support.displacementScale_pos {delta : ℝ} (hdelta : 0 < delta) (gamma : ℝ) (N : ℕ) : 0 < displacementScale delta gamma N

The scale is a genuine positive real, at every value of Y.

theorem Algsuperdiff.Section5.Support.measurable_displacementScale {Omega : Type u_1} [MeasurableSpace Omega] {Y : Omega → ℕ} (hY : Measurable Y) (delta gamma : ℝ) : Measurable fun (omega : Omega) => displacementScale delta gamma (Y omega)

The scale is a measurable function of the sample whenever Y is.

2. The integration of the tail

theorem Algsuperdiff.Section5.Support.lintegral_ofReal_three_pow_rpow_le_of_tail {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {Y : Omega → ℕ} (hY : Measurable Y) {a p : ℝ} (ha : 0 < a) (hpa : 2 * (p * Real.log 3) ≤ a) (htail : ∀ (N : ℕ), 1 ≤ N → mu {omega : Omega | N ≤ Y omega} ≤ ENNReal.ofReal (Real.exp (-(a * 3 ^ N)))) : ∫⁻ (omega : Omega), ENNReal.ofReal (3 ^ Y omega) ^ p ∂mu ≤ ENNReal.ofReal (1 - Real.exp (-(a / 2)))⁻¹

The integration of the tail. An ℕ-valued variable whose tail decays like exp(-a 3^N) from N = 1 on has E[3^{pY}] ≤ (1 - e^{-a/2})^{-1} at every exponent p with 2 p log 3 ≤ a.

theorem Algsuperdiff.Section5.Support.lintegral_ofReal_displacementScale_rpow_le {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {Y : Omega → ℕ} (hY : Measurable Y) {delta gamma a p : ℝ} (hdelta : 0 < delta) (ha : 0 < a) (hp : 1 ≤ p) (hpa : 2 * (p * Real.log 3) ≤ a) (htail : ∀ (N : ℕ), 1 ≤ N → mu {omega : Omega | N ≤ Y omega} ≤ ENNReal.ofReal (Real.exp (-(a * 3 ^ N)))) : ∫⁻ (omega : Omega), ENNReal.ofReal (displacementScale delta gamma (Y omega)) ^ p ∂mu ≤ ENNReal.ofReal (delta ^ (-(1 - gamma)⁻¹) * (1 - Real.exp (-(a / 2)))⁻¹) ^ p

The moment bound for the displacement scale at an arbitrary rate.