-- Mathlib/Probability/Martingale/Convergence.lean
theorem tendsto_of_uncrossing_lt_top (hf₁ : liminf (fun n => (‖f n ω‖₊ : ℝ≥0∞)) atTop < ∞)
    (hf₂ : ∀ a b : ℚ, a < b → upcrossings a b f ω < ∞) :
    ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Proof state:
case neg.intro.intro.intro.intro
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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₂))

Result:
no goals

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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 ∈ Set.range Rat.cast,
    ∀ b ∈ Set.range Rat.cast, a < b → ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)

Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ hab

Result:
case pos.intro.intro
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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 : ↑a < ↑b
⊢ ¬((∃ᶠ (n : ℕ) in atTop, f n ω < ↑a) ∧ ∃ᶠ (n : ℕ) in atTop, ↑b < f n ω)

Proof state:
case neg
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h : ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => |f n ω|
⊢ ∃ 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

Result:
case neg.intro.intro.intro.intro
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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)

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) atTop < ⊤
hf₂ : ∀ (a b : ℚ), a < b → upcrossings (↑a) (↑b) f ω < ⊤
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => |f n ω|
⊢ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
rw [isBoundedUnder_le_abs] at h

Result:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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)

Proof state:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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:
refine tendsto_of_no_upcrossings Rat.denseRange_cast ?_ h.1 h.2

Result:
case pos
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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 ∈ Set.range Rat.cast,
    ∀ b ∈ Set.range Rat.cast, a < b → ¬((∃ᶠ (n : ℕ) in atTop, f n ω < a) ∧ ∃ᶠ (n : ℕ) in atTop, b < f n ω)

Proof state:
case pos.intro.intro
Ω : Type u_1
f : ℕ → Ω → ℝ
ω : Ω
hf₁ : liminf (fun n => ↑‖f n ω‖₊) 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 : ↑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

Result:
no goals