awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ),
    ∫⁻ (ω : Ω), (↑‖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
-- 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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) < ∞

Tactic:
finiteness
-- 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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
refine_1 : ∀ (n : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ∂μ ≤ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ
⊢ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞

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)⟩)

Premises used: Iff.mpr, ENNReal.ofNNReal, HMul.hMul, NNNorm.nnnorm, Set.univ, HAdd.hAdd, And.intro, Exists.intro, ENNReal.add_lt_top, ne_of_lt, DFunLike.coe, ENNReal.coe_lt_top, iSup_lt_iff, 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 ℱ μ
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∞) ∂μ

Tactic:
lintegral_mono fun ω => ?_

Premises used: MeasureTheory.lintegral_mono
-- 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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
refine_1 : ∀ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ≤ (↑‖f n ω - a‖₊ : ℝ≥0∞)
⊢ ∫⁻ (ω : Ω), ENNReal.ofReal (f n ω - a)⁺ ∂μ ≤ ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ

Tactic:
refine lintegral_mono fun ω => ?_

Premises used: MeasureTheory.lintegral_mono
-- 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)
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‖
refine_1₁ : (↑‖f n ω - a‖₊ : ℝ≥0∞) ≠ ∞
⊢ ENNReal.ofReal (f n ω - a)⁺ ≤ (↑‖f n ω - a‖₊ : ℝ≥0∞)

Tactic:
rw [ENNReal.ofReal_le_iff_le_toReal, ENNReal.coe_toReal, coe_nnnorm]

Premises used: ENNReal.coe_toReal, ENNReal.ofReal_le_iff_le_toReal, coe_nnnorm
-- 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)
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‖
neg : ∀ (hnonneg : f n ω - a < 0), (f n ω - a)⁺ ≤ ‖f n ω - a‖
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖

Tactic:
by_cases! hnonneg : 0 ≤ f n ω - a
-- 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)
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|
pos₂ pos₃ : f n ω - a ≤ f n ω - a
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖

Tactic:
rw [posPart_eq_self.2 hnonneg, Real.norm_eq_abs, abs_of_nonneg hnonneg]

Premises used: Iff.mpr, posPart_eq_self, abs_of_nonneg, Real.norm_eq_abs
-- 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)
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
neg : 0 ≤ ‖f n ω - a‖
⊢ (f n ω - a)⁺ ≤ ‖f n ω - a‖

Tactic:
rw [posPart_eq_zero.2 hnonneg.le]

Premises used: Iff.mpr, LT.lt.le, posPart_eq_zero
-- 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)
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
⊢ 0 ≤ ‖f n ω - a‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- 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)
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
⊢ 0 ≤ ‖f n ω - a‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- 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)
hR' :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑‖f n ω - a‖₊ : ℝ≥0∞) ∂μ ≤
      (↑R : ℝ≥0∞) + HMul.hMul (β := ℝ≥0∞) (↑‖a‖₊ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
n : ℕ
ω : Ω
⊢ (↑‖f n ω - a‖₊ : ℝ≥0∞) ≠ ∞

Tactic:
finiteness
-- 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)
⊢ ENNReal.ofReal (b - a) ≠ 0

Tactic:
simp only [hab, Ne, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]

Premises used: not_le, ENNReal.ofReal_eq_zero, Ne, sub_nonpos
-- 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 ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
h0 : ENNReal.ofReal (b - a) ≠ 0
⊢ ENNReal.ofReal (b - a) ≠ 0 ∨ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) 0

Tactic:
left
-- 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 ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ 0

Tactic:
simp only [hab, Ne, ENNReal.ofReal_eq_zero, sub_nonpos, not_le]

Premises used: not_le, ENNReal.ofReal_eq_zero, Ne, sub_nonpos
-- 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 ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
ht : ENNReal.ofReal (b - a) ≠ ∞
⊢ ENNReal.ofReal (b - a) ≠ ∞ ∨ Ne (α := ℝ≥0∞) (⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) ∞

Tactic:
left
-- 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 ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
simp : ∀ (i i_1 : ℚ), i < i_1 → ∀ᵐ (x : Ω) ∂μ, upcrossings (↑i : ℝ) (↑i_1 : ℝ) f x < ∞
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞

Tactic:
simp only [ae_all_iff, eventually_imp_distrib_left]

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

Tactic:
hf.upcrossings_ae_lt_top' hbdd (Rat.cast_lt.2 hab)

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

Tactic:
exact hf.upcrossings_ae_lt_top' hbdd (Rat.cast_lt.2 hab)

Premises used: Iff.mpr, Rat.cast_lt, MeasureTheory.Submartingale.upcrossings_ae_lt_top'
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
h :
  ∀ (ω : Ω) (h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞)
    (h₂ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n ω‖ₑ) atTop) ∞),
    ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
