awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
ι : Type u_1
Ω : Type u_2
β : Type u_3
m0 : MeasurableSpace Ω
inst : ConditionallyCompleteLinearOrderBot ι
ℱ : Filtration ι m0
inst_1 : WellFoundedLT ι
inst_2 : Countable ι
inst_3 : TopologicalSpace β
inst_4 : Preorder β
inst_5 : ClosedIciTopology β
inst_6 : TopologicalSpace.PseudoMetrizableSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
f : ι → Ω → β
r : β
hf : StronglyAdapted (β := fun (i : ι) ↦ β) ℱ f
⊢ IsStoppingTime ℱ (leastGE f r)

Tactic:
hf.adapted.isStoppingTime_hittingAfter measurableSet_Ici

Premises used: MeasureTheory.StronglyAdapted.adapted, MeasureTheory.leastGE, measurableSet_Ici, MeasureTheory.Adapted.isStoppingTime_hittingAfter
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
⊢ Submartingale (stoppedAbove f r) ℱ μ

Tactic:
hf.stoppedProcess (hf.stronglyAdapted.isStoppingTime_leastGE r)

Premises used: MeasureTheory.stoppedAbove, MeasureTheory.Submartingale.stoppedProcess, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.StronglyAdapted.isStoppingTime_leastGE
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
h : ∀ (ω : Ω) (hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)), stoppedAbove f r i ω ≤ r + (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, stoppedAbove f r i ω ≤ r + (↑R : ℝ)

Tactic:
filter_upwards [hbdd] with ω hbddω
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h : f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
⊢ stoppedAbove f r i ω ≤ r + (↑R : ℝ)

Tactic:
rw [stoppedAbove, stoppedProcess, ENat.some_eq_coe]

Premises used: ENat.some_eq_coe, MeasureTheory.stoppedAbove, MeasureTheory.stoppedProcess
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
pos :
  ∀ (h_zero : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0),
    f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
neg :
  ∀ (h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0),
    f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)

Tactic:
by_cases h_zero : (min (i : ℕ∞) (leastGE f r ω)).untopA = 0

Premises used: Nat.cast, MeasureTheory.leastGE, WithTop.untopA, Min.min
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
pos : 0 ≤ r + (↑R : ℝ)
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)

Tactic:
simp only [h_zero, hf0, Pi.zero_apply]

Premises used: Pi.zero_apply
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
⊢ 0 ≤ r + (↑R : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
neg :
  ∀ (k : ℕ) (hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1),
    f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_one_of_ne_zero h_zero

Premises used: Nat.exists_eq_add_one_of_ne_zero
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
neg : f (k + 1) ω - r ≤ (↑R : ℝ)
⊢ f (min (↑i : WithTop ℕ) (leastGE f r ω)).untopA ω ≤ r + (↑R : ℝ)

Tactic:
rw [hk, add_comm r, ← sub_le_iff_le_add]

Premises used: sub_le_iff_le_add, add_comm
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
neg : ∀ (this : ∀ (hk₂ : LE.le (α := ℕ) ⊥ (↑k : ℕ)), f (↑k : ℕ) ω ∉ Set.Ici r), f (k + 1) ω - r ≤ (↑R : ℝ)
neg₁ : (↑k : WithTop ℕ) < leastGE f r ω
⊢ f (k + 1) ω - r ≤ (↑R : ℝ)

Tactic:
have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
this : ∀ (hk₂ : LE.le (α := ℕ) ⊥ (↑k : ℕ)), f (↑k : ℕ) ω ∉ Set.Ici r
⊢ f (↑k : ℕ) ω < r

Tactic:
simp only [bot_eq_zero, zero_le, Set.mem_Ici, not_le, forall_const] at this

Premises used: not_le, zero_le, Set.mem_Ici, forall_const, bot_eq_zero
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
this : f (↑k : ℕ) ω < r
⊢ f (k + 1) ω - r ≤ (↑R : ℝ)

Tactic:
(sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))

Premises used: le_abs_self, LT.lt.le, LE.le.trans, sub_lt_sub_left
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
this : f (↑k : ℕ) ω < r
⊢ f (k + 1) ω - r ≤ (↑R : ℝ)

Tactic:
exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))

