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
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (_x : ℕ) ↦ 1
have h : Eq (α := ℕ → ℝ)
  (fun (x : ℕ) ↦
    HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
  fun (x : ℕ) ↦
  (∑ i ∈ range ⌊c ^ x⌋₊, X i ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
    (↑⌊c ^ x⌋₊ : ℝ)⁻¹
Tactic: convert! L.mul_isBigO (isBigO_refl (fun n : ℕ => (⌊c ^ n⌋₊ : ℝ)⁻¹) 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) ℙ
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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
h :
  Eq (α := ℕ → ℝ)
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (x : ℕ) ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
      (↑⌊c ^ x⌋₊ : ℝ)⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (_x : ℕ) ↦ 1
have h₁ : Eq (α := ℕ → ℝ) (fun (_x : ℕ) ↦ 1) fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (↑⌊c ^ x⌋₊ : ℝ)⁻¹
Tactic: convert! L.mul_isBigO (isBigO_refl (fun n : ℕ => (⌊c ^ n⌋₊ : ℝ)⁻¹) 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) ℙ
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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ Eq (α := ℕ → ℝ)
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (x : ℕ) ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
      (↑⌊c ^ x⌋₊ : ℝ)⁻¹
have h : ∀ (n : ℕ),
  (HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    (∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
      (↑⌊c ^ 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) ℙ
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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ Eq (α := ℕ → ℝ) (fun (_x : ℕ) ↦ 1) fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (↑⌊c ^ x⌋₊ : ℝ)⁻¹
have h : ∀ (n : ℕ), 1 = HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (↑⌊c ^ 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) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have obtain : ∀ (c : ℕ → ℝ) (cone : ∀ (n : ℕ), 1 < c n) (clim : Tendsto c atTop (𝓝 1)),
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
Tactic: obtain ⟨c, -, cone, clim⟩ :
      ∃ c : ℕ → ℝ, StrictAnti c ∧ (∀ n : ℕ, 1 < c n) ∧ Tendsto c atTop (𝓝 1) :=
    exists_seq_strictAnti_tendsto (1 : ℝ)
-- 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 : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have this : ∀ (k : ℕ),
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
Tactic: have : ∀ k, ∀ᵐ ω,
      Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ⌊c k ^ n⌋₊) atTop (𝓝 𝔼[X 0]) :=
    fun k => strong_law_aux6 X hint hindep hident hnonneg (cone k)
-- 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 : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have h : ∀ (ω : Ω)
  (hω :
    ∀ (i : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
Tactic: filter_upwards [ae_all_iff.2 this] with ω hω
-- 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 : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
ω : Ω
hω :
  ∀ (i : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have apply : Monotone (β := ℝ) fun (n : ℕ) ↦ ∑ i ∈ range n, X i ω
Tactic: apply tendsto_div_of_monotone_of_tendsto_div_floor_pow _ _ _ c cone clim _
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have pos : ∀ (h : ∀ᵐ (ω : Ω), X 0 ω = 0),
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Tactic: by_cases h : ∀ᵐ ω, X 0 ω = 0
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
pos :
  ∀ (h : ∀ᵐ (ω : Ω), X 0 ω = 0),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), X 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have neg : ∀ (h : ¬∀ᵐ (ω : Ω), X 0 ω = 0),
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Tactic: by_cases h : ∀ᵐ ω, X 0 ω = 0
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
have rw : ∀ (i : ℕ), ∀ᵐ (a : Ω), X i a = 0
Tactic: rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
Tactic: 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
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have h₁ : ∀ (ω : Ω) (hω : ∀ (i : ℕ), X i ω = 0),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Tactic: filter_upwards [I] with ω hω
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ :=
    hint.isProbabilityMeasure_of_indepFun (X 0) (X 1) h (hindep zero_ne_one)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have posm : Measurable pos
Tactic: have posm : Measurable pos := measurable_id'.max measurable_const
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have negm : Measurable neg
Tactic: have negm : Measurable neg := measurable_id'.neg.max measurable_const
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have A : ∀ᵐ (ω : Ω),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
Tactic: have A : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (pos ∘ X i) ω) / n) atTop (𝓝 𝔼[pos ∘ X 0]) :=
    strong_law_aux7 _ hint.pos_part (fun i j hij => (hindep hij).comp posm posm)
      (fun i => (hident i).comp posm) fun i ω => le_max_right _ _
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have B : ∀ᵐ (ω : Ω),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
Tactic: have B : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, (neg ∘ X i) ω) / n) atTop (𝓝 𝔼[neg ∘ X 0]) :=
    strong_law_aux7 _ hint.neg_part (fun i j hij => (hindep hij).comp negm negm)
      (fun i => (hident i).comp negm) fun i ω => le_max_right _ _
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have h₁ : ∀ (ω : Ω)
  (hωpos :
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a)))
  (hωneg :
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Tactic: filter_upwards [A, B] with ω hωpos hωneg
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun (x1 x2 : Ω → ℝ) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun (x : ℝ) ↦ max x 0
neg : ℝ → ℝ := fun (x : ℝ) ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
B :
  ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
ω : Ω
hωpos :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (pos ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (pos ∘ X 0) a))
hωneg :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, (neg ∘ X i) ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (neg ∘ X 0) a))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have h₁ : ∀ (x : ℕ),
  HDiv.hDiv (α := ℝ) (∑ i ∈ range x, X i ω) (↑x : ℝ) =
    HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (pos ∘ X i) ω) (↑x : ℝ) -
      HDiv.hDiv (α := ℝ) (∑ i ∈ range x, (neg ∘ X i) ω) (↑x : ℝ)
Tactic: convert! hωpos.sub hωneg using 2