PthMomentProcessTail

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

Moment integration from a restricted triadic displacement tail

The displacement comparison is available at triadic radii no smaller than the normalization scale. This file interpolates that restricted family to a continuous exponential tail and then integrates it. The bounded-probability branch handles all smaller radii.

theorem Algsuperdiff.Section5.Provider.measureReal_lt_div_le_two_mul_exp_neg_of_triadic_sq_tail {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {Z : Omega → ℝ} {R c : ℝ} (hR : 0 < R) (hc : 0 < c) (hc1 : c ≤ 1) (htail : ∀ (k : ℤ), R ≤ 3 ^ k → mu.real {omega : Omega | 1 / 2 * 3 ^ k ≤ Z omega} ≤ Real.exp (-c * (3 ^ k / R) ^ 2)) : have A := 3 / 2 * max 1 (c * Real.log 2)⁻¹; ∀ (s : ℝ), 0 < s → mu.real {omega : Omega | s < Z omega / (A * R)} ≤ 2 * Real.exp (-s)

A square-exponential tail at every triadic radius gives the normalized exponential tail used by the moment integrator. The explicit enlargement factor pays only for interpolation between adjacent powers of three and for the bounded-probability range below log 2.

theorem Algsuperdiff.Section5.Provider.integral_rpow_le_of_triadic_sq_tail {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure mu] {Z : Omega → ℝ} (hZ : AEMeasurable Z mu) (hZ0 : 0 ≤ᵐ[mu] Z) {R c p : ℝ} (hR : 0 < R) (hc : 0 < c) (hc1 : c ≤ 1) (hp : 1 ≤ p) (htail : ∀ (k : ℤ), R ≤ 3 ^ k → mu.real {omega : Omega | 1 / 2 * 3 ^ k ≤ Z omega} ≤ Real.exp (-c * (3 ^ k / R) ^ 2)) : have A := 3 / 2 * max 1 (c * Real.log 2)⁻¹; MeasureTheory.Integrable (fun (omega : Omega) => Z omega ^ p) mu ∧ ∫ (omega : Omega), Z omega ^ p ∂mu ≤ (6 * p * (A * R)) ^ p

The C2 integration step from a triadic square-exponential tail.