awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
neg₃ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₄ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₅ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₆ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card * 0
neg₇ : upcrossingsBefore a b f N ω = (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card + 0
neg₈ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 1 - 1 + 0
neg₉ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 0 + 0
neg₁₀ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 0
neg₁₁ neg₁₂ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)

Tactic:
rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]

Premises used: MulZeroClass.mul_zero, Nat.card_Ico, Nat.add_succ_sub_one, smul_eq_mul, mul_one, add_zero, Finset.sum_congr, rfl, Finset.sum_const
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
h :
  ∀ (ω : Ω),
    upcrossingsBefore a b f N ω =
      ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
⊢ upcrossingsBefore a b f N = fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
ext ω
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
upcrossingsBefore_eq_sum hab

Premises used: MeasureTheory.upcrossingsBefore_eq_sum
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
exact upcrossingsBefore_eq_sum hab

Premises used: MeasureTheory.upcrossingsBefore_eq_sum
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
⊢ upcrossingsBefore a b f N = fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
have : upcrossingsBefore a b f N = fun ω =>
      ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i := by
    ext ω
    exact upcrossingsBefore_eq_sum hab
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
rw :
  Measurable (β := ℕ) fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
⊢ Measurable (upcrossingsBefore a b f N)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
⊢ Measurable (β := ℕ) fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
Finset.measurable_fun_sum _ fun i _ => Measurable.indicator measurable_const <|
    ℱ.le N _ ?_

Premises used: setOf, Measurable.indicator, MeasureTheory.upperCrossingTime, LT.lt, Finset.measurable_fun_sum, MeasureTheory.Filtration.le, measurable_const
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
refine :
  ∀ i ∈ Finset.Ico 1 (N + 1), MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ {n : ℕ | upperCrossingTime a b f N n ω < N} i
⊢ Measurable (β := ℕ) fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i

Tactic:
refine Finset.measurable_fun_sum _ fun i _ => Measurable.indicator measurable_const <|
    ℱ.le N _ ?_

Premises used: Measurable.indicator, Finset.measurable_fun_sum, MeasureTheory.Filtration.le, measurable_const
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun (ω : Ω) ↦
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
i : ℕ
h : i ∈ Finset.Ico 1 (N + 1)
⊢ MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ {n : ℕ | upperCrossingTime a b f N n ω < N} i

Tactic:
simpa only [ENat.some_eq_coe, Nat.cast_lt] using
    hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N

Premises used: ENat.some_eq_coe, MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime, MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred, Nat.cast_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
h : ∀ (ω : Ω), norm (E := ℝ) (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑N : ℝ)
⊢ ∀ᵐ (ω : Ω) ∂μ, norm (E := ℝ) (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑N : ℝ)

Tactic:
filter_upwards with ω
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
ω : Ω
h : upcrossingsBefore a b f N ω ≤ N
⊢ norm (E := ℝ) (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑N : ℝ)

Tactic:
rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]

Premises used: Nat.abs_cast, Nat.cast_le, Real.norm_eq_abs
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
upcrossingsBefore_le _ _ hab

Premises used: MeasureTheory.upcrossingsBefore_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω ≤ N

Tactic:
exact upcrossingsBefore_le _ _ hab

Premises used: MeasureTheory.upcrossingsBefore_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
⊢ Measurable (upcrossings a b f)

Tactic:
.iSup fun _ => measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)

Premises used: measurable_from_top, Measurable.comp, Measurable.iSup, MeasureTheory.upcrossings, MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
mp : upcrossings a b f ω < ∞ → ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
mpr : (∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)) → upcrossings a b f ω < ∞
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
h : upcrossings a b f ω < ∞
⊢ upcrossings a b f ω ≠ ∞

Tactic:
h.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
h : upcrossings a b f ω < ∞
mp :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) = upcrossings a b f ω)
    (upcrossings_lt_top_iff : (↑r : ℝ≥0∞) < ∞ ↔ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k)
    (h : (↑r : ℝ≥0∞) < ∞), ∃ (k : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
⊢ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)

