awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)
⊢ ∀ a ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) range,
    (HPow.hPow (α := ℝ) (β := ℕ) (↑(a.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ) 2)⁻¹ *
        ∫ (x : ℝ) in (↑(a.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(a.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ =
      (HPow.hPow (α := ℝ) (β := ℕ)
            (↑(Sigma.snd (β := fun (i : ℕ) ↦ ℕ)
                  ((fun (p : (_ : ℕ) × ℕ) ↦
                      (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                        (_ : ℕ) × ℕ))
                    a)) :
              ℝ)
            2)⁻¹ *
        ∫ (x : ℝ) in
          (↑(Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
                ((fun (p : (_ : ℕ) × ℕ) ↦
                    (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                      (_ : ℕ) × ℕ))
                  a)) :
            ℝ)..(↑(HAdd.hAdd (α := ℕ)
                (Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
                  ((fun (p : (_ : ℕ) × ℕ) ↦
                      (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
                        (_ : ℕ) × ℕ))
                    a))
                1) :
            ℝ),
          HPow.hPow (β := ℕ) x 2 ∂ρ

Tactic:
aesop (add unsafe lt_trans)

Premises used: lt_trans
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)
h₁ : ∀ k ∈ range K, ∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ ≤ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ 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 ∂ρ)

Tactic:
gcongr with k
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)

Tactic:
intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _

Premises used: sq_nonneg, intervalIntegral.integral_nonneg_of_forall
-- Module: Mathlib.Probability.StrongLaw
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
h : LE.le (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)

Tactic:
refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _

Premises used: sq_nonneg, intervalIntegral.integral_nonneg_of_forall
-- Module: Mathlib.Probability.StrongLaw
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 (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.StrongLaw
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
⊢ ∑ j ∈ Ioo k K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ ≤ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
apply sum_Ioo_inv_sq_le

Premises used: sum_Ioo_inv_sq_le
-- Module: Mathlib.Probability.StrongLaw
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,
    2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ ≤
      ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ
⊢ 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 ∂ρ)

Tactic:
gcongr with k
-- Module: Mathlib.Probability.StrongLaw
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 (α := ℝ) (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
have Ik : (k : ℝ) ≤ (k + 1 : ℕ) := by simp
-- Module: Mathlib.Probability.StrongLaw
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 :
  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 ∂ρ)
⊢ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ ≤
    ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ

Tactic:
rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]

Premises used: intervalIntegral.integral_of_le, intervalIntegral.integral_const_mul
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)

Tactic:
setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_

Premises used: measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.Probability.StrongLaw
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) : ℝ)) ρ
h₂ :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) x),
    2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ≤ 2 * x
⊢ 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:
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_

Premises used: measurableSet_Ioc, MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.Probability.StrongLaw
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) : ℝ)
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2

Tactic:
fun_prop
-- Module: Mathlib.Probability.StrongLaw
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) : ℝ)
⊢ IntegrableOn (ε := ℝ) (fun (x : ℝ) ↦ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2)
    (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ

Tactic:
apply Continuous.integrableOn_Ioc (by fun_prop)

Premises used: Continuous.integrableOn_Ioc
-- Module: Mathlib.Probability.StrongLaw
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) : ℝ)
⊢ Continuous (X := ℝ) (HMul.hMul (α := ℝ) 2)

Tactic:
fun_prop
-- Module: Mathlib.Probability.StrongLaw
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) : ℝ)
⊢ IntegrableOn (HMul.hMul (α := ℝ) 2) (Set.Ioc (↑k : ℝ) (↑(k + 1) : ℝ)) ρ

Tactic:
apply Continuous.integrableOn_Ioc (by fun_prop)

Premises used: Continuous.integrableOn_Ioc
-- Module: Mathlib.Probability.StrongLaw
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 = x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x)

Tactic:
ring
-- Module: Mathlib.Probability.StrongLaw
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
⊢ 0 < x

Tactic:
have : 0 < x := k.cast_nonneg.trans_lt hx.1
-- Module: Mathlib.Probability.StrongLaw
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
hbc : x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ 1
⊢ x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x) ≤ 1 * (2 * x)

Tactic:
gcongr
-- Module: Mathlib.Probability.StrongLaw
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
⊢ 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Probability.StrongLaw
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 ≤ 1

Tactic:
exact (div_le_one <| by positivity).2 <| mod_cast hx.2

Premises used: Iff.mpr, div_le_one, And.right
-- Module: Mathlib.Probability.StrongLaw
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
rw rw₁ : 2 * x = 2 * x
⊢ 1 * (2 * x) = 2 * x

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Probability.StrongLaw
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₁ : 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 = x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x)
x₂ : x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (2 * x) ≤ 1 * (2 * x)
x₃ : 1 * (2 * x) = 2 * x
⊢ 2 / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * HPow.hPow (β := ℕ) x 2 ≤ 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]

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)
rw : ∫ (x : ℝ) in (↑0 : ℝ)..(↑K : ℝ), 2 * x ∂ρ = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)
rw₁ : ∀ k < K, IntervalIntegrable (HMul.hMul (α := ℝ) 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ ∑ k ∈ range K, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), 2 * x ∂ρ = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]

Premises used: intervalIntegral.sum_integral_adjacent_intervals
-- Module: Mathlib.Probability.StrongLaw
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 < K
⊢ IntervalIntegrable (HMul.hMul (α := ℝ) 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
(continuous_const.mul continuous_id').intervalIntegrable _ _

Premises used: continuous_const, continuous_id', Continuous.intervalIntegrable, Continuous.mul
-- Module: Mathlib.Probability.StrongLaw
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 < K
⊢ IntervalIntegrable (HMul.hMul (α := ℝ) 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
exact (continuous_const.mul continuous_id').intervalIntegrable _ _

Premises used: continuous_const, continuous_id', Continuous.intervalIntegrable, Continuous.mul
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)
rw :
  HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in (↑0 : ℝ)..(↑K : ℝ), x ∂ρ) = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)
⊢ ∫ (x : ℝ) in (↑0 : ℝ)..(↑K : ℝ), 2 * x ∂ρ = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)

Tactic:
rw [intervalIntegral.integral_const_mul]

Premises used: intervalIntegral.integral_const_mul
-- Module: Mathlib.Probability.StrongLaw
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 ∂ρ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ) = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)
⊢ HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in (↑0 : ℝ)..(↑K : ℝ), x ∂ρ) = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..(↑K : ℝ), x ∂ρ)

Tactic:
norm_cast