awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k

Tactic:
⟨k + 1, fun N => lt_of_le_of_lt (hk N) k.lt_succ_self⟩

Premises used: lt_of_le_of_lt, Nat.lt_succ_self, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k

Tactic:
exact ⟨k + 1, fun N => lt_of_le_of_lt (hk N) k.lt_succ_self⟩
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k

Tactic:
replace hω : ∃ k, ∀ N, upcrossingsBefore a b f N ω < k := by
    obtain ⟨k, hk⟩ := hω
    exact ⟨k + 1, fun N => lt_of_le_of_lt (hk N) k.lt_succ_self⟩
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a
h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω
⊢ ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a

Tactic:
rw [frequently_atTop] at h₁ h₂

Premises used: Filter.frequently_atTop
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a
h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω
h₃ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
⊢ ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω

Tactic:
rw [frequently_atTop] at h₁ h₂

Premises used: Filter.frequently_atTop
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
⊢ False

Tactic:
Classical.not_not.2 hω ?_

Premises used: Iff.mpr, Classical.not_not
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
refine : ¬∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
⊢ False

Tactic:
refine Classical.not_not.2 hω ?_

Premises used: Iff.mpr, Classical.not_not
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
push : ∀ (k : ℕ), ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω
⊢ ¬∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
⊢ ∃ (N : ℕ), 0 ≤ upcrossingsBefore a b f N ω

Tactic:
simp only [zero_le, exists_const]

Premises used: zero_le, exists_const
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k : ℕ
ih : ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω
succ : ∀ (N : ℕ) (hN : k ≤ upcrossingsBefore a b f N ω), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω

