awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hN : 0 < N
hab : a < b
hn : n < upcrossingsBefore a b f N ω
⊢ b - a ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω

Tactic:
sub_le_sub
    (stoppedValue_upperCrossingTime (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn).ne)
    (stoppedValue_lowerCrossingTime (lowerCrossingTime_lt_of_lt_upcrossingsBefore hN hab hn).ne)

Premises used: MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore, MeasureTheory.stoppedValue_lowerCrossingTime, MeasureTheory.lowerCrossingTime_lt_of_lt_upcrossingsBefore, MeasureTheory.stoppedValue_upperCrossingTime, sub_le_sub, LT.lt.ne
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ sSup {n : ℕ | upperCrossingTime a b f N n ω < N} < n

Tactic:
rw [upcrossingsBefore] at hn

Premises used: MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n : ℕ | upperCrossingTime a b f N n ω < N} < n
rw : ¬upperCrossingTime a b f N n ω < N
⊢ N ≤ upperCrossingTime a b f N n ω

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n : ℕ | upperCrossingTime a b f N n ω < N} < n
⊢ ¬upperCrossingTime a b f N n ω < N

Tactic:
fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)

Premises used: not_le, Iff.mpr, MeasureTheory.upperCrossingTime_lt_bddAbove, le_csSup, Not
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : sSup {n : ℕ | upperCrossingTime a b f N n ω < N} < n
⊢ ¬upperCrossingTime a b f N n ω < N

Tactic:
exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)

Premises used: not_le, Iff.mpr, MeasureTheory.upperCrossingTime_lt_bddAbove, le_csSup
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ N ≤ upperCrossingTime a b f N n ω

Tactic:
have : N ≤ upperCrossingTime a b f N n ω := by
    rw [upcrossingsBefore] at hn
    rw [← not_lt]
    exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : upcrossingsBefore a b f N ω < n
this : N ≤ upperCrossingTime a b f N n ω
⊢ stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (n + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N n ω) : WithTop ℕ)) ω =
    0

Tactic:
simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
    lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]

Premises used: MeasureTheory.stoppedValue, le_rfl, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.lowerCrossingTime_stabilize', Nat.le_succ, MeasureTheory.upperCrossingTime_stabilize', le_trans
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
pos :
  ∀ (hN : N = 0),
    (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
      ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
neg :
  ∀ (hN : ¬N = 0),
    (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
      ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

Tactic:
by_cases hN : N = 0
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : N = 0
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

Tactic:
simp [hN]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
neg :
  (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ x ∈ Finset.range N,
      ∑ x_1 ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

Tactic:
simp_rw [upcrossingStrat, Finset.sum_mul, ←
    Set.indicator_mul_left _ _ (fun x ↦ (f (x + 1) - f x) ω), Pi.one_apply, Pi.sub_apply, one_mul]

Premises used: Pi.one_apply, HSub.hSub, HAdd.hAdd, MeasureTheory.upcrossingStrat, OfNat.ofNat, Set.indicator_mul_left, one_mul, Finset.sum_mul, Pi.sub_apply
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
neg :
  (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ x ∈ Finset.range N,
      ∑ x_1 ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
rw :
  f (upperCrossingTime a b f N (k + 1) ω) ω - f (lowerCrossingTime a b f N k ω) ω =
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
rw₁ :
  {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
⊢ ∑ n ∈ Finset.range N,
      (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
        (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω

Tactic:
rw [Finset.sum_indicator_eq_sum_filter, (_ : Finset.filter (fun i => i ∈ Set.Ico
      (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) (Finset.range N) =
      Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)),
      Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,
      Finset.sum_range_sub fun n => f n ω, Finset.sum_range_sub fun n => f n ω, neg_sub,
      sub_add_sub_cancel]

Premises used: Finset.sum_Ico_eq_add_neg, neg_sub, sub_add_sub_cancel, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, Finset.sum_indicator_eq_sum_filter, Finset.sum_range_sub
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ f (upperCrossingTime a b f N (k + 1) ω) ω - f (lowerCrossingTime a b f N k ω) ω =
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω

Tactic:
rfl
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
h :
  ∀ (i : ℕ),
    i ∈ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} ↔
      i ∈ Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)
⊢ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Tactic:
ext i
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k i : ℕ
h : lowerCrossingTime a b f N k ω ≤ i → i < upperCrossingTime a b f N (k + 1) ω → i < N
⊢ i ∈ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} ↔
    i ∈ Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Tactic:
simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]

Premises used: Set.mem_Ico, and_imp, Finset.mem_range, and_iff_right_iff_imp, Finset.mem_filter, Finset.mem_Ico
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k i : ℕ
⊢ lowerCrossingTime a b f N k ω ≤ i → i < upperCrossingTime a b f N (k + 1) ω → i < N

Tactic:
fun _ h => lt_of_lt_of_le h upperCrossingTime_le

Premises used: MeasureTheory.upperCrossingTime_le, lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k i : ℕ
⊢ lowerCrossingTime a b f N k ω ≤ i → i < upperCrossingTime a b f N (k + 1) ω → i < N

Tactic:
exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le

Premises used: MeasureTheory.upperCrossingTime_le, lt_of_lt_of_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω

Tactic:
have h₁ : ∀ k, ∑ n ∈ Finset.range N, (Set.Ico (lowerCrossingTime a b f N k ω)
      (upperCrossingTime a b f N (k + 1) ω)).indicator (fun m => f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ (upperCrossingTime a b f N (k + 1) ω : ℕ)) ω -
        stoppedValue f (fun ω ↦ (lowerCrossingTime a b f N k ω : ℕ)) ω := by
    intro k
    rw [Finset.sum_indicator_eq_sum_filter, (_ : Finset.filter (fun i => i ∈ Set.Ico
      (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)) (Finset.range N) =
      Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)),
      Finset.sum_Ico_eq_add_neg _ lowerCrossingTime_le_upperCrossingTime_succ,
      Finset.sum_range_sub fun n => f n ω, Finset.sum_range_sub fun n => f n ω, neg_sub,
      sub_add_sub_cancel]
    · rfl
    · ext i
      simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]
      exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
neg :
  (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ x ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (x + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N x ω) : WithTop ℕ)) ω)
