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 : ℕ
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 ∂ρ)
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑j : ℝ), 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: norm_cast
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
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)⁻¹ *
        ∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range K,
      HMul.hMul (α := ℝ) (∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹)
        (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ))
have simp_rw : Eq (α := ℝ)
  (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
      ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
        HPow.hPow (β := ℕ) x 2 ∂ρ)
  (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K,
    (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
      ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
        HPow.hPow (β := ℕ) x 2 ∂ρ)
Tactic: simp_rw [mul_sum, sum_mul, sum_sigma']
-- 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 (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
have refine_1 : ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K)
    ((fun (p : (_ : ℕ) × ℕ) ↦
        (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
      a)
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.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 ∂ρ)
refine_1 :
  ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K)
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a)
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
have refine_2 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K) a →
    (fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a ∈
      (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.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 ∂ρ)
refine_1 :
  ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K)
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K) a →
      (fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a ∈
        (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
have refine_3 : ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
  (fun (p : (_ : ℕ) × ℕ) ↦
        (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a) =
    a
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.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 ∂ρ)
refine_1 :
  ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K)
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K) a →
      (fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a ∈
        (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range
refine_3 :
  ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    (fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a) =
      a
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ)
have refine_4 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ioo a K) a →
    (fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a) =
      a
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.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 ∂ρ)
⊢ LE.le (α := ℝ)
    (∑ k ∈ range K,
      HMul.hMul (α := ℝ) (∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹)
        (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ))
    (∑ k ∈ range K,
      2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have h : ∀ k ∈ range K, LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
Tactic: gcongr with 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 ℙ
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 ∂ρ)
h : ∀ k ∈ range K, LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
⊢ LE.le (α := ℝ)
    (∑ k ∈ range K,
      HMul.hMul (α := ℝ) (∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹)
        (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ))
    (∑ k ∈ range K,
      2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have h₁ : ∀ k ∈ range K, ∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ ≤ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
Tactic: gcongr with 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 ℙ
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 ∂ρ)
k : ℕ
h : k ∈ range K
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
have h : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _
-- 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 ∂ρ)
⊢ LE.le (α := ℝ)
    (∑ k ∈ range K,
      2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range K, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ)
have h : ∀ k ∈ range K,
  2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ ≤
    ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ
Tactic: gcongr with k
-- 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 ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
k : ℕ
h : k ∈ range K
⊢ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ ≤
    ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ
have Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: have Ik : (k : ℝ) ≤ (k + 1 : ℕ) := by simp
-- 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 ∂ρ)
k : ℕ
h : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ ≤
    ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ
have h : LE.le (α := ℝ)
  (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ∂ρ)
  (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 * x ∂ρ)
Tactic: rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]
-- 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 ∂ρ)
k : ℕ
h : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ LE.le (α := ℝ)
    (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 * x ∂ρ)
have h : IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2)
  (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
-- 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 ∂ρ)
k : ℕ
h_1 : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
h :
  IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2)
    (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ
⊢ LE.le (α := ℝ)
    (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 * x ∂ρ)
have h₁ : IntegrableOn (HMul.hMul (α := ℝ) 2) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
-- 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 ∂ρ)
k : ℕ
h_1 : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
h :
  IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2)
    (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ
h₁ : IntegrableOn (HMul.hMul (α := ℝ) 2) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ
⊢ LE.le (α := ℝ)
    (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∫ (x : ℝ) in Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ), 2 * x ∂ρ)
have h₂ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) x),
  2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ≤ 2 * x
Tactic: refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
-- 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 ℙ
Y2 :
  ∀ (n : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y n) 2 a)
      (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
k : ℕ
h : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) x
⊢ x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x) ≤ 1 * (2 * x)
have this : 0 < x
Tactic: have : 0 < x := k.cast_nonneg.trans_lt hx.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 ∂ρ)
k : ℕ
h : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) x
this : 0 < x
⊢ x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x) ≤ 1 * (2 * x)
have hbc : x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ 1
Tactic: gcongr
-- 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 ∂ρ)
k : ℕ
h : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) x
⊢ 1 * (2 * x) = 2 * x
have rw : 2 * x = 2 * x
Tactic: rw [one_mul]
-- 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 ∂ρ)
k : ℕ
h : k ∈ range K
Ik : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) x
⊢ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ≤ 2 * x
have x₁ : 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 = x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x)
Tactic: calc
          2 / (↑k + 1) * x ^ 2 = x / (k + 1) * (2 * x) := by ring
          _ ≤ 1 * (2 * x) := by
              have : 0 < x := k.cast_nonneg.trans_lt hx.1
              gcongr
              exact (div_le_one <| by positivity).2 <| mod_cast hx.2
          _ = 2 * x := by rw [one_mul]