Tactic:
obtain ⟨N, hN⟩ := ih
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
succ : ∀ (N₁ : ℕ) (hN₁ : N₁ ≥ N) (hN₁' : f N₁ ω < a), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω

Tactic:
obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
N₁ : ℕ
hN₁ : N₁ ≥ N
hN₁' : f N₁ ω < a
succ : ∀ (N₂ : ℕ) (hN₂ : N₂ ≥ N₁) (hN₂' : b < f N₂ ω), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω

Tactic:
obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
N₁ : ℕ
hN₁ : N₁ ≥ N
hN₁' : f N₁ ω < a
N₂ : ℕ
hN₂ : N₂ ≥ N₁
hN₂' : b < f N₂ ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω

Tactic:
⟨N₂ + 1, Nat.succ_le_of_lt <|
      lt_of_le_of_lt hN (upcrossingsBefore_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩

Premises used: lt_of_le_of_lt, Nat.succ_le_of_lt, MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k N : ℕ
hN : k ≤ upcrossingsBefore a b f N ω
N₁ : ℕ
hN₁ : N₁ ≥ N
hN₁' : f N₁ ω < a
N₂ : ℕ
hN₂ : N₂ ≥ N₁
hN₂' : b < f N₂ ω
⊢ ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω

Tactic:
exact ⟨N₂ + 1, Nat.succ_le_of_lt <|
      lt_of_le_of_lt hN (upcrossingsBefore_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
k : ℕ
zero : ∃ (N : ℕ), 0 ≤ upcrossingsBefore a b f N ω
succ : ∀ (k : ℕ) (ih : ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
⊢ ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω

Tactic:
induction k with
  | zero => simp only [zero_le, exists_const]
  | succ k ih =>
    obtain ⟨N, hN⟩ := ih
    obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N
    obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁
    exact ⟨N₂ + 1, Nat.succ_le_of_lt <|
      lt_of_le_of_lt hN (upcrossingsBefore_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩

Premises used: zero_le, exists_const
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
h₁ : ∃ᶠ (n : ℕ) in atTop, f n ω < a
h₂ : ∃ᶠ (n : ℕ) in atTop, b < f n ω
⊢ upcrossings a b f ω = ∞

Tactic:
by_contradiction fun h => not_frequently_of_upcrossings_lt_top hab h ⟨h₁, h₂⟩

Premises used: MeasureTheory.not_frequently_of_upcrossings_lt_top, And.intro, by_contradiction
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
pos :
  ∀ (h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|),
    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
neg :
  ∀ (h : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|),
    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
by_cases h : IsBoundedUnder (· ≤ ·) atTop fun n => |f n ω|

Premises used: abs, LE.le, Filter.atTop, Filter.IsBoundedUnder
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ f n ω) ∧
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ f n ω

Tactic:
rw [isBoundedUnder_le_abs] at h

Premises used: Filter.isBoundedUnder_le_abs
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h :
  (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ f n ω) ∧
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ f n ω
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
tendsto_of_no_upcrossings Rat.denseRange_cast ?_ h.1 h.2

Premises used: And.right, And.left, Rat.denseRange_cast, tendsto_of_no_upcrossings
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h :
  (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ f n ω) ∧
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ f n ω
pos :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Set.range Rat.cast) a →
      ∀ (b : ℝ),
        Membership.mem (γ := Set ℝ) (Set.range Rat.cast) b →
          a < b → ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
refine tendsto_of_no_upcrossings Rat.denseRange_cast ?_ h.1 h.2

Premises used: And.right, And.left, Rat.denseRange_cast, tendsto_of_no_upcrossings
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h :
  (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ f n ω) ∧
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ f n ω
a b : ℚ
hab : LT.lt (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < (↑a : ℝ)) ∧ ∃ᶠ (n : ℕ) in atTop, (↑b : ℝ) < f n ω)

Tactic:
not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne

Premises used: MeasureTheory.not_frequently_of_upcrossings_lt_top, Rat.cast_lt, Iff.mp, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h :
  (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ f n ω) ∧
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ f n ω
a b : ℚ
hab : LT.lt (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < (↑a : ℝ)) ∧ ∃ᶠ (n : ℕ) in atTop, (↑b : ℝ) < f n ω)

Tactic:
exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne

Premises used: MeasureTheory.not_frequently_of_upcrossings_lt_top, Rat.cast_lt, Iff.mp, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|
neg :
  ∀ (a b : ℚ) (hab : a < b) (h₁ : ∃ᶠ (i : ℕ) in atTop, f i ω < (↑a : ℝ)) (h₂ : ∃ᶠ (i : ℕ) in atTop, (↑b : ℝ) < f i ω),
    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
obtain ⟨a, b, hab, h₁, h₂⟩ := ENNReal.exists_upcrossings_of_not_bounded_under hf₁.ne h

Premises used: ENNReal.exists_upcrossings_of_not_bounded_under, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|
a b : ℚ
hab : a < b
h₁ : ∃ᶠ (i : ℕ) in atTop, f i ω < (↑a : ℝ)
h₂ : ∃ᶠ (i : ℕ) in atTop, (↑b : ℝ) < f i ω
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
False.elim ((hf₂ a b hab).ne (upcrossings_eq_top_of_frequently_lt (Rat.cast_lt.2 hab) h₁ h₂))

Premises used: Iff.mpr, False.elim, Rat.cast_lt, MeasureTheory.upcrossings_eq_top_of_frequently_lt, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ (↑‖f n ω‖₊ : ℝ≥0∞)) atTop) ∞
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|
a b : ℚ
hab : a < b
h₁ : ∃ᶠ (i : ℕ) in atTop, f i ω < (↑a : ℝ)
h₂ : ∃ᶠ (i : ℕ) in atTop, (↑b : ℝ) < f i ω
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
exact
      False.elim ((hf₂ a b hab).ne (upcrossings_eq_top_of_frequently_lt (Rat.cast_lt.2 hab) h₁ h₂))

Premises used: Iff.mpr, False.elim, Rat.cast_lt, MeasureTheory.upcrossings_eq_top_of_frequently_lt, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, upcrossings a b f ω < ∞

Tactic:
ae_lt_top (hf.stronglyAdapted.measurable_upcrossings hab) ?_

