awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
      ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)
have obtain : ∀ (i : ℕ) (hi : v i < ε),
  ∀ᶠ (x : ℕ) in atTop,
    ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
      ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)
Tactic: obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
      ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)
have h : ∀ (n : ℕ)
  (hn :
    |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
      v i * (↑⌊c ^ n⌋₊ : ℝ)),
  ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
    ε * norm (E := ℝ) (↑⌊c ^ n⌋₊ : ℝ)
Tactic: filter_upwards [hω i] with n hn
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
n : ℕ
hn :
  |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
    v i * (↑⌊c ^ n⌋₊ : ℝ)
⊢ ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
    ε * norm (E := ℝ) (↑⌊c ^ n⌋₊ : ℝ)
have h : |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
        (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| ≤
  ε * (↑⌊c ^ n⌋₊ : ℝ)
Tactic: simp only [Real.norm_eq_abs, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have h : Eq (α := ℕ → ℝ)
  (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
  ((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
Tactic: convert! (tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop using 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ Eq (α := ℕ → ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
    ((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
have h : ∀ (i : ℕ),
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
    (((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
      i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    Nat.cast
have A : Tendsto (β := ℝ)
  (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
  (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
Tactic: have A : Tendsto (fun i => 𝔼[truncation (X i) i]) atTop (𝓝 𝔼[X 0]) := by
    convert! (tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop using 1
    ext i
    exact (hident i).truncation.integral_eq
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    Nat.cast
have h : Eq (α := ℕ → ℝ)
  (fun (n : ℕ) ↦
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
  fun (n : ℕ) ↦
  ∑ i ∈ range n,
    HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
Tactic: convert! Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 A) using 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦
    ∑ i ∈ range n,
      HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
have h : ∀ (n : ℕ),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    ∑ i ∈ range n,
      HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
n : ℕ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    ∑ i ∈ range n,
      HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
have h : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ ∑ c ∈ range n, truncation (X c) (↑c : ℝ) a)
  (∑ x ∈ range n, @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X x) (↑x : ℝ) a)
Tactic: simp only [sum_sub_distrib, sum_const, card_range, nsmul_eq_mul, sum_apply, sub_left_inj]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
n : ℕ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ ∑ c ∈ range n, truncation (X c) (↑c : ℝ) a)
    (∑ x ∈ range n, @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X x) (↑x : ℝ) a)
have rw : ∀ i ∈ range n, @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (truncation (X i) (↑i : ℝ)) ℙ
Tactic: rw [integral_finsetSum _ fun i _ => ?_]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
⊢ ∀ᵐ (ω : Ω),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
          HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
      fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
have h : ∀ (ω : Ω)
  (hω :
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦
        HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
      fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)),
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
Tactic: filter_upwards [strong_law_aux2 X hint hindep hident hnonneg c_one] with ω hω
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
have A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
Tactic: have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
    tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
have h : Eq (α := ℕ → ℝ)
  (fun (n : ℕ) ↦
    ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
  fun (x : ℕ) ↦
  HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
        (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a) +
    ((fun (n : ℕ) ↦
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
            HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
        fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
      x
Tactic: convert! hω.add ((strong_law_aux3 X hint hident).comp_tendsto A) using 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (x : ℕ) ↦
    HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a) +
      ((fun (n : ℕ) ↦
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
              HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        x
have h : ∀ (n : ℕ),
  ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a) +
      ((fun (n : ℕ) ↦
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
              HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
have h : Eq (α := ℕ → ℝ≥0∞)
  (fun (j : ℕ) ↦
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
  fun (j : ℕ) ↦ ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)}
Tactic: convert! tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ Eq (α := ℕ → ℝ≥0∞)
    (fun (j : ℕ) ↦
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    fun (j : ℕ) ↦
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)}
have h : ∀ (j : ℕ),
  Eq (α := ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)} : ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)} : ℝ≥0∞)
Tactic: ext1 j
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∀ᵐ (ω : Ω),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
      fun (n : ℕ) ↦ (↑n : ℝ)
have A : LT.lt (α := ℝ≥0∞)
  (∑' (j : ℕ), ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
  ∞
Tactic: have A : (∑' j : ℕ, ℙ {ω | X j ω ∈ Set.Ioi (j : ℝ)}) < ∞ := by
    convert! tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2
    ext1 j
    exact (hident j).measure_mem_eq measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
⊢ ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
have h : ∀ (ω : Ω) (hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
Tactic: filter_upwards [ae_eventually_notMem A.ne] with ω hω