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)
N : ℕ
⊢ 0 ≤ HPow.hPow (β := ℕ) (c - 1)⁻¹ 3

Tactic:
exact pow_nonneg (inv_nonneg.2 (sub_nonneg.2 c_one.le)) _

Premises used: Iff.mpr, pow_nonneg, LT.lt.le, inv_nonneg, sub_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)
⊢ ∀ (N : ℕ),
    ∑ i ∈ range N,
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ ≤
      C

Tactic:
have I2 : ∀ N, ∑ i ∈ range N, ((u i : ℝ) ^ 2)⁻¹ * Var[S (u i)] ≤ C := by
    intro N
    calc
      ∑ i ∈ range N, ((u i : ℝ) ^ 2)⁻¹ * Var[S (u i)] =
          ∑ i ∈ range N, ((u i : ℝ) ^ 2)⁻¹ * ∑ j ∈ range (u i), Var[Y j] := by
        congr 1 with i
        congr 1
        rw [hS, IndepFun.variance_sum]
        · intro j _
          exact (hident j).aestronglyMeasurable_fst.memLp_truncation
        · intro k _ l _ hkl
          exact (hindep hkl).comp (A k).measurable (A l).measurable
      _ = ∑ j ∈ range (u (N - 1)), (∑ i ∈ range N with j < u i, ((u i : ℝ) ^ 2)⁻¹) * Var[Y j] := by
        simp_rw [mul_sum, sum_mul, sum_sigma']
        refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_
        · simp only [mem_sigma, mem_range, mem_filter, and_imp,
            Sigma.forall]
          exact fun a b haN hb ↦ ⟨hb.trans_le <| u_mono <| Nat.le_pred_of_lt haN, haN, hb⟩
        all_goals simp
      _ ≤ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j] := by
        gcongr ∑ _ ∈ _, ?_ with j
        rcases eq_zero_or_pos j with (rfl | hj)
        · simp only [Nat.cast_zero]
          simp only [Y, Nat.cast_zero, truncation_zero, variance_zero, mul_zero, le_rfl]
        apply mul_le_mul_of_nonneg_right _ (variance_nonneg _ _)
        convert! sum_div_nat_floor_pow_sq_le_div_sq N (Nat.cast_pos.2 hj) c_one using 2
        · simp only [u, Nat.cast_lt]
        · simp only [u, one_div]
      _ = c ^ 5 * (c - 1)⁻¹ ^ 3 * ∑ j ∈ range (u (N - 1)), ((j : ℝ) ^ 2)⁻¹ * Var[Y j] := by
        simp_rw [mul_sum, div_eq_mul_inv, mul_assoc]
      _ ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * 𝔼[X 0]) := by
        apply mul_le_mul_of_nonneg_left (I1 _)
        apply mul_nonneg (pow_nonneg c_pos.le _)
        exact pow_nonneg (inv_nonneg.2 (sub_nonneg.2 c_one.le)) _
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 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,
    ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          (↑(u i) : ℝ) * ε ≤ |S (u i) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u i) a|} ≤
      ENNReal.ofReal
        (variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2)
⊢ LE.le (α := ℝ≥0∞)
    (∑ i ∈ range N,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        {ω : Ω |
          (↑(u i) : ℝ) * ε ≤ |S (u i) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u i) a|})
    (∑ i ∈ range N,
      ENNReal.ofReal
        (variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2))

Tactic:
gcongr with 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
ε : ℝ
ε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_1 : i ∈ range N
h : MemLp (m0 := MeasureSpace.toMeasurableSpace) (S (u i)) 2 ℙ
h₁ : 0 < (↑(u i) : ℝ) * ε
⊢ ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      {ω : Ω |
        (↑(u i) : ℝ) * ε ≤ |S (u i) ω - @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ S (u i) a|} ≤
    ENNReal.ofReal
      (variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2)

Tactic:
apply meas_ge_le_variance_div_sq

Premises used: ProbabilityTheory.meas_ge_le_variance_div_sq
-- 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
⊢ MemLp (m0 := MeasureSpace.toMeasurableSpace) (S (u i)) 2 ℙ

Tactic:
memLp_finsetSum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation

Premises used: MeasureTheory.AEStronglyMeasurable.memLp_truncation, ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst, MeasureTheory.memLp_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) ℙ
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
⊢ MemLp (m0 := MeasureSpace.toMeasurableSpace) (S (u i)) 2 ℙ

Tactic:
exact memLp_finsetSum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation

Premises used: MeasureTheory.AEStronglyMeasurable.memLp_truncation, ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst, MeasureTheory.memLp_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) ℙ
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
apply : 0 < u i
⊢ 0 < (↑(u i) : ℝ) * ε

Tactic:
apply mul_pos (Nat.cast_pos.2 _) εpos

Premises used: Iff.mpr, Nat.cast_pos, mul_pos
-- 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 < u i

Tactic:
zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 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_1 : i ∈ range N
h : (↑1 : ℝ) ≤ c ^ i
⊢ 1 ≤ u i

Tactic:
apply Nat.le_floor

Premises used: Nat.le_floor
-- 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_1 : i ∈ range N
h : 1 ≤ c ^ i
⊢ (↑1 : ℝ) ≤ c ^ i

Tactic:
rw [Nat.cast_one]

Premises used: Nat.cast_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
ε : ℝ
ε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
⊢ 1 ≤ c ^ i

Tactic:
apply one_le_pow₀ c_one.le

Premises used: one_le_pow₀, LT.lt.le
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 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 : ℕ
rw :
  ∀ i ∈ range N,
    0 ≤ variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2
⊢ ∑ i ∈ range N,
      ENNReal.ofReal
        (variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2) =
    ENNReal.ofReal
      (∑ i ∈ range N,
        variance (mΩ := MeasureSpace.toMeasurableSpace) (S (u i)) ℙ / HPow.hPow (β := ℕ) ((↑(u i) : ℝ) * ε) 2)

Tactic:
rw [ENNReal.ofReal_sum_of_nonneg fun i _ => ?_]

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

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

Premises used: ProbabilityTheory.variance_nonneg, sq_nonneg, div_nonneg