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 ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j : ℕ
hj : j ∈ range K
⊢ Eq (α := ℝ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
have e_r : Eq (α := ℝ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
Tactic: rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
-- 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 ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have j : Eq (α := ℝ≥0∞)
  (∑ j ∈ range K,
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
  (∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ))
Tactic: calc
    ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
        ∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp_rw [B]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by
      simp [ENNReal.ofReal_sum_of_nonneg]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) := by
      congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
    _ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A
-- 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 ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j :
  Eq (α := ℝ≥0∞)
    (∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    (∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ))
⊢ ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have j₁ : ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
  ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
Tactic: calc
    ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
        ∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp_rw [B]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by
      simp [ENNReal.ofReal_sum_of_nonneg]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) := by
      congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
    _ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A
-- 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 ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A :
  ∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ ≤
    HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1
B :
  ∀ (a b : ℝ),
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
j :
  Eq (α := ℝ≥0∞)
    (∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    (∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ))
j₁ :
  ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ)
⊢ ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have j₂ : ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc (↑j : ℝ) (↑N : ℝ), 1 ∂ρ) =
  ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
Tactic: calc
    ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
        ∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp_rw [B]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by
      simp [ENNReal.ofReal_sum_of_nonneg]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) := by
      congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
    _ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A
-- 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 ℙ
hnonneg : 0 ≤ X
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ), ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)})
    ∞
have suffices : ∀ (K : ℕ),
  ∑ j ∈ range K, ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
Tactic: suffices ∀ K : ℕ, ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)} ≤ ENNReal.ofReal (𝔼[X] + 1) from
    (le_of_tendsto_of_tendsto (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds
      (Eventually.of_forall this)).trans_lt ENNReal.ofReal_lt_top
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    atTop
    (𝓝
      (∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)}))
have refine : ∀ i ∈ range K,
  Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
        ℝ≥0∞))
    atTop
    (𝓝 (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}) :
      Filter ℝ≥0∞)
Tactic: refine tendsto_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 ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
have apply : Subset.{u_1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
  (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
Tactic: apply Set.Subset.antisymm _ _
-- 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 ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
apply :
  Subset.{u_1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
have apply₁ : Subset.{u_1} (α := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
  {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
Tactic: apply Set.Subset.antisymm _ _
-- 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 ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
ω : Ω
hω : Membership.mem (γ := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)} ω
⊢ Membership.mem (γ := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}) ω
have obtain : ∀ (N : ℕ) (hN : X ω ≤ (↑N : ℝ)),
  Membership.mem (γ := Set Ω) (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}) ω
Tactic: obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
-- 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 ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
        ℝ≥0∞))
    atTop
    (𝓝 (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}) :
      Filter ℝ≥0∞)
have this : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
  (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
Tactic: have : {ω | X ω ∈ Set.Ioi (i : ℝ)} = ⋃ N : ℕ, {ω | X ω ∈ Set.Ioc (i : ℝ) N} := by
      apply Set.Subset.antisymm _ _
      · intro ω hω
        obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
        exact Set.mem_iUnion.2 ⟨N, hω, hN⟩
      · simp +contextual only [Set.mem_Ioc, Set.mem_Ioi,
          Set.iUnion_subset_iff, Set.setOf_subset_setOf, imp_true_iff]
-- 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 ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
        ℝ≥0∞))
    atTop
    (𝓝 (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}) :
      Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞)
  (fun (N : ℕ) ↦
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
      ℝ≥0∞))
  atTop
  (𝓝
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})) :
    Filter ℝ≥0∞)
Tactic: rw [this]
-- 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 ℙ
hnonneg : 0 ≤ X
K i : ℕ
h : i ∈ range K
this :
  Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑i : ℝ)) (X ω)}
    (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})
⊢ Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} :
        ℝ≥0∞))
    atTop
    (𝓝
        (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋃ (N : ℕ), {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)})) :
      Filter ℝ≥0∞)
have hm : Monotone.{0, u_1} (β := Set Ω) fun (N : ℕ) ↦ {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)}
Tactic: apply tendsto_measure_iUnion_atTop
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ ∑ j ∈ range K, ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have A : Tendsto (β := ℝ≥0∞)
  (fun (N : ℕ) ↦
    ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
  atTop
  (𝓝
    (∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)}))
Tactic: have A : Tendsto (fun N : ℕ => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N}) atTop
      (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)})) := by
    refine tendsto_finsetSum _ fun i _ => ?_
    have : {ω | X ω ∈ Set.Ioi (i : ℝ)} = ⋃ N : ℕ, {ω | X ω ∈ Set.Ioc (i : ℝ) N} := by
      apply Set.Subset.antisymm _ _
      · intro ω hω
        obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
        exact Set.mem_iUnion.2 ⟨N, hω, hN⟩
      · simp +contextual only [Set.mem_Ioc, Set.mem_Ioi,
          Set.iUnion_subset_iff, Set.setOf_subset_setOf, imp_true_iff]
    rw [this]
    apply tendsto_measure_iUnion_atTop
    intro m n hmn x hx
    exact ⟨hx.1, hx.2.trans (Nat.cast_le.2 hmn)⟩
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
A :
  Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    atTop
    (𝓝
      (∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)}))
⊢ ∑ j ∈ range K, ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have apply : EventuallyLE (β := ℝ≥0∞) atTop
  (fun (N : ℕ) ↦
    ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
  fun (x : ℕ) ↦
  ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
Tactic: apply le_of_tendsto_of_tendsto A tendsto_const_nhds
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
A :
  Tendsto (β := ℝ≥0∞)
    (fun (N : ℕ) ↦
      ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    atTop
    (𝓝
      (∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X ω)}))
⊢ EventuallyLE (β := ℝ≥0∞) atTop
    (fun (N : ℕ) ↦
      ∑ j ∈ range K,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)})
    fun (x : ℕ) ↦
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have h : ∀ (N : ℕ) (hN : N ∈ Set.Ici K),
  ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
Tactic: filter_upwards [Ici_mem_atTop K] 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
n : ℕ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (fun (x : Ω) ↦ HPow.hPow (β := ℕ) (Y n x) 2) a)
    (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have rw : Eq (α := ℝ) (∫ (y : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) y 2 ∂Measure.map X ℙ)
  (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
Tactic: rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
⊢ (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          HPow.hPow (β := ℕ) (truncation X (↑j : ℝ)) 2 a) ≤
    HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a)
have Y2 : ∀ (n : ℕ),
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
    (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
Tactic: have Y2 : ∀ n, 𝔼[Y n ^ 2] = ∫ x in 0..n, x ^ 2 ∂ρ := by
    intro n
    change 𝔼[fun x => Y n x ^ 2] = _
    rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
⊢ Eq (α := ℝ)
    (∑ j ∈ range K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * ∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        ∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have e_f : ∀ (j : ℕ),
  (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * ∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ =
    (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
      ∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ
Tactic: congr 1 with j
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j : ℕ
⊢ (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * ∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ =
    (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
      ∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ
have e_f : Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
  (∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
Tactic: congr 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j : ℕ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have e_f : Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
  (∫ (x : ℝ) in (↑0 : ℝ)..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
Tactic: rw [intervalIntegral.sum_integral_adjacent_intervals]
-- 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 ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation X (↑n : ℝ)
ρ : Measure ℝ := Measure.map X ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
j : ℕ
e_f :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have e_f₁ : ∀ k < j, IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: rw [intervalIntegral.sum_integral_adjacent_intervals]