Premises used: le_abs_self, LT.lt.le, LE.le.trans, sub_lt_sub_left
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
neg : (↑k : ℕ∞) < min (↑i : ℕ∞) (leastGE f r ω)
⊢ (↑k : WithTop ℕ) < leastGE f r ω

Tactic:
suffices (k : ℕ∞) < min (i : ℕ∞) (leastGE f r ω) from this.trans_le (min_le_right _ _)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
⊢ Ne (α := ℕ∞) (↑i : ℕ∞) ⊤

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
⊢ min (↑i : ℕ∞) (leastGE f r ω) ≠ ⊤

Tactic:
have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
      ne_top_of_le_ne_top (by simp) (min_le_left _ _)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
h_top : min (↑i : ℕ∞) (leastGE f r ω) ≠ ⊤
⊢ min (↑i : ℕ∞) (leastGE f r ω) ≠ ⊤

Tactic:
h_top
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
h_zero : ¬WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i : ℕ∞) (leastGE f r ω)) = k + 1
h_top : min (↑i : ℕ∞) (leastGE f r ω) ≠ ⊤
neg :
  ∀ (p : ℕ) (h_zero : ¬Eq (α := ℕ) (WithTop.untopA (↑p : ℕ∞)) 0) (hk : WithTop.untopA (↑p : ℕ∞) = k + 1),
    LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑p : ℕ∞)
⊢ (↑k : ℕ∞) < min (↑i : ℕ∞) (leastGE f r ω)

Tactic:
lift min (i : ℕ∞) (leastGE f r ω) to ℕ using h_top with p

Premises used: Nat.cast, MeasureTheory.leastGE, Min.min
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
k p : ℕ
h_zero : ¬Eq (α := ℕ) (WithTop.untopA (↑p : ℕ∞)) 0
hk : WithTop.untopA (↑p : ℕ∞) = k + 1
neg : k < p
⊢ LT.lt (α := ℕ∞) (↑k : ℕ∞) (↑p : ℕ∞)

Tactic:
simp only [untopD_coe_enat, Nat.cast_lt, gt_iff_lt] at *

Premises used: untopD_coe_enat, gt_iff_lt, Nat.cast_lt
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
k p : ℕ
h_zero : ¬p = 0
hk : p = k + 1
⊢ k < p

Tactic:
lia
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
      ENNReal.ofReal (r + (↑R : ℝ))

Tactic:
eLpNorm_one_le_of_le' ((hf.stoppedAbove r).integrable _) ?_
    (stoppedAbove_le hr hf0 hbdd i)

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.eLpNorm_one_le_of_le', MeasureTheory.Submartingale.stoppedAbove, MeasureTheory.stoppedAbove_le
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
refine : LE.le (α := ℝ) 0 (∫ (x : Ω), stoppedAbove f r i x ∂μ)
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
      ENNReal.ofReal (r + (↑R : ℝ))

Tactic:
refine eLpNorm_one_le_of_le' ((hf.stoppedAbove r).integrable _) ?_
    (stoppedAbove_le hr hf0 hbdd i)

Premises used: MeasureTheory.Submartingale.integrable, MeasureTheory.eLpNorm_one_le_of_le', MeasureTheory.Submartingale.stoppedAbove, MeasureTheory.stoppedAbove_le
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
rw : LE.le (α := ℝ) 0 (∫ (x : Ω) in Set.univ, stoppedAbove f r i x ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), stoppedAbove f r i x ∂μ)

Tactic:
rw [← setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in Set.univ, stoppedAbove f r i x ∂μ)

Tactic:
le_trans ?_ ((hf.stoppedAbove r).setIntegral_le zero_le MeasurableSet.univ)

Premises used: zero_le, MeasureTheory.Submartingale.setIntegral_le, MeasureTheory.Submartingale.stoppedAbove, MeasurableSet.univ, le_trans
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
refine : LE.le (α := ℝ) 0 (∫ (ω : Ω) in Set.univ, stoppedAbove f r 0 ω ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω) in Set.univ, stoppedAbove f r i x ∂μ)

Tactic:
refine le_trans ?_ ((hf.stoppedAbove r).setIntegral_le zero_le MeasurableSet.univ)

