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 : ℕ
h :
  ∀ j ∈ range (u (N - 1)),
    (∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ
⊢ LE.le (α := ℝ)
    (∑ j ∈ range (u (N - 1)),
      (∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ)
    (∑ j ∈ range (u (N - 1)),
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ)

Tactic:
gcongr ∑ _ ∈ _, ?_ with j
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
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 j : ℕ
h_1 : j ∈ range (u (N - 1))
h :
  0 ∈ range (u (N - 1)) →
    (∑ i ∈ range N with 0 < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ ≤
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ
h₁ :
  ∀ (hj : 0 < j),
    (∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ
⊢ (∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ

Tactic:
rcases eq_zero_or_pos j with (rfl | hj)

Premises used: eq_zero_or_pos, rfl
-- 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 : ℕ
h_1 : 0 ∈ range (u (N - 1))
h :
  (∑ i ∈ range N with 0 < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) 0 2 *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ
⊢ (∑ i ∈ range N with 0 < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑0 : ℝ) 2 *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ

Tactic:
simp only [Nat.cast_zero]

Premises used: Nat.cast_zero
-- 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 : ℕ
h : 0 ∈ range (u (N - 1))
⊢ (∑ i ∈ range N with 0 < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) 0 2 *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y 0) ℙ

Tactic:
simp only [Y, Nat.cast_zero, truncation_zero, variance_zero, mul_zero, le_rfl]

Premises used: le_rfl, ProbabilityTheory.variance_zero, MulZeroClass.mul_zero, Nat.cast_zero, ProbabilityTheory.truncation_zero
-- 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 j : ℕ
h : j ∈ range (u (N - 1))
hj : 0 < j
apply :
  ∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2
⊢ (∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹) *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
      variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ

Tactic:
apply mul_le_mul_of_nonneg_right _ (variance_nonneg _ _)

Premises used: ProbabilityTheory.variance_nonneg, mul_le_mul_of_nonneg_right
-- 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 j : ℕ
h : j ∈ range (u (N - 1))
hj : 0 < j
⊢ ∑ i ∈ range N with LT.lt (α := ℝ) (↑j : ℝ) (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2

Tactic:
sum_div_nat_floor_pow_sq_le_div_sq N (Nat.cast_pos.2 hj) c_one

Premises used: Iff.mpr, Nat.cast_pos, sum_div_nat_floor_pow_sq_le_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)
N j : ℕ
h_1 : j ∈ range (u (N - 1))
hj : 0 < j
h : {i ∈ range N | j < u i} = {i ∈ range N | LT.lt (α := ℝ) (↑j : ℝ) (↑⌊c ^ i⌋₊ : ℝ)}
h₁ :
  ∀ x ∈ {i ∈ range N | LT.lt (α := ℝ) (↑j : ℝ) (↑⌊c ^ i⌋₊ : ℝ)},
    (HPow.hPow (α := ℝ) (β := ℕ) (↑(u x) : ℝ) 2)⁻¹ = 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ x⌋₊ : ℝ) 2
⊢ ∑ i ∈ range N with j < u i, (HPow.hPow (α := ℝ) (β := ℕ) (↑(u i) : ℝ) 2)⁻¹ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2

Tactic:
convert! sum_div_nat_floor_pow_sq_le_div_sq N (Nat.cast_pos.2 hj) c_one using 2

Premises used: Iff.mpr, Nat.cast_pos, sum_div_nat_floor_pow_sq_le_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)
N j : ℕ
h : j ∈ range (u (N - 1))
hj : 0 < j
⊢ {i ∈ range N | j < u i} = {i ∈ range N | LT.lt (α := ℝ) (↑j : ℝ) (↑⌊c ^ i⌋₊ : ℝ)}

Tactic:
simp only [u, Nat.cast_lt]

Premises used: Nat.cast_lt
-- 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 j : ℕ
h : j ∈ range (u (N - 1))
hj : 0 < j
x : ℕ
h_1 : x ∈ {i ∈ range N | LT.lt (α := ℝ) (↑j : ℝ) (↑⌊c ^ i⌋₊ : ℝ)}
⊢ (HPow.hPow (α := ℝ) (β := ℕ) (↑(u x) : ℝ) 2)⁻¹ = 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ x⌋₊ : ℝ) 2

Tactic:
simp only [u, one_div]

Premises used: one_div
-- 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 : ℕ
simp_rw :
  Eq (α := ℝ)
    (∑ j ∈ range (u (N - 1)),
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ)
    (∑ i ∈ range (u (N - 1)),
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
        ((HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (Y i) ℙ))
simp_rw₁ :
  Eq (α := ℝ)
    (∑ x ∈ range (u (N - 1)),
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 * (HPow.hPow (α := ℝ) (β := ℕ) (↑x : ℝ) 2)⁻¹ *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y x) ℙ)
    (∑ i ∈ range (u (N - 1)),
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
        ((HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (Y i) ℙ))
⊢ ∑ j ∈ range (u (N - 1)),
      HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2 *
        variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ =
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
      ∑ j ∈ range (u (N - 1)),
        (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ

Tactic:
simp_rw [mul_sum, div_eq_mul_inv, mul_assoc]

Premises used: Finset.mul_sum, mul_assoc, div_eq_mul_inv
-- 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 : ℕ
apply : 0 ≤ HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3
⊢ HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
      ∑ j ∈ range (u (N - 1)),
        (HPow.hPow (α := ℝ) (β := ℕ) (↑j : ℝ) 2)⁻¹ * variance (mΩ := MeasureSpace.toMeasurableSpace) (Y j) ℙ ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 *
      HMul.hMul (α := ℝ) 2 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)

Tactic:
apply mul_le_mul_of_nonneg_left (I1 _)

Premises used: mul_le_mul_of_nonneg_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
ε : ℝ
ε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 : ℕ
apply : 0 ≤ HPow.hPow (β := ℕ) (c - 1)⁻¹ 3
⊢ 0 ≤ HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3

Tactic:
apply mul_nonneg (pow_nonneg c_pos.le _)

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

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

Premises used: Iff.mpr, pow_nonneg, LT.lt.le, inv_nonneg, sub_nonneg