strong_law_Lp — Mathlib

English

Let X_n be i.i.d. E-valued random variables with X_0 ∈ L^p for some p ≥ 1, p < ∞. Then the L^p-distance between the empirical mean and the true mean tends to zero: lim_{n→∞} ||(1/n) ∑_{i=0}^{n-1} X_i - μ[X_0]||_{L^p(μ)} = 0.

Русский

Пусть X_n — независимы и одинаково распределены значения в банаховом пространстве, X_0 ∈ L^p. Тогда сходится в L^p: лимит нормы отклонения среднего от мат. ожидания равен нулю.

LaTeX

$$$\displaystyle \lim_{n \to \infty} \left\| \frac{1}{n} \sum_{i=0}^{n-1} X_i - μ[X_0] \right\|_{L^p(μ)} = 0$$$

Lean4

/-- **Strong law of large numbers**, Lᵖ version: if `X n` is a sequence of independent
identically distributed random variables in Lᵖ, then `n⁻¹ • ∑ i ∈ range n, X i`
converges in `Lᵖ` to `𝔼[X 0]`. -/
theorem strong_law_Lp {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞) (X : ℕ → Ω → E) (hℒp : MemLp (X 0) p μ)
    (hindep : Pairwise ((IndepFun · · μ) on X)) (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
    Tendsto (fun (n : ℕ) => eLpNorm (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω) - μ[X 0]) p μ) atTop (𝓝 0) := by
  -- First exclude the trivial case where the space is not a probability space

  by_cases h : ∀ᵐ ω ∂μ, X 0 ω = 0
  · have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
    have A (n : ℕ) : eLpNorm (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω) - μ[X 0]) p μ = 0 :=
      by
      simp only [integral_eq_zero_of_ae h, sub_zero]
      apply eLpNorm_eq_zero_of_ae_zero
      filter_upwards [I] with ω hω
      simp [hω]
    simp [A]
      -- Then use ae convergence and uniform integrability

  have : IsProbabilityMeasure μ :=
    MemLp.isProbabilityMeasure_of_indepFun (X 0) (X 1) (zero_lt_one.trans_le hp).ne' hp' hℒp h (hindep zero_ne_one)
  have hmeas : ∀ i, AEStronglyMeasurable (X i) μ := fun i => (hident i).aestronglyMeasurable_iff.2 hℒp.1
  have hint : Integrable (X 0) μ := hℒp.integrable hp
  have havg (n : ℕ) : AEStronglyMeasurable (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω)) μ :=
    AEStronglyMeasurable.const_smul (aestronglyMeasurable_fun_sum _ fun i _ => hmeas i) _
  refine
    tendsto_Lp_finite_of_tendstoInMeasure hp hp' havg (memLp_const _) ?_
      (tendstoInMeasure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident))
  rw [(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω)) = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))]
  · apply UniformIntegrable.unifIntegrable
    apply uniformIntegrable_average hp
    exact MemLp.uniformIntegrable_of_identDistrib hp hp' hℒp hident
  · ext n ω
    simp only [Pi.smul_apply, sum_apply]

Похожие утверждения