Premises used: zero_le, MeasureTheory.Submartingale.setIntegral_le, MeasureTheory.Submartingale.stoppedAbove, MeasurableSet.univ, le_trans
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ LE.le (α := ℝ) 0 (∫ (ω : Ω) in Set.univ, stoppedAbove f r 0 ω ∂μ)

Tactic:
simp [stoppedAbove, stoppedProcess, hf0]

Premises used: MeasureTheory.stoppedAbove, MeasureTheory.stoppedProcess
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤
    (↑(HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
            ENNReal.ofReal (r + (↑R : ℝ))).toNNReal :
      ℝ≥0∞)

Tactic:
(hf.eLpNorm_stoppedAbove_le hr hf0 hbdd i).trans ?_

Premises used: MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le, LE.le.trans
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
refine :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
      ENNReal.ofReal (r + (↑R : ℝ)) ≤
    (↑(HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
            ENNReal.ofReal (r + (↑R : ℝ))).toNNReal :
      ℝ≥0∞)
⊢ eLpNorm (stoppedAbove f r i) 1 μ ≤
    (↑(HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
            ENNReal.ofReal (r + (↑R : ℝ))).toNNReal :
      ℝ≥0∞)

Tactic:
refine (hf.eLpNorm_stoppedAbove_le hr hf0 hbdd i).trans ?_

Premises used: MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le, LE.le.trans
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
i : ℕ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
      ENNReal.ofReal (r + (↑R : ℝ)) ≤
    (↑(HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) *
            ENNReal.ofReal (r + (↑R : ℝ))).toNNReal :
      ℝ≥0∞)

Tactic:
simp [ENNReal.coe_toNNReal (measure_ne_top μ _), ENNReal.coe_toNNReal]

Premises used: ENNReal.coe_toNNReal, MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
rw : ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n a) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n a) atTop (𝓝 c)

Tactic:
fun i ↦ Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedAbove i)
      (hf.eLpNorm_stoppedAbove_le' i.cast_nonneg hf0 hbdd)

Premises used: Nat.cast_nonneg, MeasureTheory.Submartingale.eLpNorm_stoppedAbove_le', Nat.cast, MeasureTheory.Submartingale.stoppedAbove, MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ (i : ℕ), ∀ᵐ (a : Ω) ∂μ, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n a) atTop (𝓝 c)

Tactic:
exact fun i ↦ Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedAbove i)
      (hf.eLpNorm_stoppedAbove_le' i.cast_nonneg hf0 hbdd)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)

Tactic:
have ht : ∀ᵐ ω ∂μ, ∀ i : ℕ, ∃ c, Tendsto (fun n => stoppedAbove f i n ω) atTop (𝓝 c) := by
    rw [ae_all_iff]
    exact fun i ↦ Submartingale.exists_ae_tendsto_of_bdd (hf.stoppedAbove i)
      (hf.eLpNorm_stoppedAbove_le' i.cast_nonneg hf0 hbdd)
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
h :
  ∀ (ω : Ω) (hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c))
    (hωb : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω) → ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
filter_upwards [ht] with ω hω hωb
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ f n ω)
⊢ Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))

Tactic:
rw [BddAbove] at hωb

Premises used: BddAbove
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
h :
  ∀ (i : ℕ) (hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)),
    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
obtain ⟨i, hi⟩ := exists_nat_gt hωb.some

Premises used: exists_nat_gt, Set.Nonempty.some
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
n : ℕ
⊢ f n ω < (↑i : ℝ)

Tactic:
lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi

Premises used: lt_of_le_of_lt, Set.Nonempty.some_mem, Exists.intro, Iff.mp, rfl, mem_upperBounds
-- Module: Mathlib.Probability.Martingale.BorelCantelli
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ (↑R : ℝ)
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ stoppedAbove f (↑i : ℝ) n ω) atTop (𝓝 c)
hωb : Set.Nonempty (α := ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ f n ω))
i : ℕ
hi : hωb.some (s := upperBounds (Set.range fun (n : ℕ) ↦ f n ω)) < (↑i : ℝ)
n : ℕ
⊢ f n ω < (↑i : ℝ)

Tactic:
exact lt_of_le_of_lt ((mem_upperBounds.1 hωb.some_mem) _ ⟨n, rfl⟩) hi

Premises used: lt_of_le_of_lt, Set.Nonempty.some_mem, Exists.intro, Iff.mp, rfl, mem_upperBounds