awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ 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)
have neg₉ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 0 + 0
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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ 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)
have neg₁₀ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 0
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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ 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)
have neg₁₁ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω
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]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
have h : ∀ (ω : Ω),
  upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
⊢ Measurable (upcrossingsBefore a b f N)
have 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
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
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 (upcrossingsBefore a b f N)
have rw : Measurable (β := ℕ) fun (ω : Ω) ↦
  ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
have refine : ∀ i ∈ Finset.Ico 1 (N + 1), MeasurableSet.{u_1} (α := Ω) fun (ω : Ω) ↦ {n : ℕ | upperCrossingTime a b f N n ω < N} i
Tactic: refine Finset.measurable_fun_sum _ fun i _ => Measurable.indicator measurable_const <|
    ℱ.le N _ ?_
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, norm (E := ℝ) (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑N : ℝ)
have h : ∀ (ω : Ω), norm (E := ℝ) (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑N : ℝ)
Tactic: filter_upwards with ω
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
hf : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ f
hab : a < b
ω : Ω
⊢ norm (E := ℝ) (↑(upcrossingsBefore a b f N ω) : ℝ) ≤ (↑N : ℝ)
have h : upcrossingsBefore a b f N ω ≤ N
Tactic: rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
have mp : upcrossings a b f ω < ∞ → ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
mp : upcrossings a b f ω < ∞ → ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
have mpr : (∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)) → upcrossings a b f ω < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
h : upcrossings a b f ω < ∞
⊢ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
have 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∞)
Tactic: lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
⊢ upcrossings a b f ω < ∞ ↔ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
have simp_rw : (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) ↔
  ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Tactic: simp_rw [this, upcrossings, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ (k : ℝ≥0), upcrossings a b f ω ≤ (↑k : ℝ≥0∞)
⊢ (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) ↔
    ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
have mp : (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) →
  ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
⊢ (∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)) ↔
    ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
have mpr : (∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k) →
  ∃ (k : ℝ≥0), ∀ (i : ℕ), (↑(upcrossingsBefore a b f i ω) : ℝ≥0∞) ≤ (↑k : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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∞)
⊢ ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
have mp : ∀ (m : ℕ) (hm : k ≤ (↑m : ℝ≥0)), ∃ (k : ℕ), ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Tactic: obtain ⟨m, hm⟩ := exists_nat_ge k
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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
have mp : ∀ (N : ℕ), (↑k : ℝ≥0∞) ≤ (↑m : ℝ≥0∞)
Tactic: refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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 : ℕ
⊢ (↑k : ℝ≥0∞) ≤ (↑m : ℝ≥0∞)
have mp : (↑k : ℝ≥0∞) ≤ (↑(↑m : ℝ≥0) : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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∞)
have mpr : ∀ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ≤ (↑(↑k : ℝ≥0) : ℝ≥0∞)
Tactic: refine ⟨k, fun N => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have pos : ∀ (hab : a < b),
  ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
Tactic: by_cases! hab : a < b
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have neg : ∀ (hab : b ≤ a),
  ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
Tactic: by_cases! hab : a < b
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺ ∂μ)
have hfi : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (f N ω - a)⁺) μ
Tactic: rw [ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺) μ
⊢ ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
have f_nn : (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ (f N ω - a)⁺
Tactic: rw [ofReal_integral_eq_lintegral_ofReal]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have this : ∀ (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 _
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have pos : ENNReal.ofReal (b - a) * ⨆ (n : ℕ), ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f n a_1) : ℝ≥0∞) ∂μ ≤
  ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
Tactic: rw [lintegral_iSup']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have pos₁ : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (ω : Ω) ↦ (↑(upcrossingsBefore a b f n ω) : ℝ≥0∞)) μ
Tactic: rw [lintegral_iSup']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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∞)) μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ (N : ℕ), (↑(upcrossingsBefore a b f N ω) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have pos₂ : ∀ᵐ (x : Ω) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (↑(upcrossingsBefore a b f n x) : ℝ≥0∞)
Tactic: rw [lintegral_iSup']
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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)⁺ ∂μ)
⊢ ENNReal.ofReal (b - a) * ⨆ (n : ℕ), ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f n a_1) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
have pos : ∀ (i : ℕ),
  ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), (↑(upcrossingsBefore a b f i a_1) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
Tactic: simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
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) : ℝ≥0∞) ∂μ ≤
    ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
have pos : 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]