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 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range n,
        HSub.hSub (α := ℝ)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 A)

Premises used: Iff.mpr, Asymptotics.isLittleO_sum_range_of_tendsto_zero, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
h :
  Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦
    ∑ i ∈ range n,
      HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    Nat.cast

Tactic:
convert! Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 A) using 1

Premises used: Iff.mpr, Asymptotics.isLittleO_sum_range_of_tendsto_zero, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
h :
  ∀ (n : ℕ),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
      ∑ i ∈ range n,
        HSub.hSub (α := ℝ)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
        HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦
    ∑ i ∈ range n,
      HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)

Tactic:
ext1 n
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
n : ℕ
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ ∑ c ∈ range n, truncation (X c) (↑c : ℝ) a)
    (∑ x ∈ range n, @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X x) (↑x : ℝ) a)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    ∑ i ∈ range n,
      HSub.hSub (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)

Tactic:
simp only [sum_sub_distrib, sum_const, card_range, nsmul_eq_mul, sum_apply, sub_left_inj]

Premises used: Finset.sum_apply, Finset.card_range, sub_left_inj, Finset.sum_sub_distrib, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
n : ℕ
rw : ∀ i ∈ range n, @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (truncation (X i) (↑i : ℝ)) ℙ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ ∑ c ∈ range n, truncation (X c) (↑c : ℝ) a)
    (∑ x ∈ range n, @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X x) (↑x : ℝ) a)

Tactic:
rw [integral_finsetSum _ fun i _ => ?_]

Premises used: MeasureTheory.integral_finsetSum
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
n i : ℕ
h : i ∈ range n
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (truncation (X i) (↑i : ℝ)) ℙ

Tactic:
((hident i).symm.integrable_snd hint).1.integrable_truncation

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.integrable_snd, And.left, MeasureTheory.AEStronglyMeasurable.integrable_truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
n i : ℕ
h : i ∈ range n
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (truncation (X i) (↑i : ℝ)) ℙ

Tactic:
exact ((hident i).symm.integrable_snd hint).1.integrable_truncation

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.integrable_snd, And.left, MeasureTheory.AEStronglyMeasurable.integrable_truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
h :
  ∀ (ω : Ω)
    (hω :
      IsLittleO (E := ℝ) (F := ℝ) atTop
        (fun (n : ℕ) ↦
          HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
        fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
          HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
      fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ ∀ᵐ (ω : Ω),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
          HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
      fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
filter_upwards [strong_law_aux2 X hint hindep hident hnonneg c_one] with ω hω

Premises used: ProbabilityTheory.strong_law_aux2
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop

Tactic:
have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
    tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a) +
        ((fun (n : ℕ) ↦
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                  (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
                HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
            fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
          x)
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
hω.add ((strong_law_aux3 X hint hident).comp_tendsto A)

Premises used: Asymptotics.IsLittleO.add, Asymptotics.IsLittleO.comp_tendsto, ProbabilityTheory.strong_law_aux3
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
h :
  Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (x : ℕ) ↦
    HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a) +
      ((fun (n : ℕ) ↦
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
              HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
convert! hω.add ((strong_law_aux3 X hint hident).comp_tendsto A) using 1

Premises used: Asymptotics.IsLittleO.add, Asymptotics.IsLittleO.comp_tendsto, ProbabilityTheory.strong_law_aux3
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
h :
  ∀ (n : ℕ),
    ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a) +
        ((fun (n : ℕ) ↦
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                  (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
                HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
            fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
          n
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (x : ℕ) ↦
    HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a) +
      ((fun (n : ℕ) ↦
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
              HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        x

Tactic:
ext1 n
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
n : ℕ
⊢ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a) +
      ((fun (n : ℕ) ↦
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range n, truncation (X i) (↑i : ℝ)) a) -
              HMul.hMul (α := ℝ) (↑n : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        n

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 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)})
    ∞

Tactic:
tsum_prob_mem_Ioi_lt_top hint (hnonneg 0)

Premises used: ProbabilityTheory.tsum_prob_mem_Ioi_lt_top, 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 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
h :
  Eq (α := ℕ → ℝ≥0∞)
    (fun (j : ℕ) ↦
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    fun (j : ℕ) ↦
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)}
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞

Tactic:
convert! tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2

Premises used: ProbabilityTheory.tsum_prob_mem_Ioi_lt_top, 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 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
h :
  ∀ (j : ℕ),
    Eq (α := ℝ≥0∞)
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)} : ℝ≥0∞)
      (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)} : ℝ≥0∞)
⊢ Eq (α := ℕ → ℝ≥0∞)
    (fun (j : ℕ) ↦
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    fun (j : ℕ) ↦
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)}

Tactic:
ext1 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 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
j : ℕ
⊢ Eq (α := ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)} : ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)} : ℝ≥0∞)

Tactic:
(hident j).measure_mem_eq measurableSet_Ioi

Premises used: measurableSet_Ioi, Set.preimage, ProbabilityTheory.IdentDistrib.measure_mem_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
j : ℕ
⊢ Eq (α := ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)} : ℝ≥0∞)
    (((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X 0 ω)} : ℝ≥0∞)

Tactic:
exact (hident j).measure_mem_eq measurableSet_Ioi

Premises used: measurableSet_Ioi, ProbabilityTheory.IdentDistrib.measure_mem_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞

Tactic:
have A : (∑' j : ℕ, ℙ {ω | X j ω ∈ Set.Ioi (j : ℝ)}) < ∞ := by
    convert! tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2
    ext1 j
    exact (hident j).measure_mem_eq measurableSet_Ioi
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
h :
  ∀ (ω : Ω) (hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)

Tactic:
filter_upwards [ae_eventually_notMem A.ne] with ω hω

Premises used: MeasureTheory.ae_eventually_notMem, LT.lt.ne
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
apply : EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr' _

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'