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) ℙ
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 ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
have apply : EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω
Tactic: apply tendsto_const_nhds.congr' _
-- 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 ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω
have h : ∀ (n : ℕ) (hn : X n ω ∉ Set.Ioi (↑n : ℝ)) (npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n),
  0 = truncation (X n) (↑n : ℝ) ω - X n ω
Tactic: filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos
-- 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 ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
⊢ 0 = truncation (X n) (↑n : ℝ) ω - X n ω
have h : 0 = (if -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ) then X n ω else 0) - X n ω
Tactic: simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]
-- 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 ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
⊢ 0 = (if -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ) then X n ω else 0) - X n ω
have pos : ∀ (h : -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ)), 0 = X n ω - X n ω
Tactic: split_ifs 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) ℙ
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 ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
pos : ∀ (h : -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ)), 0 = X n ω - X n ω
⊢ 0 = (if -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ) then X n ω else 0) - X n ω
have neg : ∀ (h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))), 0 = 0 - X n ω
Tactic: split_ifs 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) ℙ
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 ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
⊢ -(↑n : ℝ) < X n ω
have apply : LT.lt (α := ℝ) (-(↑n : ℝ)) 0
Tactic: apply lt_of_lt_of_le _ (hnonneg n ω)
-- 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 ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
⊢ 0 = 0 - X n ω
have this : -(↑n : ℝ) < X n ω
Tactic: have : -(n : ℝ) < X n ω := by
        apply lt_of_lt_of_le _ (hnonneg n ω)
        simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos
-- 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 ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
this : -(↑n : ℝ) < X n ω
⊢ 0 = 0 - X n ω
have h₁ : (↑n : ℝ) < X n ω
Tactic: simp only [this, true_and, not_le] at h
Cleared hypotheses: 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) ℙ
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 ω)})
    ∞
⊢ ∀ᵐ (ω : Ω),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
      fun (n : ℕ) ↦ (↑n : ℝ)
have B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
Tactic: have B : ∀ᵐ ω, Tendsto (fun n : ℕ => truncation (X n) n ω - X n ω) atTop (𝓝 0) := by
    filter_upwards [ae_eventually_notMem A.ne] with ω hω
    apply tendsto_const_nhds.congr' _
    filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos
    simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]
    split_ifs with h
    · exact (sub_self _).symm
    · have : -(n : ℝ) < X n ω := by
        apply lt_of_lt_of_le _ (hnonneg n ω)
        simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos
      simp only [this, true_and, not_le] at h
      exact (hn h).elim
-- 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 ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
      fun (n : ℕ) ↦ (↑n : ℝ)
have h : ∀ (ω : Ω) (hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)),
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
Tactic: filter_upwards [B] 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) ℙ
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 ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
have h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
  fun (n : ℕ) ↦ ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)
Tactic: convert! isLittleO_sum_range_of_tendsto_zero hω 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
    fun (n : ℕ) ↦ ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)
have h : ∀ (n : ℕ),
  HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω) =
    ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)
Tactic: ext 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 ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
n : ℕ
⊢ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω) =
    ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)
have h : HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω) =
  HSub.hSub (α := ℝ) (∑ x ∈ range n, truncation (X x) (↑x : ℝ) ω) (∑ x ∈ range n, X x ω)
Tactic: rw [sum_sub_distrib]
-- 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
n : ℕ
⊢ LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
have refine : LE.le (α := ℝ) 1 (↑⌊c ^ n⌋₊ : ℝ)
Tactic: refine zero_lt_one.trans_le ?_
-- 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
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
Tactic: have H : ∀ n : ℕ, (0 : ℝ) < ⌊c ^ n⌋₊ := by
    intro n
    refine zero_lt_one.trans_le ?_
    simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ c_one.le]
-- 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⌋₊ : ℝ)
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have h : ∀ (ω : Ω)
  (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 : ℝ)),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
Tactic: filter_upwards [strong_law_aux4 X hint hindep hident hnonneg c_one,
    strong_law_aux5 X hint hident hnonneg] with ω hω 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 : ℝ
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 : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
have h : 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
Tactic: rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ]
-- 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 : ∀ (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 : ℝ)
⊢ 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⌋₊ : ℝ)
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 : ∀ (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 : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ 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⌋₊ : ℝ)
have h : Eq (α := ℕ → ℝ)
  (fun (n : ℕ) ↦
    ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
  fun (x : ℕ) ↦
  ∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
    ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
        fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
      x
Tactic: convert! hω.sub (h'ω.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 : ∀ (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 : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (x : ℕ) ↦
    ∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
      ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        x
have h : ∀ (n : ℕ),
  ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
      ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        n
Tactic: ext1 n
-- 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 : ∀ (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 : ℝ)
⊢ 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 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⌋₊ : ℝ)
Tactic: have L : (fun n : ℕ => ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ⌊c ^ n⌋₊ * 𝔼[X 0]) =o[atTop] fun n =>
      (⌊c ^ n⌋₊ : ℝ) := by
    have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
      tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
    convert! hω.sub (h'ω.comp_tendsto A) using 1
    ext1 n
    simp only [Function.comp_apply, sub_sub_sub_cancel_left]