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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ)
S : (n : ℕ) → Ω → ℝ := fun (n : ℕ) ↦ ∑ i ∈ range n, Y i
hS : S = fun (n : ℕ) ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun (n : ℕ) ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 :
  ∀ (K : ℕ),
    ∑ j ∈ range K,
        (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
      HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
C : ℝ :=
  HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
    HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
I2 :
  ∀ (N : ℕ),
    ∑ i ∈ range N,
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ ≤
      C
I3 :
  ∀ (N : ℕ),
    ∑ i ∈ range N,
        ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          {ω : Ω |
            (↑(u i) : ℝ) * ε ≤
              |S (u i) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u i) a|} ≤
      ENNReal.ofReal (HPow.hPow (β := ℕ) ε⁻¹ 2 * C)
I4 :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          (↑(u i) : ℝ) * ε ≤ |S (u i) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u i) a|})
    ∞
ω : Ω
hω :
  ∀ᶠ (n : ℕ) in atTop,
    |HSub.hSub (α := ℝ) (∑ c ∈ range (u n), Y c ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ ∑ c ∈ range (u n), Y c a)| <
      ε * (↑(u n) : ℝ)
x : ℕ
x_1 : Ω
⊢ (range ⌊c ^ x⌋₊).sum Y x_1 = ∑ c ∈ range (u x), Y c x_1

Tactic:
simp only [Y, u, sum_apply]

Premises used: Finset.sum_apply
-- 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
⊢ ∃ (v : ℕ → ℝ), StrictAnti v ∧ (∀ (n : ℕ), 0 < v n) ∧ Tendsto v atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ)

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 : ℝ
c_one : 1 < c
obtain :
  ∀ (v : ℕ → ℝ) (v_pos : ∀ (n : ℕ), 0 < v n) (v_lim : Tendsto v atTop (𝓝 0)),
    ∀ᵐ (ω : Ω),
      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 : ℕ) ↦
        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⌋₊ : ℝ)

Tactic:
obtain ⟨v, -, v_pos, v_lim⟩ :
      ∃ v : ℕ → ℝ, StrictAnti v ∧ (∀ n : ℕ, 0 < v n) ∧ Tendsto v atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

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 : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
⊢ ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
have := fun i => strong_law_aux1 X hint hindep hident hnonneg c_one (v_pos i)
-- 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
h :
  ∀ (ω : Ω)
    (hω :
      ∀ (i : ℕ),
        ∀ᶠ (n : ℕ) in atTop,
          |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
                (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                  (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
            v i * (↑⌊c ^ n⌋₊ : ℝ)),
    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 : ℕ) ↦
        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⌋₊ : ℝ)

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 : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
apply :
  ∀ (ε : ℝ) (εpos : 0 < ε),
    ∀ᶠ (x : ℕ) in atTop,
      ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
        ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)
⊢ 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⌋₊ : ℝ)

Tactic:
apply Asymptotics.isLittleO_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Asymptotics.isLittleO_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 : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
⊢ ∃ (i : ℕ), v i < ε

Tactic:
((tendsto_order.1 v_lim).2 ε εpos).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
obtain :
  ∀ (i : ℕ) (hi : v i < ε),
    ∀ᶠ (x : ℕ) in atTop,
      ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
        ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
      ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)

Tactic:
obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
h :
  ∀ (n : ℕ)
    (hn :
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ 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)‖ ≤
      ε * norm (E := ℝ) (↑⌊c ^ n⌋₊ : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
            (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i : ℝ)) a)‖ ≤
      ε * norm (E := ℝ) (↑⌊c ^ x⌋₊ : ℝ)

Tactic:
filter_upwards [hω i] with n hn
-- 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
n : ℕ
hn :
  |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
    v i * (↑⌊c ^ n⌋₊ : ℝ)
h :
  |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| ≤
    ε * (↑⌊c ^ 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)‖ ≤
    ε * norm (E := ℝ) (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
simp only [Real.norm_eq_abs, Nat.abs_cast]

Premises used: Nat.abs_cast, Real.norm_eq_abs
-- 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
n : ℕ
hn :
  |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
    v i * (↑⌊c ^ 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)| ≤
    ε * (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))

Premises used: Nat.cast_nonneg, LT.lt.le, mul_le_mul_of_nonneg_right, 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 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
              (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
                (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
          v i * (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
              (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
        v i * (↑⌊c ^ n⌋₊ : ℝ)
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
n : ℕ
hn :
  |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦
          (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ)) a)| <
    v i * (↑⌊c ^ 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)| ≤
    ε * (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))

Premises used: Nat.cast_nonneg, LT.lt.le, mul_le_mul_of_nonneg_right, 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 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ Tendsto (β := ℝ)
    ((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
    atTop (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ X 0 x))

Tactic:
(tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop

Premises used: ProbabilityTheory.tendsto_integral_truncation, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- 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) ℙ ℙ
h :
  Eq (α := ℕ → ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
    ((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
convert! (tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop using 1

Premises used: ProbabilityTheory.tendsto_integral_truncation, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- 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) ℙ ℙ
h :
  ∀ (i : ℕ),
    Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
      (((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘
          Nat.cast)
        i)
⊢ Eq (α := ℕ → ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
    ((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)

Tactic:
ext i
-- 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) ℙ ℙ
i : ℕ
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
    (((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
      i)

Tactic:
(hident i).truncation.integral_eq

Premises used: ProbabilityTheory.IdentDistrib.truncation, ProbabilityTheory.IdentDistrib.integral_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) ℙ ℙ
i : ℕ
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a)
    (((fun (A : ℝ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : Ω) ↦ truncation (X 0) A x) ∘ Nat.cast)
      i)

Tactic:
exact (hident i).truncation.integral_eq

Premises used: ProbabilityTheory.IdentDistrib.truncation, ProbabilityTheory.IdentDistrib.integral_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) ℙ ℙ
⊢ Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ truncation (X i) (↑i : ℝ) a) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
have A : Tendsto (fun i => 𝔼[truncation (X i) i]) atTop (𝓝 𝔼[X 0]) := by
    convert! (tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop using 1
    ext i
    exact (hident i).truncation.integral_eq