-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem mul_upcrossingsBefore_le (hf : a ≤ f N ω) (hab : a < b) :
    (b - a) * upcrossingsBefore a b f N ω ≤
    ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω

Proof state:
case pos
Ω : 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]

Result:
no goals

Proof state:
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
⊢ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)

Tactic:
refine Finset.sum_le_sum fun i hi =>
  le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_

Result:
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
i : ℕ
hi : i ∈ Finset.range (upcrossingsBefore a b f N ω)
⊢ i < upcrossingsBefore a b f N ω

Proof state:
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
⊢ ∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) ≤
    ∑ k ∈ Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)

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

Result:
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
i : ℕ
x✝ : i ∈ Finset.range N
hi : i ∉ Finset.range (upcrossingsBefore a b f N ω)
⊢ 0 ≤ stoppedValue f (upperCrossingTime a b f N (i + 1)) ω - stoppedValue f (lowerCrossingTime a b f N i) ω

Proof state:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k i : ℕ
⊢ i ∈
      Finset.filter (fun i => i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
        (Finset.range N) ↔
    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]

Result:
case h
Ω : 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

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ 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) ω)

Tactic:
ext i

Result:
case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k i : ℕ
⊢ i ∈
      Finset.filter (fun i => i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
        (Finset.range N) ↔
    i ∈ Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Proof state:
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω

Tactic:
rfl

Result:
no goals

Proof state:
case h
Ω : 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

Result:
no goals

Proof state:
case pos
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
⊢ 0 ≤ f N ω - f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) ω

Tactic:
by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N

Result:
case pos
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f N ω - f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) ω

case neg
Ω : 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 (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f N ω - f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
⊢ (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

Result:
case pos
Ω : 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) ω

case neg
Ω : 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) ω