awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
linarith : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₁ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ ε / 4 + ε / 4 + ε / 4 < ε
have linarith₆ : ε ≤ ε / 4 + ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
linarith : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₁ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε ≤ ε / 4 + ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε ≤ ε / 4 + ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
⊢ ε / 4 + ε / 4 + ε / 4 < ε
have linarith₇ : ε ≤ ε / 4 + ε / 4 + ε / 4 → 0 - ε + (4 * ε - (1 * ε + 1 * ε + 1 * ε)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
have h : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : δ + δ + δ < ε),
  ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
Tactic: obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ δ + δ + δ < ε := ⟨ε/4, by positivity, by linarith⟩
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
⊢ ∃ (k : ℕ), ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
have simp_rw : ∃ (k : ℕ), ∫ (ω : Ω), ‖Y k 0 ω - X 0 ω‖ ∂μ < δ
Tactic: simp_rw [Pi.sub_apply, norm_sub_rev (X 0 _)]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
⊢ ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
have h : ∀ (k : ℕ) (hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ),
  ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
Tactic: obtain ⟨k, hk⟩ : ∃ k, ∫ ω, ‖(X 0 - Y k 0) ω‖ ∂μ < δ := by
    simp_rw [Pi.sub_apply, norm_sub_rev (X 0 _)]
    exact ((tendsto_order.1 (tendsto_integral_norm_approxOn_sub h'.measurable hint)).2 δ
      δpos).exists
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
⊢ ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
have rw : norm.{u_2} (E := E) (∫ (a : Ω), X 0 a - Y k 0 a ∂μ) < δ
Tactic: rw [norm_sub_rev, ← integral_sub hint]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
rw : norm.{u_2} (E := E) (∫ (a : Ω), X 0 a - Y k 0 a ∂μ) < δ
⊢ ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
have rw₁ : Integrable (Y k 0) μ
Tactic: rw [norm_sub_rev, ← integral_sub hint]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
⊢ ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
have this₁ : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
Tactic: have : ‖μ[Y k 0] - μ[X 0]‖ < δ := by
    rw [norm_sub_rev, ← integral_sub hint]
    · exact (norm_integral_le_integral_norm _).trans_lt hk
    · exact ((φ k).comp (X 0) h'.measurable).integrable_of_isFiniteMeasure
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
⊢ ∀ᶠ (b : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑b : ℝ)⁻¹ (∑ i ∈ Finset.range b, X i ω) - ∫ (x : Ω), X 0 x ∂μ‖ < ε
have I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
Tactic: have I : ∀ᶠ n in atTop, (∑ i ∈ range n, ‖(X i - Y k i) ω‖) / n < δ :=
    (tendsto_order.1 (h'ω k)).2 δ hk
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω :
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
⊢ ∀ᶠ (n : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
have hω₁ : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω)) atTop
  (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
Tactic: specialize hω k
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this_2 : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
h'ω :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖HSub.hSub (α := E) (∫ (x : Ω), Y k 0 x ∂μ) (∫ (x : Ω), X 0 x ∂μ)‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ) < δ
hω :
  Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
    atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
⊢ ∀ᶠ (n : ℕ) in atTop,
    ‖HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
have hω₁ : Tendsto (β := ℝ)
  (fun (e : ℕ) ↦ ‖HSMul.hSMul (α := ℝ) (β := E) (↑e : ℝ)⁻¹ (∑ i ∈ Finset.range e, Y k i ω) - ∫ (x : Ω), Y k 0 x ∂μ‖)
  atTop (𝓝 0)
Tactic: rw [tendsto_iff_norm_sub_tendsto_zero] at hω
Cleared hypotheses: hω