awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
have succ : ∀ (N₂ : ℕ) (hN₂ : N₂ ≥ N₁) (hN₂' : b < f N₂ ω), ∃ (N : ℕ), k + 1 ≤ upcrossingsBefore a b f N ω
Tactic: obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 : ℕ), k ≤ upcrossingsBefore a b f N ω
have zero : ∃ (N : ℕ), 0 ≤ 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₂')⟩
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ω
⊢ ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω
have succ : ∀ (k : ℕ) (ih : ∃ (N : ℕ), k ≤ upcrossingsBefore a b f N ω), ∃ (N : ℕ), k + 1 ≤ 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₂')⟩
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ω < ∞
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have pos : ∀ (h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|),
  ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: by_cases h : IsBoundedUnder (· ≤ ·) atTop fun n => |f n ω|
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have neg : ∀ (h : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ |f n ω|),
  ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
Tactic: by_cases h : IsBoundedUnder (· ≤ ·) atTop fun n => |f n ω|
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
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 ω|
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have h₁ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
have 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 ω)
Tactic: refine tendsto_of_no_upcrossings Rat.denseRange_cast ?_ h.1 h.2
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ω|
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
have 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)
Tactic: obtain ⟨a, b, hab, h₁, h₂⟩ := ENNReal.exists_upcrossings_of_not_bounded_under hf₁.ne h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ω < ∞
have refine : ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
Tactic: refine ae_lt_top (hf.stronglyAdapted.measurable_upcrossings hab) ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
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
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)⁺ ∂μ
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
have rw : ∀
  (this :
    ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤
      (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)),
  ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
Tactic: rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ∂μ ≠ ∞
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
have 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
Tactic: rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
have 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)⁺ ∂μ) ∞
Tactic: rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ∂μ ≠ ∞
have refine_1 : Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞
Tactic: refine (lt_of_le_of_lt this (ENNReal.div_lt_top ?_ ?_)).ne
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)⁺ ∂μ) ∞
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞
have refine_2 : ENNReal.ofReal (b - a) ≠ 0
Tactic: refine (lt_of_le_of_lt this (ENNReal.div_lt_top ?_ ?_)).ne
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
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 : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have hbdd₁ : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ (↑R : ℝ≥0∞)
Tactic: simp_rw [eLpNorm_one_eq_lintegral_enorm] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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∞)
have refine_1 : LE.le.{u_1} (α := Ω → ℝ≥0∞) (fun (ω : Ω) ↦ (↑‖f n ω - a‖₊ : ℝ≥0∞)) fun (ω : Ω) ↦ (↑‖f n ω‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞)
Tactic: refine (lintegral_mono ?_ : ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ ∫⁻ ω, ‖f n ω‖₊ + ‖a‖₊ ∂μ).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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∞)
⊢ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have refine_2 : ∫⁻ (a_1 : Ω), (↑‖f n a_1‖₊ : ℝ≥0∞) + (↑‖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 ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 : ℕ
ω : Ω
⊢ LE.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (ω : Ω) ↦ (↑‖f n ω - a‖₊ : ℝ≥0∞)) ω)
    ((fun (ω : Ω) ↦ (↑‖f n ω‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞)) ω)
have refine_1 : ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊
Tactic: simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ENNReal.coe_add, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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_1 : Ω), (↑‖f n a_1‖₊ : ℝ≥0∞) + (↑‖a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [lintegral_add_right _ measurable_const, lintegral_const]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (hypothesis)
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)
⊢ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞
have hR' : ∀ (n : ℕ),
  ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
    (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: have hR' : ∀ n, ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ R + ‖a‖₊ * μ Set.univ := by
        simp_rw [eLpNorm_one_eq_lintegral_enorm] at hbdd
        intro n
        refine (lintegral_mono ?_ : ∫⁻ ω, ‖f n ω - a‖₊ ∂μ ≤ ∫⁻ ω, ‖f n ω‖₊ + ‖a‖₊ ∂μ).trans ?_
        · intro ω
          simp_rw [sub_eq_add_neg, ← nnnorm_neg a, ← ENNReal.coe_add, ENNReal.coe_le_coe]
          exact nnnorm_add_le _ _
        · simp_rw [lintegral_add_right _ measurable_const, lintegral_const]
          exact add_le_add (hbdd _) le_rfl
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞
have refine_1 : ∀ (n : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ∂μ ≤ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ
Tactic: refine ne_of_lt (iSup_lt_iff.2 ⟨R + ‖a‖₊ * μ Set.univ, ENNReal.add_lt_top.2
        ⟨ENNReal.coe_lt_top, by finiteness⟩,
        fun n => le_trans ?_ (hR' n)⟩)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
⊢ ∫⁻ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ∂μ ≤ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ
have refine_1 : ∀ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ≤ (↑‖f n ω - a‖₊ : ℝ≥0∞)
Tactic: refine lintegral_mono fun ω => ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
⊢ ENNReal.ofReal (f n ω - a)⁺ ≤ (↑‖f n ω - a‖₊ : ℝ≥0∞)
have refine_1 : (f n ω - a)⁺ ≤ ‖f n ω - a‖
Tactic: rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
refine_1 : (f n ω - a)⁺ ≤ ‖f n ω - a‖
⊢ ENNReal.ofReal (f n ω - a)⁺ ≤ (↑‖f n ω - a‖₊ : ℝ≥0∞)
have refine_1₁ : (↑‖f n ω - a‖₊ : ℝ≥0∞) ≠ ∞
Tactic: rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
have pos : ∀ (hnonneg : 0 ≤ f n ω - a), (f n ω - a)⁺ ≤ ‖f n ω - a‖
Tactic: by_cases! hnonneg : 0 ≤ f n ω - a
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
pos : ∀ (hnonneg : 0 ≤ f n ω - a), (f n ω - a)⁺ ≤ ‖f n ω - a‖
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
have neg : ∀ (hnonneg : f n ω - a < 0), (f n ω - a)⁺ ≤ ‖f n ω - a‖
Tactic: by_cases! hnonneg : 0 ≤ f n ω - a
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
hnonneg : 0 ≤ f n ω - a
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
have pos : f n ω - a ≤ ‖f n ω - a‖
Tactic: rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
hnonneg : 0 ≤ f n ω - a
pos : f n ω - a ≤ ‖f n ω - a‖
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
have pos₁ : f n ω - a ≤ |f n ω - a|
Tactic: rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
hnonneg : 0 ≤ f n ω - a
pos : f n ω - a ≤ ‖f n ω - a‖
pos₁ : f n ω - a ≤ |f n ω - a|
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
have pos₂ : f n ω - a ≤ f n ω - a
Tactic: rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
hnonneg : f n ω - a < 0
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖
have neg : 0 ≤ ‖f n ω - a‖
Tactic: rw [posPart_eq_zero.2 hnonneg.le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Convergence (goal)
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 ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ 0 ∨ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) 0
have h0 : ENNReal.ofReal (b - a) ≠ 0
Tactic: left