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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
h :
  ∀ (n : ℕ) (hn : X n ω ∉ Set.Ioi (↑n : ℝ)) (npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n),
    0 = truncation (X n) (↑n : ℝ) ω - X n ω
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω

Tactic:
filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos

Premises used: Filter.Ioi_mem_atTop, 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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : 0 = (if -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ) then X n ω else 0) - X n ω
⊢ 0 = truncation (X n) (↑n : ℝ) ω - X n ω

Tactic:
simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]

Premises used: Set.indicator, id, Set.mem_Ioc, Function.comp_apply, ProbabilityTheory.truncation
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
pos : ∀ (h : -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ)), 0 = X n ω - X n ω
neg : ∀ (h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))), 0 = 0 - X n ω
⊢ 0 = (if -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ) then X n ω else 0) - X n ω

Tactic:
split_ifs with 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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ)
⊢ 0 = X n ω - X n ω

Tactic:
(sub_self _).symm

Premises used: sub_self, Eq.symm
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : -(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ)
⊢ 0 = X n ω - X n ω

Tactic:
exact (sub_self _).symm

Premises used: sub_self, Eq.symm
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
apply : LT.lt (α := ℝ) (-(↑n : ℝ)) 0
⊢ -(↑n : ℝ) < X n ω

Tactic:
apply lt_of_lt_of_le _ (hnonneg n ω)

Premises used: lt_of_lt_of_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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
⊢ LT.lt (α := ℝ) (-(↑n : ℝ)) 0

Tactic:
simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos

Premises used: Nat.cast_pos, Right.neg_neg_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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
⊢ -(↑n : ℝ) < X n ω

Tactic:
have : -(n : ℝ) < X n ω := by
        apply lt_of_lt_of_le _ (hnonneg n ω)
        simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : ¬(-(↑n : ℝ) < X n ω ∧ X n ω ≤ (↑n : ℝ))
this : -(↑n : ℝ) < X n ω
⊢ (↑n : ℝ) < X n ω

Tactic:
simp only [this, true_and, not_le] at h

Premises used: not_le, true_and
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
this : -(↑n : ℝ) < X n ω
h : (↑n : ℝ) < X n ω
⊢ 0 = 0 - X n ω

Tactic:
(hn h).elim

Premises used: False.elim
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi (↑n : ℝ)
n : ℕ
hn : X n ω ∉ Set.Ioi (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
this : -(↑n : ℝ) < X n ω
h : (↑n : ℝ) < X n ω
⊢ 0 = 0 - X n ω

Tactic:
exact (hn h).elim

Premises used: False.elim
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
⊢ ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)

Tactic:
have B : ∀ᵐ ω, Tendsto (fun n : ℕ => truncation (X n) n ω - X n ω) atTop (𝓝 0) := by
    filter_upwards [ae_eventually_notMem A.ne] with ω hω
    apply tendsto_const_nhds.congr' _
    filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos
    simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]
    split_ifs with h
    · exact (sub_self _).symm
    · have : -(n : ℝ) < X n ω := by
        apply lt_of_lt_of_le _ (hnonneg n ω)
        simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos
      simp only [this, true_and, not_le] at h
      exact (hn h).elim
-- 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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
h :
  ∀ (ω : Ω) (hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
      fun (n : ℕ) ↦ (↑n : ℝ)
⊢ ∀ᵐ (ω : Ω),
    IsLittleO (E := ℝ) (F := ℝ) atTop
      (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
      fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
filter_upwards [B] with ω 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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)

Tactic:
isLittleO_sum_range_of_tendsto_zero hω

Premises used: Asymptotics.isLittleO_sum_range_of_tendsto_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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
h :
  Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
    fun (n : ℕ) ↦ ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)

Tactic:
convert! isLittleO_sum_range_of_tendsto_zero hω using 1

Premises used: Asymptotics.isLittleO_sum_range_of_tendsto_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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
h :
  ∀ (n : ℕ),
    HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω) =
      ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
    fun (n : ℕ) ↦ ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)

Tactic:
ext 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) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A :
  LT.lt (α := ℝ≥0∞)
    (∑' (j : ℕ),
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioi (↑j : ℝ)) (X j ω)})
    ∞
B : ∀ᵐ (ω : Ω), Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (β := ℝ) (fun (n : ℕ) ↦ truncation (X n) (↑n : ℝ) ω - X n ω) atTop (𝓝 0)
n : ℕ
h h₁ :
  HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω) =
    HSub.hSub (α := ℝ) (∑ x ∈ range n, truncation (X x) (↑x : ℝ) ω) (∑ x ∈ range n, X x ω)
⊢ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω) =
    ∑ i ∈ range n, (truncation (X i) (↑i : ℝ) ω - X i ω)

Tactic:
rw [sum_sub_distrib]

Premises used: Finset.sum_sub_distrib
-- 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
n : ℕ
⊢ LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)

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
n : ℕ
refine : LE.le (α := ℝ) 1 (↑⌊c ^ n⌋₊ : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
refine 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
n : ℕ
⊢ LE.le (α := ℝ) 1 (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ c_one.le]

Premises used: Nat.one_le_cast, Nat.one_le_floor_iff, 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
⊢ ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)

Tactic:
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c ^ n⌋₊ := by
    intro n
    refine zero_lt_one.trans_le ?_
    simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ 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
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
h :
  ∀ (ω : Ω)
    (hω :
      IsLittleO (E := ℝ) (F := ℝ) atTop
        (fun (n : ℕ) ↦
          ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
            HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
        fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ))
    (h'ω :
      IsLittleO (E := ℝ) (F := ℝ) atTop
        (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω))
        fun (n : ℕ) ↦ (↑n : ℝ)),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
⊢ ∀ᵐ (ω : Ω),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
      (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
filter_upwards [strong_law_aux4 X hint hindep hident hnonneg c_one,
    strong_law_aux5 X hint hident hnonneg] with ω hω h'ω

Premises used: ProbabilityTheory.strong_law_aux4, ProbabilityTheory.strong_law_aux5
-- Module: Mathlib.Probability.StrongLaw
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : ℕ → Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (X 0) ℙ
hindep : Pairwise ((fun (f g : Ω → ℝ) ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c ^ n⌋₊ : ℝ)
ω : Ω
hω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i : ℝ) ω -
        HMul.hMul (α := ℝ) (↑⌊c ^ n⌋₊ : ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))
    fun (n : ℕ) ↦ (↑⌊c ^ n⌋₊ : ℝ)
h'ω :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) (∑ i ∈ range n, truncation (X i) (↑i : ℝ) ω) (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    (↑n : ℝ)
h :
  IsLittleO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℕ) ↦
      HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) (↑⌊c ^ x⌋₊ : ℝ) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a)
    fun (_x : ℕ) ↦ 1
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) (↑⌊c ^ n⌋₊ : ℝ)) atTop
    (𝓝 (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X 0 a))

Tactic:
rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ]

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

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

Tactic:
hω.sub (h'ω.comp_tendsto A)

Premises used: Asymptotics.IsLittleO.comp_tendsto, Asymptotics.IsLittleO.sub