Tactic:
lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr

Premises used: MeasureTheory.upcrossings, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ≥0
hr : (↑r : ℝ≥0∞) = upcrossings a b f ω
upcrossings_lt_top_iff : (↑r : ℝ≥0∞) < ∞ ↔ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
h : (↑r : ℝ≥0∞) < ∞
⊢ ∃ (k : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)

Tactic:
⟨r, le_rfl⟩

Premises used: le_rfl, Exists.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
r : ℝ≥0
hr : (↑r : ℝ≥0∞) = upcrossings a b f ω
upcrossings_lt_top_iff : (↑r : ℝ≥0∞) < ∞ ↔ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
h : (↑r : ℝ≥0∞) < ∞
⊢ ∃ (k : ℝ≥0), (↑r : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)

Tactic:
exact ⟨r, le_rfl⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
k : ℝ≥0
hk : upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
⊢ upcrossings a b f ω < ∞

Tactic:
lt_of_le_of_lt hk ENNReal.coe_lt_top

Premises used: lt_of_le_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
k : ℝ≥0
hk : upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
⊢ upcrossings a b f ω < ∞

Tactic:
exact lt_of_le_of_lt hk ENNReal.coe_lt_top

Premises used: lt_of_le_of_lt, ENNReal.coe_lt_top
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)

Tactic:
have : upcrossings a b f ω < ∞ ↔ ∃ k : ℝ≥0, upcrossings a b f ω ≤ k := by
    constructor
    · intro h
      lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
      exact ⟨r, le_rfl⟩
    · rintro ⟨k, hk⟩
      exact lt_of_le_of_lt hk ENNReal.coe_lt_top
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
simp_rw :
  (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) ↔
    ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
simp_rw [this, upcrossings, iSup_le_iff]

Premises used: MeasureTheory.upcrossings, iSup_le_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
mp :
  (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) →
    ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
mpr :
  (∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k) →
    ∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
⊢ (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) ↔
    ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
constructor
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℝ≥0
hk : ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
mp : ∀ (m : ℕ) (hm : k ≤ (↑m : ℝ≥0)), ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
obtain ⟨m, hm⟩ := exists_nat_ge k

Premises used: exists_nat_ge
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℝ≥0
hk : ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
m : ℕ
hm : k ≤ (↑m : ℝ≥0)
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩

Premises used: Exists.intro, Iff.mp, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℝ≥0
hk : ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
m : ℕ
hm : k ≤ (↑m : ℝ≥0)
mp : ∀ (N : ℕ), (↑k : ℝ≥0∞) ≤ (↑m : ℝ≥0∞)
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℝ≥0
hk : ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
m : ℕ
hm : k ≤ (↑m : ℝ≥0)
N : ℕ
mp : (↑k : ℝ≥0∞) ≤ (↑(↑m : ℝ≥0) : ℝ≥0∞)
mp₁ mp₂ mp₃ mp₄ : k ≤ (↑m : ℝ≥0)
⊢ (↑k : ℝ≥0∞) ≤ (↑m : ℝ≥0∞)

Tactic:
rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, ENNReal.coe_natCast
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)

Tactic:
⟨k, fun N => ?_⟩

Premises used: Nat.cast, Exists.intro
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
mpr : ∀ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ≤ (↑(↑k : ℝ≥0) : ℝ≥0∞)
⊢ ∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)

Tactic:
refine ⟨k, fun N => ?_⟩
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
N : ℕ
⊢ (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ≤ (↑(↑k : ℝ≥0) : ℝ≥0∞)

Tactic:
simp only [ENNReal.coe_natCast, Nat.cast_le, hk N]

Premises used: Nat.cast_le, ENNReal.coe_natCast
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
pos :
  ∀ (hab : a < b),
    ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
neg :
  ∀ (hab : b ≤ a),
    ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
by_cases! hab : a < b
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
hfi : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (f N ω - a)⁺) μ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ (f N ω - a)⁺
⊢ ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (f N ω - a)⁺) μ