Premises used: MeasureTheory.StronglyAdapted.measurable_upcrossings, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.ae_lt_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
refine : ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
⊢ ∀ᵐ (ω : Ω) ∂μ, upcrossings a b f ω < ∞

Tactic:
refine ae_lt_top (hf.stronglyAdapted.measurable_upcrossings hab) ?_

Premises used: MeasureTheory.StronglyAdapted.measurable_upcrossings, MeasureTheory.Submartingale.stronglyAdapted, MeasureTheory.ae_lt_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
have := hf.mul_lintegral_upcrossings_le_lintegral_pos_part a b
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
this :
  ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
rw :
  ∀
    (this :
      ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤
        (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)),
    ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
h0 :
  ∀
    (this :
      (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤
        ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ),
    ENNReal.ofReal (b - a) ≠ 0 ∨ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) 0
ht :
  ∀
    (this :
      (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤
        ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ),
    ENNReal.ofReal (b - a) ≠ ∞ ∨ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞

Tactic:
rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this

Premises used: ENNReal.le_div_iff_mul_le, mul_comm
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞

Tactic:
(lt_of_le_of_lt this (ENNReal.div_lt_top ?_ ?_)).ne

Premises used: lt_of_le_of_lt, ENNReal.div_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
refine_1 : Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞
refine_2 : ENNReal.ofReal (b - a) ≠ 0
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞

Tactic:
refine (lt_of_le_of_lt this (ENNReal.div_lt_top ?_ ?_)).ne

Premises used: lt_of_le_of_lt, ENNReal.div_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm] at hbdd

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
⊢ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
(lintegral_mono ?_ : ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ ∫⁻ ω, ‖f n ω‖₊ + ‖a‖₊ ∂μ).trans ?_

Premises used: MeasureTheory.lintegral_mono, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
refine_1 :
  LE.le.{u_1} (α := Ω → ℝ≥0∞) (fun (ω : Ω) ↦ (↑‖f n ω - a‖₊ : ℝ≥0∞)) fun (ω : Ω) ↦ (↑‖f n ω‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞)
refine_2 :
  ∫⁻ (a_1 : Ω), (↑‖f n a_1‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
refine (lintegral_mono ?_ : ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ ∫⁻ ω, ‖f n ω‖₊ + ‖a‖₊ ∂μ).trans ?_

Premises used: MeasureTheory.lintegral_mono, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
ω : Ω
refine_1 : ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊
⊢ LE.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (ω : Ω) ↦ (↑‖f n ω - a‖₊ : ℝ≥0∞)) ω)
    ((fun (ω : Ω) ↦ (↑‖f n ω‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞)) ω)

Tactic:
simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ENNReal.coe_add, ENNReal.coe_le_coe]

Premises used: sub_eq_add_neg, ENNReal.coe_le_coe, nnnorm_neg, ENNReal.coe_add
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
ω : Ω
⊢ ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊

Tactic:
nnnorm_add_le _ _

Premises used: nnnorm_add_le
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
ω : Ω
⊢ ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊

Tactic:
exact nnnorm_add_le _ _

Premises used: nnnorm_add_le
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
refine_2 :
  ∫⁻ (a : Ω), (↑‖f n a‖₊ : ℝ≥0∞) ∂μ + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (a_1 : Ω), (↑‖f n a_1‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp_rw [lintegral_add_right _ measurable_const, lintegral_const]

Premises used: MeasureTheory.lintegral_const, measurable_const, MeasureTheory.lintegral_add_right
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
⊢ ∫⁻ (a : Ω), (↑‖f n a‖₊ : ℝ≥0∞) ∂μ + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
add_le_add (hbdd _) le_rfl

Premises used: le_rfl, add_le_add
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this :
  ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
n : ℕ
⊢ ∫⁻ (a : Ω), (↑‖f n a‖₊ : ℝ≥0∞) ∂μ + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
exact add_le_add (hbdd _) le_rfl

Premises used: le_rfl, add_le_add