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
N i : ℕ
h : i ∈ range N
⊢ 0 ≤ variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2

Tactic:
exact div_nonneg (variance_nonneg _ _) (sq_nonneg _)

Premises used: ProbabilityTheory.variance_nonneg, sq_nonneg, div_nonneg
-- 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
N : ℕ
h :
  ∑ i ∈ range N, variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2 ≤
    HPow.hPow (β := ℕ) ε⁻¹ 2 * C
⊢ ENNReal.ofReal
      (∑ i ∈ range N,
        variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2) ≤
    ENNReal.ofReal (HPow.hPow (β := ℕ) ε⁻¹ 2 * C)

Tactic:
apply ENNReal.ofReal_le_ofReal

Premises used: ENNReal.ofReal_le_ofReal
-- 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
N : ℕ
h :
  HPow.hPow (β := ℕ) ε⁻¹ 2 *
      ∑ i ∈ range N,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ)⁻¹ 2 * variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ ≤
    HPow.hPow (β := ℕ) ε⁻¹ 2 * C
⊢ ∑ i ∈ range N, variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2 ≤
    HPow.hPow (β := ℕ) ε⁻¹ 2 * C

Tactic:
simp_rw [div_eq_inv_mul, ← inv_pow, mul_inv, mul_comm _ (ε⁻¹), mul_pow, mul_assoc,
          ← mul_sum]

Premises used: Finset.mul_sum, mul_inv, mul_assoc, inv_pow, Inv.inv, mul_comm, div_eq_inv_mul, mul_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 : ℝ
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
N : ℕ
h :
  ∑ i ∈ range N,
      HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ)⁻¹ 2 * variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ ≤
    C
⊢ HPow.hPow (β := ℕ) ε⁻¹ 2 *
      ∑ i ∈ range N,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ)⁻¹ 2 * variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ ≤
    HPow.hPow (β := ℕ) ε⁻¹ 2 * C

Tactic:
gcongr
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 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
N : ℕ
⊢ ∑ i ∈ range N,
      HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ)⁻¹ 2 * variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ ≤
    C

Tactic:
simpa only [inv_pow] using I2 N

Premises used: inv_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 : ℝ
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
⊢ ∀ (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)

Tactic:
have I3 : ∀ N, ∑ i ∈ range N, ℙ {ω | (u i * ε : ℝ) ≤ |S (u i) ω - 𝔼[S (u i)]|} ≤
      ENNReal.ofReal (ε⁻¹ ^ 2 * C) := by
    intro N
    calc
      ∑ i ∈ range N, ℙ {ω | (u i * ε : ℝ) ≤ |S (u i) ω - 𝔼[S (u i)]|} ≤
          ∑ i ∈ range N, ENNReal.ofReal (Var[S (u i)] / (u i * ε) ^ 2) := by
        gcongr with i _
        apply meas_ge_le_variance_div_sq
        · exact memLp_finsetSum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation
        · apply mul_pos (Nat.cast_pos.2 _) εpos
          refine zero_lt_one.trans_le ?_
          apply Nat.le_floor
          rw [Nat.cast_one]
          apply one_le_pow₀ c_one.le
      _ = ENNReal.ofReal (∑ i ∈ range N, Var[S (u i)] / (u i * ε) ^ 2) := by
        rw [ENNReal.ofReal_sum_of_nonneg fun i _ => ?_]
        exact div_nonneg (variance_nonneg _ _) (sq_nonneg _)
      _ ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C) := by
        apply ENNReal.ofReal_le_ofReal
        simp_rw [div_eq_inv_mul, ← inv_pow, mul_inv, mul_comm _ (ε⁻¹), mul_pow, mul_assoc,
          ← mul_sum]
        gcongr
        simpa only [inv_pow] using I2 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
ε : ℝ
ε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)
⊢ LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          (↑(u i) : ℝ) * ε ≤ |S (u i) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u i) a|})
    ∞

Tactic:
have I4 : (∑' i, ℙ {ω | (u i * ε : ℝ) ≤ |S (u i) ω - 𝔼[S (u i)]|}) < ∞ :=
    (le_of_tendsto_of_tendsto' (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds I3).trans_lt
      ENNReal.ofReal_lt_top
-- 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 :
  ∀ (ω : Ω)
    (hω :
      ∀ᶠ (n : ℕ) in atTop,
        ¬(↑(u n) : ℝ) * ε ≤ |S (u n) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u n) a|),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (range ⌊c ^ n⌋₊).sum Y a)| <
        ε * (↑⌊c ^ n⌋₊ : ℝ)
⊢ ∀ᵐ (ω : Ω),
    ∀ᶠ (n : ℕ) in atTop,
      |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (range ⌊c ^ n⌋₊).sum Y a)| <
        ε * (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
filter_upwards [ae_eventually_notMem I4.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) ℙ
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,
    ¬(↑(u n) : ℝ) * ε ≤ |S (u n) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u n) a|
⊢ ∀ᶠ (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) : ℝ)

Tactic:
simp_rw [S, not_le, mul_comm, sum_apply] at hω

Premises used: not_le, Finset.sum_apply, mul_comm
-- 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) : ℝ)
⊢ ∀ᶠ (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) : ℝ)

Tactic:
hω
-- 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) : ℝ)
h : ∀ (x : ℕ) (x_1 : Ω), (range ⌊c ^ x⌋₊).sum Y x_1 = ∑ c ∈ range (u x), Y c x_1
⊢ ∀ᶠ (n : ℕ) in atTop,
    |HSub.hSub (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ (range ⌊c ^ n⌋₊).sum Y a)| <
      ε * (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
convert! hω