⊢ ∀ᵐ (ω : Ω) ∂μ, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
filter_upwards [hf.upcrossings_ae_lt_top hbdd, ae_bdd_liminf_atTop_of_eLpNorm_bdd one_ne_zero
    (fun n => (hf.stronglyMeasurable n).measurable.mono (ℱ.le n) le_rfl) hbdd] with ω h₁ h₂

Premises used: MeasureTheory.Submartingale.upcrossings_ae_lt_top, le_rfl, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Submartingale.stronglyMeasurable, MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd, MeasureTheory.Filtration.le, one_ne_zero, Measurable.mono
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h₂ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n ω‖ₑ) atTop) ∞
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
tendsto_of_uncrossing_lt_top h₂ h₁

Premises used: MeasureTheory.tendsto_of_uncrossing_lt_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ω : Ω
h₁ : ∀ (a b : ℚ), a < b → upcrossings (↑a : ℝ) (↑b : ℝ) f ω < ∞
h₂ : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n ω‖ₑ) atTop) ∞
⊢ ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
exact tendsto_of_uncrossing_lt_top h₂ h₁

Premises used: MeasureTheory.tendsto_of_uncrossing_lt_top
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
hs : MeasurableSet.{u_1} (α := Ω) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)}
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)

Tactic:
rw [ae_iff, trim_measurableSet_eq]

Premises used: MeasureTheory.ae_iff, MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
hf.exists_ae_tendsto_of_bdd hbdd

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
exact hf.exists_ae_tendsto_of_bdd hbdd

Premises used: MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
⊢ MeasurableSet.{u_1} (α := Ω) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)}

Tactic:
MeasurableSet.compl <| measurableSet_exists_tendsto
      fun n => (hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩) le_rfl

Premises used: MeasureTheory.measurableSet_exists_tendsto, le_rfl, Set.Mem, MeasureTheory.StronglyMeasurable.measurable, setOf, MeasureTheory.Submartingale.stronglyMeasurable, MeasurableSet.compl, Exists.intro, le_sSup, Measurable.mono, rfl
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : MeasurableSpace Ω := ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n
⊢ MeasurableSet.{u_1} (α := Ω) {a : Ω | ¬∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 c)}

Tactic:
exact MeasurableSet.compl <| measurableSet_exists_tendsto
      fun n => (hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩) le_rfl

Premises used: MeasurableSet.compl
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
rw :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ f n ω) atTop
      (𝓝
        (Classical.choose (p := fun (x : Ω → ℝ) ↦
          StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) this ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))

Tactic:
rw [limitProcess, dif_pos this]

Premises used: dif_pos, MeasureTheory.Filtration.limitProcess
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ f n ω) atTop
      (𝓝
        (Classical.choose (p := fun (x : Ω → ℝ) ↦
          StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) this ω))

Tactic:
(Classical.choose_spec this).2

Premises used: Classical.choose_spec, And.right
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
this : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun (n : ℕ) ↦ f n ω) atTop
      (𝓝
        (Classical.choose (p := fun (x : Ω → ℝ) ↦
          StronglyMeasurable x ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (x ω))) this ω))

Tactic:
exact (Classical.choose_spec this).2

Premises used: Classical.choose_spec, And.right
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
ℱ₁ : ∃ (g : Ω → ℝ), StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g ω))
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))

Tactic:
suffices
      ∃ g, StronglyMeasurable[⨆ n, ℱ n] g ∧ ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω)) by
    rw [limitProcess, dif_pos this]
    exact (Classical.choose_spec this).2
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
⊢ ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0

Tactic:
have hle : ⨆ n, ℱ n ≤ m0 := sSup_le fun m ⟨n, hn⟩ => hn ▸ ℱ.le _
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
h :
  ∀ (ω : Ω) (hω : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))

Tactic:
filter_upwards [hf.exists_ae_trim_tendsto_of_bdd hbdd] with ω hω

Premises used: MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd
-- Module: Mathlib.Probability.Martingale.Convergence
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ (↑R : ℝ≥0∞)
g' : Ω → ℝ :=
  fun (ω : Ω) ↦
    if h : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c) then
      h.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))
    else 0
hle : ⨆ (n : ℕ), (↑ℱ : ℕ → MeasurableSpace Ω) n ≤ m0
ω : Ω
hω : ∃ (c : ℝ), Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c)
h : Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (hω.choose (p := fun (c : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 c))))
⊢ Tendsto (fun (n : ℕ) ↦ f n ω) atTop (𝓝 (g' ω))

Tactic:
simp_rw [g', dif_pos hω]

Premises used: dif_pos