OAI/Probability/SLE/Gauge/MomentCoefficientConvergence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded truncation of the prescribed moment coefficients. An integrable finite-level density is enough to pass from convergence in probability of the discrete mass to its clipped weighted moments.

  1. lemma OAI.SLEExactGauge.continuous_clip line 15
  2. lemma OAI.SLEExactGauge.clip_nonneg line 18
  3. lemma OAI.SLEExactGauge.clip_le line 21
  4. theorem OAI.SLEExactGauge.weighted_clip_pow_integral_tendsto line 25

    Source documentation

    This is the inner limit in the paper's explicit coefficient formula; the density need only be integrable, not uniformly bounded.

    theorem weighted_clip_pow_integral_tendsto
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsFiniteMeasure P]
    (X : ℕ → Ω → ℝ) (Y w : Ω → ℝ)
    (hX : ∀ n, AEStronglyMeasurable (X n) P) (hw : Integrable w P)
    (hXY : TendstoInMeasure P X atTop Y) (u : ℝ) (hu : 0 ≤ u) (k : ℕ) :
    Tendsto (fun n => ∫ ω, w ω*(Target.clip u (X n ω))^k ∂P) atTop
      (𝓝 (∫ ω, w ω*(Target.clip u (Y ω))^k ∂P)) := by
…

    Mentions: OAI.SLEExactGauge.Target.clip