⊢ (b - a) * (↑(upcrossingsBefore a b f N ω) : ℝ) ≤
    ∑ y ∈ Finset.range N,
      ∑ x ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω)).indicator
          (fun (j : ℕ) ↦ f (j + 1) ω - f j ω) x

Tactic:
simp_rw [h₁]
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)),
    b - a ≤
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
⊢ LE.le (α := ℝ) (∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a))
    (∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))

Tactic:
gcongr ∑ k ∈ _, ?_ with i hi
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ b - a ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω

Tactic:
le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_

Premises used: Iff.mpr, MeasureTheory.le_sub_of_le_upcrossingsBefore, zero_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
h : i < upcrossingsBefore a b f N ω
⊢ b - a ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω

Tactic:
refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_

Premises used: Iff.mpr, MeasureTheory.le_sub_of_le_upcrossingsBefore, zero_lt_iff
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
h h₂ h₃ h₄ : ∀ (hi : i < upcrossingsBefore a b f N ω), i < upcrossingsBefore a b f N ω
⊢ i < upcrossingsBefore a b f N ω

Tactic:
rwa [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
⊢ LE.le (α := ℝ)
    (∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))

Tactic:
Finset.sum_le_sum_of_subset_of_nonneg
          (Finset.range_subset_range.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => ?_

Premises used: Iff.mpr, Finset.range_subset_range, MeasureTheory.upcrossingsBefore_le, Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
refine :
  ∀ i ∈ Finset.range N,
    ∀ (hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)),
      0 ≤
        stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
          stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
⊢ LE.le (α := ℝ)
    (∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))
    (∑ k ∈ Finset.range N,
      (stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω))

Tactic:
refine Finset.sum_le_sum_of_subset_of_nonneg
          (Finset.range_subset_range.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => ?_

Premises used: Iff.mpr, Finset.range_subset_range, MeasureTheory.upcrossingsBefore_le, Finset.sum_le_sum_of_subset_of_nonneg
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
pos :
  ∀ (hi' : i = upcrossingsBefore a b f N ω),
    0 ≤
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
neg :
  ∀ (hi' : ¬i = upcrossingsBefore a b f N ω),
    0 ≤
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω

Tactic:
by_cases hi' : i = upcrossingsBefore a b f N ω

Premises used: MeasureTheory.upcrossingsBefore
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
i : ℕ
h : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
hi' : i = upcrossingsBefore a b f N ω
pos :
  upcrossingsBefore a b f N ω ∈ Finset.range N →
    ∀ (hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)),
      0 ≤
        stoppedValue f
            (fun (ω_1 : Ω) ↦ (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω_1) : WithTop ℕ)) ω -
          stoppedValue f (fun (ω_1 : Ω) ↦ (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω_1) : WithTop ℕ))
            ω
⊢ 0 ≤
    stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (i + 1) ω) : WithTop ℕ)) ω -
      stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N i ω) : WithTop ℕ)) ω

Tactic:
subst hi'
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
pos :
  0 ≤
    f (WithTop.untopA (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω) : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
⊢ 0 ≤
    stoppedValue f (fun (ω_1 : Ω) ↦ (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω_1) : WithTop ℕ))
        ω -
      stoppedValue f (fun (ω_1 : Ω) ↦ (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω_1) : WithTop ℕ)) ω

Tactic:
simp only [stoppedValue]

Premises used: MeasureTheory.stoppedValue
-- Module: Mathlib.Probability.Martingale.Upcrossing
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun (m : ℕ) ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun (ω : Ω) ↦ (↑(upperCrossingTime a b f N (k + 1) ω) : WithTop ℕ)) ω -
        stoppedValue f (fun (ω : Ω) ↦ (↑(lowerCrossingTime a b f N k ω) : WithTop ℕ)) ω
h : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
pos :
  0 ≤
    f (WithTop.untopA (↑N : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω
⊢ 0 ≤
    f (WithTop.untopA (↑(upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω) : WithTop ℕ)) ω -
      f (WithTop.untopA (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) : WithTop ℕ)) ω

Tactic:
rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]

Premises used: Nat.lt_succ_self, MeasureTheory.upperCrossingTime_eq_of_upcrossingsBefore_lt