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 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 ω)})
hm :
  Monotone.{0, u_1} (β := Set Ω) fun (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∞)

Tactic:
apply tendsto_measure_iUnion_atTop

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop
-- 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 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 ω)})
m n : ℕ
hmn : m ≤ n
x : Ω
hx :
  Membership.mem (γ := Set Ω)
    ((fun (N : ℕ) ↦ ({ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} : Set Ω)) m) x
⊢ Membership.mem (γ := Set Ω)
    ((fun (N : ℕ) ↦ ({ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} : Set Ω)) n) x

Tactic:
⟨hx.1, hx.2.trans (Nat.cast_le.2 hmn)⟩

Premises used: Iff.mpr, Set.Ioc, Set.Mem, setOf, And.right, And.left, And.intro, Nat.cast_le, LE.le.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 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 ω)})
m n : ℕ
hmn : m ≤ n
x : Ω
hx :
  Membership.mem (γ := Set Ω)
    ((fun (N : ℕ) ↦ ({ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} : Set Ω)) m) x
⊢ Membership.mem (γ := Set Ω)
    ((fun (N : ℕ) ↦ ({ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑i : ℝ) (↑N : ℝ)) (X ω)} : Set Ω)) n) x

Tactic:
exact ⟨hx.1, hx.2.trans (Nat.cast_le.2 hmn)⟩
-- 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 : ℕ
⊢ 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)⟩
-- 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 : ℕ
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 ω)}))
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)
⊢ ∑ 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:
apply le_of_tendsto_of_tendsto A tendsto_const_nhds

Premises used: tendsto_const_nhds, le_of_tendsto_of_tendsto
-- 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 : ℕ
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 ω)}))
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)
⊢ 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:
filter_upwards [Ici_mem_atTop K] with N hN

Premises used: Filter.Ici_mem_atTop
-- 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 : ℕ
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 ω)}))
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:
sum_prob_mem_Ioc_le hint hnonneg hN

Premises used: ProbabilityTheory.sum_prob_mem_Ioc_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 : ℕ
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 ω)}))
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:
exact sum_prob_mem_Ioc_le hint hnonneg hN

Premises used: ProbabilityTheory.sum_prob_mem_Ioc_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 ℙ
n : ℕ
rw rw₁ :
  Eq (α := ℝ) (∫ (y : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) y 2 ∂Measure.map X ℙ)
    (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (fun (x : Ω) ↦ HPow.hPow (β := ℕ) (Y n x) 2) a)
    (∫ (x : ℝ) in 0..(↑n : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)

Tactic:
rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]

Premises used: ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg, two_ne_zero, And.left
-- 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 ℙ
⊢ ∀ (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]
-- 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 ∂ρ)
⊢ Eq (α := ℝ)
    (∑ j ∈ range K,
      (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ HPow.hPow (β := ℕ) (Y j) 2 a)
    (∑ j ∈ range K, (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * ∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)

Tactic:
simp_rw [Y2]
-- 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 ∂ρ)
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 ∂ρ
⊢ 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 ∂ρ)

Tactic:
congr 1 with j
-- 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 ∂ρ)
j : ℕ
e_f :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
⊢ (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
-- 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 ∂ρ)
j : ℕ
e_f :
  Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
e_f₁ : ∀ k < j, IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)
    (∑ k ∈ range j, ∫ (x : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals]

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 ∂ρ)
j : ℕ
e_f e_f₁ e_f₂ 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 ∂ρ)
    (∫ (x : ℝ) in (↑0 : ℝ)..(↑j : ℝ), HPow.hPow (β := ℕ) x 2 ∂ρ)

Tactic:
norm_cast
-- 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 ∂ρ)
j k : ℕ
e_f : k < j → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
⊢ k < j → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
_
-- 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 ∂ρ)
j k : ℕ
h : k < j
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
(continuous_id.pow _).intervalIntegrable _ _

Premises used: Continuous.pow, Continuous.intervalIntegrable, continuous_id
-- 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 ∂ρ)
j k : ℕ
h : k < j
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ρ (↑k : ℝ) (↑(k + 1) : ℝ)

Tactic:
exact (continuous_id.pow _).intervalIntegrable _ _

Premises used: Continuous.pow, Continuous.intervalIntegrable, continuous_id
-- 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 ∂ρ)
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 ∂ρ)
⊢ 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 ∂ρ))

Tactic:
simp_rw [mul_sum, sum_mul, sum_sigma']

Premises used: Finset.mul_sum, Finset.sum_sigma', Finset.sum_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 ∂ρ)
⊢ 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:
sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_

Premises used: Sigma.fst, Sigma.mk, Sigma.snd, Finset.sum_nbij'
-- 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,
    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:
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 ∂ρ)
⊢ ∀ (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:
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 ∂ρ)
⊢ ∀ 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:
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 ∂ρ)
⊢ ∀ (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:
aesop (add unsafe lt_trans)

Premises used: lt_trans