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) ℙ
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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
h :
  Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (x : ℕ) ↦
    ∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
      ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        x
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
convert! hω.sub (h'ω.comp_tendsto A) using 1

Premises used: Asymptotics.IsLittleO.comp_tendsto, Asymptotics.IsLittleO.sub
-- 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
h :
  ∀ (n : ℕ),
    ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
          HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
        ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
            fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
          n
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (x : ℕ) ↦
    ∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
      ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
          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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
A : Tendsto (β := ℕ) (fun (n : ℕ) ↦ ⌊c ^ n⌋₊) atTop atTop
n : ℕ
⊢ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
      HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) -
      ((fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) ∘
          fun (n : ℕ) ↦ ⌊c ^ n⌋₊)
        n

Tactic:
simp only [Function.comp_apply, sub_sub_sub_cancel_left]

Premises used: Function.comp_apply, sub_sub_sub_cancel_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 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
have L : (fun n : ℕ => ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ⌊c ^ n⌋₊ * 𝔼[X 0]) =o[atTop] fun n =>
      (⌊c ^ n⌋₊ : ℝ) := by
    have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
      tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
    convert! hω.sub (h'ω.comp_tendsto A) using 1
    ext1 n
    simp only [Function.comp_apply, sub_sub_sub_cancel_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 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦
      (∑ i ∈ range ⌊c ^ x⌋₊, X i ω -
          HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
        (↑⌊c ^ x⌋₊ : ℝ)⁻¹)
    fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (↑⌊c ^ x⌋₊ : ℝ)⁻¹

Tactic:
L.mul_isBigO (isBigO_refl (fun n : ℕ => (⌊c ^ n⌋₊ : ℝ)⁻¹) atTop)

Premises used: Nat.cast, Filter.atTop, Inv.inv, HPow.hPow, Nat.floor, Asymptotics.IsLittleO.mul_isBigO, Asymptotics.isBigO_refl
-- 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
h :
  Eq (α := ℕ → ℝ)
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (x : ℕ) ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
      (↑⌊c ^ x⌋₊ : ℝ)⁻¹
h₁ : Eq (α := ℕ → ℝ) (fun (_x : ℕ) ↦ 1) fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (↑⌊c ^ x⌋₊ : ℝ)⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (_x : ℕ) ↦ 1

Tactic:
convert! L.mul_isBigO (isBigO_refl (fun n : ℕ => (⌊c ^ n⌋₊ : ℝ)⁻¹) atTop) using 1

Premises used: Nat.cast, Filter.atTop, Inv.inv, HPow.hPow, Nat.floor, Asymptotics.IsLittleO.mul_isBigO, Asymptotics.isBigO_refl
-- 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
h :
  ∀ (n : ℕ),
    (HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
      (∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
          HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
        (↑⌊c ^ n⌋₊ : ℝ)⁻¹
⊢ Eq (α := ℕ → ℝ)
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (x : ℕ) ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
      (↑⌊c ^ 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
n : ℕ
⊢ (HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ) -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a) =
    (∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)) *
      (↑⌊c ^ n⌋₊ : ℝ)⁻¹

Tactic:
field [(H n).ne']

Premises used: 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) ℙ
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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
h : ∀ (n : ℕ), 1 = HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (↑⌊c ^ n⌋₊ : ℝ)⁻¹
⊢ Eq (α := ℕ → ℝ) (fun (_x : ℕ) ↦ 1) fun (x : ℕ) ↦ HMul.hMul (α := ℝ) (↑⌊c ^ x⌋₊ : ℝ) (↑⌊c ^ 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 : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  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⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
L :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, X i ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
n : ℕ
⊢ 1 = HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (↑⌊c ^ n⌋₊ : ℝ)⁻¹

Tactic:
field [(H n).ne']

Premises used: 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) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∃ (c : ℕ → ℝ), StrictAnti c ∧ (∀ (n : ℕ), 1 < c n) ∧ Tendsto c atTop (𝓝 1)

Tactic:
exists_seq_strictAnti_tendsto (1 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, 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) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
obtain :
  ∀ (c : ℕ → ℝ) (cone : ∀ (n : ℕ), 1 < c n) (clim : Tendsto c atTop (𝓝 1)),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
obtain ⟨c, -, cone, clim⟩ :
      ∃ c : ℕ → ℝ, StrictAnti c ∧ (∀ n : ℕ, 1 < c n) ∧ Tendsto c atTop (𝓝 1) :=
    exists_seq_strictAnti_tendsto (1 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, 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) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
⊢ ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
have : ∀ k, ∀ᵐ ω,
      Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ⌊c k ^ n⌋₊) atTop (𝓝 𝔼[X 0]) :=
    fun k => strong_law_aux6 X hint hindep hident hnonneg (cone 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 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
h :
  ∀ (ω : Ω)
    (hω :
      ∀ (i : ℕ),
        Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
          (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
filter_upwards [ae_all_iff.2 this] with ω hω

Premises used: Iff.mpr, MeasureTheory.ae_all_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) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
ω : Ω
hω :
  ∀ (i : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
apply : Monotone (β := ℝ) fun (n : ℕ) ↦ ∑ i ∈ range n, X i ω
apply₁ :
  ∀ (k : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range n, X i ω) (↑n : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
apply tendsto_div_of_monotone_of_tendsto_div_floor_pow _ _ _ c cone clim _

Premises used: tendsto_div_of_monotone_of_tendsto_div_floor_pow
-- 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 : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ),
    ∀ᵐ (ω : Ω),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) (↑⌊c k ^ n⌋₊ : ℝ)) atTop
        (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
ω : Ω
hω :
  ∀ (i : ℕ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) (↑⌊c i ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
m n : ℕ
hmn : m ≤ n
⊢ LE.le (α := ℝ) ((fun (n : ℕ) ↦ (∑ i ∈ range n, X i ω : ℝ)) m) ((fun (n : ℕ) ↦ (∑ i ∈ range n, X i ω : ℝ)) n)

Tactic:
sum_le_sum_of_subset_of_nonneg (range_mono hmn) fun i _ _ => hnonneg i ω

Premises used: Finset.sum_le_sum_of_subset_of_nonneg, Finset.range_mono