Tactic:
(hf.sub_martingale (martingale_const _ _ _)).pos.integrable _

Premises used: MeasureTheory.martingale_const, MeasureTheory.Submartingale.integrable, MeasureTheory.Submartingale.pos, MeasureTheory.Submartingale.sub_martingale
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (f N ω - a)⁺) μ

Tactic:
exact (hf.sub_martingale (martingale_const _ _ _)).pos.integrable _

Premises used: MeasureTheory.martingale_const, MeasureTheory.Submartingale.integrable, MeasureTheory.Submartingale.pos, MeasureTheory.Submartingale.sub_martingale
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ (f N ω - a)⁺

Tactic:
Eventually.of_forall fun ω => posPart_nonneg _

Premises used: posPart_nonneg, HSub.hSub, Filter.Eventually.of_forall, Filter.EventuallyLE
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ (f N ω - a)⁺

Tactic:
exact Eventually.of_forall fun ω => posPart_nonneg _

Premises used: posPart_nonneg, Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
⊢ ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
have : ∀ N, ∫⁻ ω, ENNReal.ofReal ((f N ω - a)⁺) ∂μ = ENNReal.ofReal (∫ ω, (f N ω - a)⁺ ∂μ) := by
      intro N
      rw [ofReal_integral_eq_lintegral_ofReal]
      · exact (hf.sub_martingale (martingale_const _ _ _)).pos.integrable _
      · exact Eventually.of_forall fun ω => posPart_nonneg _
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
pos :
  ENNReal.ofReal (b - a) * ⨆ (n : ℕ), ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f n a_1) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
pos₁ : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ (↑(upcrossingsBefore a b f n ω) : ℝ≥0∞)) μ
pos₂ : ∀ᵐ (x : Ω) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(upcrossingsBefore a b f n x) : ℝ≥0∞)
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
rw [lintegral_iSup']

Premises used: MeasureTheory.lintegral_iSup'
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
pos :
  ∀ (i : ℕ),
    ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f i a_1) : ℝ≥0∞) ∂μ ≤
      ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ (n : ℕ), ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f n a_1) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]

Premises used: iSup_le_iff, ENNReal.mul_iSup
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
N : ℕ
⊢ ∫⁻ (ω : Ω), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ∂μ =
    ∫⁻ (ω : Ω), (↑(↑(upcrossingsBefore a b f N ω) : ℝ≥0) : ℝ≥0∞) ∂μ

Tactic:
simp
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
N : ℕ
pos :
  ENNReal.ofReal ((b - a) * ∫ (a_1 : Ω), (↑(↑(upcrossingsBefore a b f N a_1) : ℝ≥0) : ℝ) ∂μ) ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
pos₁ : Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(↑(upcrossingsBefore a b f N x) : ℝ≥0) : ℝ)) μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f N a_1) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
rw [(by simp :
          ∫⁻ ω, upcrossingsBefore a b f N ω ∂μ = ∫⁻ ω, ↑(upcrossingsBefore a b f N ω : ℝ≥0) ∂μ),
        lintegral_coe_eq_integral, ← ENNReal.ofReal_mul (sub_pos.2 hab).le]

Premises used: Iff.mpr, sub_pos, ENNReal.ofReal_mul, LT.lt.le, MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
N : ℕ
⊢ ENNReal.ofReal ((b - a) * ∫ (a_1 : Ω), (↑(upcrossingsBefore a b f N a_1) : ℝ) ∂μ) ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)

Tactic:
(ENNReal.ofReal_le_ofReal
          (hf.mul_integral_upcrossingsBefore_le_integral_pos_part a b N)).trans
            (le_iSup (α := ℝ≥0∞) _ N)

Premises used: MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part, ENNReal.ofReal_le_ofReal, le_iSup, LE.le.trans