[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
⊢ upperCrossingTime a b f N (n + 1) ω =
    hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
[PROOFSTEP]
rw [upperCrossingTime]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω✝ ω : Ω
⊢ upperCrossingTime a b f N (n + 1) ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω
[PROOFSTEP]
simp only [upperCrossingTime_succ]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω✝ ω : Ω
⊢ hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω =
    hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ N
[PROOFSTEP]
cases n
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
m : ℕ
ω : Ω
⊢ upperCrossingTime a b f N Nat.zero ω ≤ N
[PROOFSTEP]
simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le, Nat.zero_eq]
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
m : ℕ
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (Nat.succ n✝) ω ≤ N
[PROOFSTEP]
simp only [upperCrossingTime_succ, hitting_le]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ N
[PROOFSTEP]
simp only [lowerCrossingTime, hitting_le ω]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω
[PROOFSTEP]
simp only [lowerCrossingTime, le_hitting upperCrossingTime_le ω]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤ upperCrossingTime a b f N (n + 1) ω
[PROOFSTEP]
rw [upperCrossingTime_succ]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hitting f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
[PROOFSTEP]
exact le_hitting lowerCrossingTime_le ω
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω
[PROOFSTEP]
suffices Monotone fun n => lowerCrossingTime a b f N n ω by exact this hnm
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone fun n => lowerCrossingTime a b f N n ω
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω
[PROOFSTEP]
exact this hnm
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n => lowerCrossingTime a b f N n ω
[PROOFSTEP]
exact
  monotone_nat_of_le_succ fun n =>
    le_trans lowerCrossingTime_le_upperCrossingTime_succ upperCrossingTime_le_lowerCrossingTime
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω
[PROOFSTEP]
suffices Monotone fun n => upperCrossingTime a b f N n ω by exact this hnm
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone fun n => upperCrossingTime a b f N n ω
⊢ upperCrossingTime a b f N n ω ≤ upperCrossingTime a b f N m ω
[PROOFSTEP]
exact this hnm
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n => upperCrossingTime a b f N n ω
[PROOFSTEP]
exact
  monotone_nat_of_le_succ fun n =>
    le_trans upperCrossingTime_le_lowerCrossingTime lowerCrossingTime_le_upperCrossingTime_succ
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
⊢ stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := (hitting_le_iff_of_lt _ (lt_of_le_of_ne lowerCrossingTime_le h)).1 le_rfl
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
h : lowerCrossingTime a b f N n ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (upperCrossingTime a b f N n ω) (lowerCrossingTime a b f N n ω)
hj₂ : f j ω ∈ Set.Iic a
⊢ stoppedValue f (lowerCrossingTime a b f N n) ω ≤ a
[PROOFSTEP]
exact stoppedValue_hitting_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 lowerCrossingTime_le⟩, hj₂⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := (hitting_le_iff_of_lt _ (lt_of_le_of_ne upperCrossingTime_le h)).1 le_rfl
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
j : ℕ
hj₁ :
  j ∈
    Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N (Nat.add n 0) ω) N ω)
      (upperCrossingTime a b f N (n + 1) ω)
hj₂ : f j ω ∈ Set.Ici b
⊢ b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω
[PROOFSTEP]
exact stoppedValue_hitting_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 (hitting_le _)⟩, hj₂⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
⊢ upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω
[PROOFSTEP]
refine'
  lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
    not_le.2 hab <| le_trans _ (stoppedValue_lowerCrossingTime hn)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ stoppedValue f (lowerCrossingTime a b f N (n + 1)) ω
[PROOFSTEP]
simp only [stoppedValue]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (lowerCrossingTime a b f N (n + 1) ω) ω
[PROOFSTEP]
rw [← h]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (upperCrossingTime a b f N (n + 1) ω) ω
[PROOFSTEP]
exact stoppedValue_upperCrossingTime (h.symm ▸ hn)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω
[PROOFSTEP]
refine'
  lt_of_le_of_ne lowerCrossingTime_le_upperCrossingTime_succ fun h =>
    not_le.2 hab <| le_trans (stoppedValue_upperCrossingTime hn) _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω ≤ a
[PROOFSTEP]
simp only [stoppedValue]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (upperCrossingTime a b f N (n + 1) ω) ω ≤ a
[PROOFSTEP]
rw [← h]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
hn : upperCrossingTime a b f N (n + 1) ω ≠ N
h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω
⊢ f (lowerCrossingTime a b f N n ω) ω ≤ a
[PROOFSTEP]
exact stoppedValue_lowerCrossingTime (h.symm ▸ hn)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ ∃ n, upperCrossingTime a b f N n ω = N
[PROOFSTEP]
by_contra h
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ¬∃ n, upperCrossingTime a b f N n ω = N
⊢ False
[PROOFSTEP]
push_neg at h
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
⊢ False
[PROOFSTEP]
have : StrictMono fun n => upperCrossingTime a b f N n ω :=
  strictMono_nat_of_lt_succ fun n => upperCrossingTime_lt_succ hab (h _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n => upperCrossingTime a b f N n ω
⊢ False
[PROOFSTEP]
obtain ⟨_, ⟨k, rfl⟩, hk⟩ : ∃ (m : _) (_ : m ∈ Set.range fun n => upperCrossingTime a b f N n ω), N < m :=
  ⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩, lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩
[GOAL]
case intro.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n => upperCrossingTime a b f N n ω
k : ℕ
hk : N < (fun n => upperCrossingTime a b f N n ω) k
⊢ False
[PROOFSTEP]
exact not_le.2 hk upperCrossingTime_le
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
⊢ BddAbove {n | upperCrossingTime a b f N n ω < N}
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_upperCrossingTime_eq f N ω hab
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
⊢ BddAbove {n | upperCrossingTime a b f N n ω < N}
[PROOFSTEP]
refine' ⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => _⟩
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ k
[PROOFSTEP]
by_contra hn'
[GOAL]
case intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hn' : ¬n ≤ k
⊢ False
[PROOFSTEP]
exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upperCrossingTime a b f N N ω = N
[PROOFSTEP]
by_cases hN' : N < Nat.find (exists_upperCrossingTime_eq f N ω hab)
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
⊢ upperCrossingTime a b f N N ω = N
[PROOFSTEP]
refine' le_antisymm upperCrossingTime_le _
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
⊢ N ≤ upperCrossingTime a b f N N ω
[PROOFSTEP]
have hmono :
  StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.find (exists_upperCrossingTime_eq f N ω hab)).pred) :=
  by
  refine' strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab _
  rw [Nat.lt_pred_iff] at hm
  convert Nat.find_min _ hm
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
⊢ StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.pred (Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N))))
[PROOFSTEP]
refine' strictMonoOn_Iic_of_lt_succ fun m hm => upperCrossingTime_lt_succ hab _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m✝ : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
m : ℕ
hm : m < Nat.pred (Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N))
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N
[PROOFSTEP]
rw [Nat.lt_pred_iff] at hm
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m✝ : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
m : ℕ
hm : Nat.succ m < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
⊢ upperCrossingTime a b f N (m + 1) ω ≠ N
[PROOFSTEP]
convert Nat.find_min _ hm
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
hmono :
  StrictMonoOn (fun n => upperCrossingTime a b f N n ω)
    (Set.Iic (Nat.pred (Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N))))
⊢ N ≤ upperCrossingTime a b f N N ω
[PROOFSTEP]
convert StrictMonoOn.Iic_id_le hmono N (Nat.le_pred_of_lt hN')
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : ¬N < Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N)
⊢ upperCrossingTime a b f N N ω = N
[PROOFSTEP]
rw [not_lt] at hN'
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN' : Nat.find (_ : ∃ n, upperCrossingTime a b f N n ω = N) ≤ N
⊢ upperCrossingTime a b f N N ω = N
[PROOFSTEP]
exact upperCrossingTime_stabilize hN' (Nat.find_spec (exists_upperCrossingTime_eq f N ω hab))
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N n) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N n)
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N Nat.zero) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N Nat.zero)
[PROOFSTEP]
refine' ⟨isStoppingTime_const _ 0, _⟩
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ IsStoppingTime ℱ (lowerCrossingTime a b f N Nat.zero)
[PROOFSTEP]
simp [hitting_isStoppingTime hf measurableSet_Iic]
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
ih : IsStoppingTime ℱ (upperCrossingTime a b f N k) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (Nat.succ k)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (Nat.succ k))
[PROOFSTEP]
obtain ⟨_, ih₂⟩ := ih
[GOAL]
case succ.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (Nat.succ k)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (Nat.succ k))
[PROOFSTEP]
have : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) :=
  by
  intro n
  simp_rw [upperCrossingTime_succ_eq]
  exact isStoppingTime_hitting_isStoppingTime ih₂ (fun _ => lowerCrossingTime_le) measurableSet_Ici hf _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
[PROOFSTEP]
intro n
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
n : ℕ
⊢ MeasurableSet {ω | upperCrossingTime a b f N (k + 1) ω ≤ n}
[PROOFSTEP]
simp_rw [upperCrossingTime_succ_eq]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
n : ℕ
⊢ MeasurableSet {ω | hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω ≤ n}
[PROOFSTEP]
exact isStoppingTime_hitting_isStoppingTime ih₂ (fun _ => lowerCrossingTime_le) measurableSet_Ici hf _
[GOAL]
case succ.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
⊢ IsStoppingTime ℱ (upperCrossingTime a b f N (Nat.succ k)) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N (Nat.succ k))
[PROOFSTEP]
refine' ⟨this, _⟩
[GOAL]
case succ.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
⊢ IsStoppingTime ℱ (lowerCrossingTime a b f N (Nat.succ k))
[PROOFSTEP]
intro n
[GOAL]
case succ.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
k : ℕ
left✝ : IsStoppingTime ℱ (upperCrossingTime a b f N k)
ih₂ : IsStoppingTime ℱ (lowerCrossingTime a b f N k)
this : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1))
n : ℕ
⊢ MeasurableSet {ω | lowerCrossingTime a b f N (Nat.succ k) ω ≤ n}
[PROOFSTEP]
exact isStoppingTime_hitting_isStoppingTime this (fun _ => upperCrossingTime_le) measurableSet_Iic hf _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ upcrossingStrat a b f N n ω ≤ 1
[PROOFSTEP]
rw [upcrossingStrat, ← Set.indicator_finset_biUnion_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ Set.indicator
      (⋃ (i : ℕ) (_ : i ∈ Finset.range N),
        Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
      1 n ≤
    1
[PROOFSTEP]
exact Set.indicator_le_self' (fun _ _ => zero_le_one) _
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ ∀ (i : ℕ),
    i ∈ Finset.range N →
      ∀ (j : ℕ),
        j ∈ Finset.range N →
          i ≠ j →
            Disjoint (Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
              (Set.Ico (lowerCrossingTime a b f N j ω) (upperCrossingTime a b f N (j + 1) ω))
[PROOFSTEP]
intro i _ j _ hij
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
⊢ Disjoint (Set.Ico (lowerCrossingTime a b f N i ω) (upperCrossingTime a b f N (i + 1) ω))
    (Set.Ico (lowerCrossingTime a b f N j ω) (upperCrossingTime a b f N (j + 1) ω))
[PROOFSTEP]
rw [Set.Ico_disjoint_Ico]
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
[PROOFSTEP]
obtain hij' | hij' := lt_or_gt_of_ne hij
[GOAL]
case h.inl
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
hij' : i < j
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
[PROOFSTEP]
rw [min_eq_left
    (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) : upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
  max_eq_right (lowerCrossingTime_mono hij'.le : lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
[GOAL]
case h.inl
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
hij' : i < j
⊢ upperCrossingTime a b f N (Nat.succ i) ω ≤ lowerCrossingTime a b f N j ω
[PROOFSTEP]
refine' le_trans upperCrossingTime_le_lowerCrossingTime (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))
[GOAL]
case h.inr
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
hij' : i > j
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
[PROOFSTEP]
rw [gt_iff_lt] at hij'
[GOAL]
case h.inr
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
hij' : j < i
⊢ min (upperCrossingTime a b f N (i + 1) ω) (upperCrossingTime a b f N (j + 1) ω) ≤
    max (lowerCrossingTime a b f N i ω) (lowerCrossingTime a b f N j ω)
[PROOFSTEP]
rw [min_eq_right
    (upperCrossingTime_mono (Nat.succ_le_succ hij'.le) : upperCrossingTime a b f N _ ω ≤ upperCrossingTime a b f N _ ω),
  max_eq_left (lowerCrossingTime_mono hij'.le : lowerCrossingTime a b f N _ _ ≤ lowerCrossingTime _ _ _ _ _ _)]
[GOAL]
case h.inr
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
i : ℕ
a✝¹ : i ∈ Finset.range N
j : ℕ
a✝ : j ∈ Finset.range N
hij : i ≠ j
hij' : j < i
⊢ upperCrossingTime a b f N (Nat.succ j) ω ≤ lowerCrossingTime a b f N i ω
[PROOFSTEP]
refine' le_trans upperCrossingTime_le_lowerCrossingTime (lowerCrossingTime_mono (Nat.succ_le_of_lt hij'))
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ Adapted ℱ (upcrossingStrat a b f N)
[PROOFSTEP]
intro n
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n : ℕ
⊢ StronglyMeasurable (upcrossingStrat a b f N n)
[PROOFSTEP]
change
  StronglyMeasurable[ℱ n] fun ω =>
    ∑ k in Finset.range N,
      ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n : ℕ
⊢ StronglyMeasurable fun ω =>
    ∑ k in Finset.range N,
      Set.indicator ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}) 1 n
[PROOFSTEP]
refine'
  Finset.stronglyMeasurable_sum _ fun i _ =>
    stronglyMeasurable_const.indicator ((hf.isStoppingTime_lowerCrossingTime n).inter _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω => setOf (fun n => n < upperCrossingTime a b f N (i + 1) ω) n
[PROOFSTEP]
simp_rw [← not_le]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n✝ m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω => setOf (fun n => ¬upperCrossingTime a b f N (i + 1) ω ≤ n) n
[PROOFSTEP]
exact (hf.isStoppingTime_upperCrossingTime n).compl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ Submartingale (fun n => ∑ k in Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ
[PROOFSTEP]
refine'
  hf.sum_mul_sub (fun n => (adapted_const ℱ 1 n).sub (hf.adapted.upcrossingStrat_adapted n))
    (_ : ∀ n ω, (1 - upcrossingStrat a b f N n) ω ≤ 1) _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), (1 - upcrossingStrat a b f N n) ω ≤ 1
[PROOFSTEP]
exact fun n ω => sub_le_self _ upcrossingStrat_nonneg
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), 0 ≤ (1 - upcrossingStrat a b f N n) ω
[PROOFSTEP]
intro n ω
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n✝ m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N n : ℕ
ω : Ω
⊢ 0 ≤ (1 - upcrossingStrat a b f N n) ω
[PROOFSTEP]
simp [upcrossingStrat_le_one]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
[PROOFSTEP]
have h₁ : (0 : ℝ) ≤ μ[∑ k in Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] :=
  by
  have := (hf.sum_sub_upcrossingStrat_mul a b N).set_integral_le (zero_le n) MeasurableSet.univ
  rw [integral_univ, integral_univ] at this
  refine' le_trans _ this
  simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
⊢ 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
have := (hf.sum_sub_upcrossingStrat_mul a b N).set_integral_le (zero_le n) MeasurableSet.univ
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
this :
  ∫ (ω : Ω) in Set.univ,
      Finset.sum (Finset.range 0) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ω ∂μ ≤
    ∫ (ω : Ω) in Set.univ,
      Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ω ∂μ
⊢ 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
rw [integral_univ, integral_univ] at this
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
this :
  ∫ (x : Ω), Finset.sum (Finset.range 0) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
refine' le_trans _ this
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
this :
  ∫ (x : Ω), Finset.sum (Finset.range 0) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range 0) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
[PROOFSTEP]
have h₂ :
  μ[∑ k in Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] =
    μ[∑ k in Finset.range n, (f (k + 1) - f k)] -
      μ[∑ k in Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)] :=
  by
  simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply, Pi.mul_apply]
  refine'
    integral_sub
      (Integrable.sub (integrable_finset_sum _ fun i _ => hf.integrable _)
        (integrable_finset_sum _ fun i _ => hf.integrable _))
      _
  convert (hf.sum_upcrossingStrat_mul a b N).integrable n using 1
  ext; simp
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ -
      ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply, Pi.mul_apply]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω),
      ∑ x_1 in Finset.range n, f (x_1 + 1) x - ∑ x_1 in Finset.range n, f x_1 x -
        ∑ x_1 in Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x) ∂μ =
    ∫ (x : Ω), ∑ x_1 in Finset.range n, f (x_1 + 1) x - ∑ x_1 in Finset.range n, f x_1 x ∂μ -
      ∫ (x : Ω), ∑ x_1 in Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x) ∂μ
[PROOFSTEP]
refine'
  integral_sub
    (Integrable.sub (integrable_finset_sum _ fun i _ => hf.integrable _)
      (integrable_finset_sum _ fun i _ => hf.integrable _))
    _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ Integrable fun x => ∑ x_1 in Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x)
[PROOFSTEP]
convert (hf.sum_upcrossingStrat_mul a b N).integrable n using 1
[GOAL]
case h.e'_5
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
⊢ (fun x => ∑ x_1 in Finset.range n, upcrossingStrat a b f N x_1 x * (f (x_1 + 1) x - f x_1 x)) =
    ∑ k in Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
x✝ : Ω
⊢ ∑ x in Finset.range n, upcrossingStrat a b f N x x✝ * (f (x + 1) x✝ - f x x✝) =
    Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x✝
[PROOFSTEP]
simp
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ : 0 ≤ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ
h₂ :
  ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ -
      ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
[PROOFSTEP]
rw [h₂, sub_nonneg] at h₁
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ
h₂ :
  ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ -
      ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
[PROOFSTEP]
refine' le_trans h₁ _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
h₁ :
  ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ ≤
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ
h₂ :
  ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) x ∂μ =
    ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ -
      ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
⊢ ∫ (x : Ω), Finset.sum (Finset.range n) (fun k => f (k + 1) - f k) x ∂μ ≤ ∫ (x : Ω), f n x ∂μ - ∫ (x : Ω), f 0 x ∂μ
[PROOFSTEP]
simp_rw [Finset.sum_range_sub, integral_sub' (hf.integrable _) (hf.integrable _), le_refl]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f✝ : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f ⊥ ω = ⊥
[PROOFSTEP]
simp [upcrossingsBefore]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ upcrossingsBefore a b f 0 ω = 0
[PROOFSTEP]
simp [upcrossingsBefore]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ upcrossingsBefore a b f 0 = 0
[PROOFSTEP]
ext ω
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
ω : Ω
⊢ upcrossingsBefore a b f 0 ω = OfNat.ofNat 0 ω
[PROOFSTEP]
exact upcrossingsBefore_zero
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ upperCrossingTime a b f N n ω = N
[PROOFSTEP]
refine' le_antisymm upperCrossingTime_le (not_lt.1 _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ ¬upperCrossingTime a b f N n ω < N
[PROOFSTEP]
convert not_mem_of_csSup_lt hn (upperCrossingTime_lt_bddAbove hab)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f N ω ≤ N
[PROOFSTEP]
by_cases hN : N = 0
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω ≤ N
[PROOFSTEP]
subst hN
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
⊢ upcrossingsBefore a b f 0 ω ≤ 0
[PROOFSTEP]
rw [upcrossingsBefore_zero]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω ≤ N
[PROOFSTEP]
refine' csSup_le ⟨0, zero_lt_iff.2 hN⟩ fun n (hn : _ < N) => _
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N n✝ m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ N
[PROOFSTEP]
by_contra hnN
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f✝ : ℕ → Ω → ℝ
N n✝ m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hN : ¬N = 0
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hnN : ¬n ≤ N
⊢ False
[PROOFSTEP]
exact hn.ne (upperCrossingTime_eq_of_bound_le hab (not_le.1 hnN).le)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
[PROOFSTEP]
have h' : upperCrossingTime a b f N n ω < N := lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime h
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h : lowerCrossingTime a b f N Nat.zero ω < N
h' : upperCrossingTime a b f N Nat.zero ω < N
⊢ upperCrossingTime a b f M Nat.zero ω = upperCrossingTime a b f N Nat.zero ω ∧
    lowerCrossingTime a b f M Nat.zero ω = lowerCrossingTime a b f N Nat.zero ω
[PROOFSTEP]
simp only [Nat.zero_eq, upperCrossingTime_zero, bot_eq_zero', eq_self_iff_true, lowerCrossingTime_zero, true_and_iff,
  eq_comm]
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h : lowerCrossingTime a b f N Nat.zero ω < N
h' : upperCrossingTime a b f N Nat.zero ω < N
⊢ hitting f (Set.Iic a) 0 N ω = hitting f (Set.Iic a) 0 M ω
[PROOFSTEP]
refine' hitting_eq_hitting_of_exists hNM _
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h : lowerCrossingTime a b f N Nat.zero ω < N
h' : upperCrossingTime a b f N Nat.zero ω < N
⊢ ∃ j, j ∈ Set.Icc 0 N ∧ f j ω ∈ Set.Iic a
[PROOFSTEP]
rw [lowerCrossingTime, hitting_lt_iff] at h
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h : ∃ j, j ∈ Set.Ico (upperCrossingTime a b f N Nat.zero ω) N ∧ f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N Nat.zero ω < N
⊢ ∃ j, j ∈ Set.Icc 0 N ∧ f j ω ∈ Set.Iic a
case zero.hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h : hitting f (Set.Iic a) (upperCrossingTime a b f N Nat.zero ω) N ω < N
h' : upperCrossingTime a b f N Nat.zero ω < N
⊢ N ≤ N
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h
[GOAL]
case zero.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N Nat.zero ω < N
j : ℕ
hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N Nat.zero ω) N
hj₂ : f j ω ∈ Set.Iic a
⊢ ∃ j, j ∈ Set.Icc 0 N ∧ f j ω ∈ Set.Iic a
case zero.hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
h : hitting f (Set.Iic a) (upperCrossingTime a b f N Nat.zero ω) N ω < N
h' : upperCrossingTime a b f N Nat.zero ω < N
⊢ N ≤ N
[PROOFSTEP]
exacts [⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl]
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
ih :
  lowerCrossingTime a b f N k ω < N →
    upperCrossingTime a b f N k ω < N →
      upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
        lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
⊢ upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω ∧
    lowerCrossingTime a b f M (Nat.succ k) ω = lowerCrossingTime a b f N (Nat.succ k) ω
[PROOFSTEP]
specialize
  ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
    (lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω ∧
    lowerCrossingTime a b f M (Nat.succ k) ω = lowerCrossingTime a b f N (Nat.succ k) ω
[PROOFSTEP]
have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω :=
  by
  rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h'
  simp only [upperCrossingTime_succ_eq]
  obtain ⟨j, hj₁, hj₂⟩ := h'
  rw [eq_comm, ih.2]
  exacts [hitting_eq_hitting_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
[PROOFSTEP]
rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h'
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : ∃ j, j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
case hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ N ≤ N
[PROOFSTEP]
simp only [upperCrossingTime_succ_eq]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : ∃ j, j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω
case hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ N ≤ N
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h'
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f M k ω) M ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω
case hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ N ≤ N
[PROOFSTEP]
rw [eq_comm, ih.2]
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h' : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N k ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) M ω
case hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : hitting f (Set.Ici b) (lowerCrossingTime a b f N k ω) N ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
⊢ N ≤ N
[PROOFSTEP]
exacts [hitting_eq_hitting_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl]
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
⊢ upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω ∧
    lowerCrossingTime a b f M (Nat.succ k) ω = lowerCrossingTime a b f N (Nat.succ k) ω
[PROOFSTEP]
refine' ⟨this, _⟩
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
⊢ lowerCrossingTime a b f M (Nat.succ k) ω = lowerCrossingTime a b f N (Nat.succ k) ω
[PROOFSTEP]
simp only [lowerCrossingTime, eq_comm, this]
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
⊢ hitting f (Set.Iic a) (upperCrossingTime a b f N (Nat.succ k) ω) N ω =
    hitting f (Set.Iic a) (upperCrossingTime a b f N (Nat.succ k) ω) M ω
[PROOFSTEP]
refine' hitting_eq_hitting_of_exists hNM _
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : lowerCrossingTime a b f N (Nat.succ k) ω < N
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
⊢ ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
[PROOFSTEP]
rw [lowerCrossingTime, hitting_lt_iff _ le_rfl] at h
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h✝ : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h : ∃ j, j ∈ Set.Ico (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
⊢ ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h
[GOAL]
case succ.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N n ω < N
h'✝ : upperCrossingTime a b f N n ω < N
k : ℕ
h' : upperCrossingTime a b f N (Nat.succ k) ω < N
ih :
  upperCrossingTime a b f M k ω = upperCrossingTime a b f N k ω ∧
    lowerCrossingTime a b f M k ω = lowerCrossingTime a b f N k ω
this : upperCrossingTime a b f M (Nat.succ k) ω = upperCrossingTime a b f N (Nat.succ k) ω
j : ℕ
hj₁ : j ∈ Set.Ico (upperCrossingTime a b f N (Nat.succ k) ω) N
hj₂ : f j ω ∈ Set.Iic a
⊢ ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
[PROOFSTEP]
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
[PROOFSTEP]
have :=
  (crossing_eq_crossing_of_lowerCrossingTime_lt hNM (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
[PROOFSTEP]
refine' ⟨_, this⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω
[PROOFSTEP]
rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω = hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) M ω
[PROOFSTEP]
refine' hitting_eq_hitting_of_exists hNM _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N ∧ f j ω ∈ Set.Ici b
[PROOFSTEP]
rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : ∃ j, j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N ∧ f j ω ∈ Set.Ici b
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N ∧ f j ω ∈ Set.Ici b
case hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := h
[GOAL]
case intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
j : ℕ
hj₁ : j ∈ Set.Ico (lowerCrossingTime a b f N n ω) N
hj₂ : f j ω ∈ Set.Ici b
⊢ ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N n ω) N ∧ f j ω ∈ Set.Ici b
case hi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : hitting f (Set.Ici b) (lowerCrossingTime a b f N n ω) N ω < N
this : lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
⊢ N ≤ N
[PROOFSTEP]
exacts [⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩, le_rfl]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω
[PROOFSTEP]
cases n
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N Nat.zero ω < N
⊢ upperCrossingTime a b f M Nat.zero ω = upperCrossingTime a b f N Nat.zero ω
[PROOFSTEP]
simp
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
M : ℕ
hNM : N ≤ M
n✝ : ℕ
h : upperCrossingTime a b f N (Nat.succ n✝) ω < N
⊢ upperCrossingTime a b f M (Nat.succ n✝) ω = upperCrossingTime a b f N (Nat.succ n✝) ω
[PROOFSTEP]
exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
⊢ Monotone fun N ω => upcrossingsBefore a b f N ω
[PROOFSTEP]
intro N M hNM ω
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ (fun N ω => upcrossingsBefore a b f N ω) N ω ≤ (fun N ω => upcrossingsBefore a b f N ω) M ω
[PROOFSTEP]
simp only [upcrossingsBefore]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}
[PROOFSTEP]
by_cases hemp : {n : ℕ | upperCrossingTime a b f N n ω < N}.Nonempty
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : Set.Nonempty {n | upperCrossingTime a b f N n ω < N}
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}
[PROOFSTEP]
refine' csSup_le_csSup (upperCrossingTime_lt_bddAbove hab) hemp fun n hn => _
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n✝ m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : Set.Nonempty {n | upperCrossingTime a b f N n ω < N}
n : ℕ
hn : n ∈ {n | upperCrossingTime a b f N n ω < N}
⊢ n ∈ {n | upperCrossingTime a b f M n ω < M}
[PROOFSTEP]
rw [Set.mem_setOf_eq, upperCrossingTime_eq_upperCrossingTime_of_lt hNM hn]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n✝ m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : Set.Nonempty {n | upperCrossingTime a b f N n ω < N}
n : ℕ
hn : n ∈ {n | upperCrossingTime a b f N n ω < N}
⊢ upperCrossingTime a b f N n ω < M
[PROOFSTEP]
exact lt_of_lt_of_le hn hNM
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : ¬Set.Nonempty {n | upperCrossingTime a b f N n ω < N}
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at hemp
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
N M : ℕ
hNM : N ≤ M
ω : Ω
hemp : {n | upperCrossingTime a b f N n ω < N} = ∅
⊢ sSup {n | upperCrossingTime a b f N n ω < N} ≤ sSup {n | upperCrossingTime a b f M n ω < M}
[PROOFSTEP]
simp [hemp, csSup_empty, bot_eq_zero', zero_le']
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω
[PROOFSTEP]
refine' lt_of_lt_of_le (Nat.lt_succ_self _) (le_csSup (upperCrossingTime_lt_bddAbove hab) _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ Nat.succ (upcrossingsBefore a b f N ω) ∈ {n | upperCrossingTime a b f (N₂ + 1) n ω < N₂ + 1}
[PROOFSTEP]
rw [Set.mem_setOf_eq, upperCrossingTime_succ_eq, hitting_lt_iff _ le_rfl]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j, j ∈ Set.Ico (lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) (N₂ + 1) ∧ f j ω ∈ Set.Ici b
[PROOFSTEP]
refine' ⟨N₂, ⟨_, Nat.lt_succ_self _⟩, hN₂'.le⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ lowerCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N₂
[PROOFSTEP]
rw [lowerCrossingTime, hitting_le_iff_of_lt _ (Nat.lt_succ_self _)]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ ∃ j, j ∈ Set.Icc (upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω) N₂ ∧ f j ω ∈ Set.Iic a
[PROOFSTEP]
refine' ⟨N₁, ⟨le_trans _ hN₁, hN₂⟩, hN₁'.le⟩
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
[PROOFSTEP]
by_cases hN : 0 < N
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
[PROOFSTEP]
have : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N :=
  Nat.sSup_mem (upperCrossingTime_lt_nonempty hN) (upperCrossingTime_lt_bddAbove hab)
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
[PROOFSTEP]
rw [upperCrossingTime_eq_upperCrossingTime_of_lt (hN₁.trans (hN₂.trans <| Nat.le_succ _)) this]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : 0 < N
this : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N
⊢ upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω ≤ N
[PROOFSTEP]
exact this.le
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : ¬0 < N
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
[PROOFSTEP]
rw [not_lt, le_zero_iff] at hN
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
⊢ upperCrossingTime a b f (N₂ + 1) (upcrossingsBefore a b f N ω) ω ≤ N
[PROOFSTEP]
rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
N₁ N₂ : ℕ
hN₁ : N ≤ N₁
hN₁' : f N₁ ω < a
hN₂ : N₁ ≤ N₂
hN₂' : b < f N₂ ω
hN : N = 0
⊢ ⊥ ω ≤ 0
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0
[PROOFSTEP]
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)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : upcrossingsBefore a b f N ω < n
⊢ N ≤ upperCrossingTime a b f N n ω
[PROOFSTEP]
rw [upcrossingsBefore] at hn
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ N ≤ upperCrossingTime a b f N n ω
[PROOFSTEP]
rw [← not_lt]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : sSup {n | upperCrossingTime a b f N n ω < N} < n
⊢ ¬upperCrossingTime a b f N n ω < N
[PROOFSTEP]
exact fun h => not_le.2 hn (le_csSup (upperCrossingTime_lt_bddAbove hab) h)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hn : upcrossingsBefore a b f N ω < n
this : N ≤ upperCrossingTime a b f N n ω
⊢ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω = 0
[PROOFSTEP]
simp [stoppedValue, upperCrossingTime_stabilize' (Nat.le_succ n) this,
  lowerCrossingTime_stabilize' le_rfl (le_trans this upperCrossingTime_le_lowerCrossingTime)]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ k in Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
[PROOFSTEP]
classical
by_cases hN : N = 0
· simp [hN]
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]
rw [Finset.sum_comm]
have h₁ :
  ∀ k,
    ∑ n in 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) ω :=
  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
simp_rw [h₁]
have h₂ :
  ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
  by
  calc
    ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
        ∑ k in Finset.range (upcrossingsBefore a b f N ω),
          (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
      by
      refine' Finset.sum_le_sum fun i hi => le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab _
      rwa [Finset.mem_range] at hi
    _ ≤
        ∑ k in Finset.range N,
          (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
      by
      refine'
        Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_subset.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => _
      by_cases hi' : i = upcrossingsBefore a b f N ω
      · subst hi'
        simp only [stoppedValue]
        rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
        by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
        · rw [heq, sub_self]
        · rw [sub_nonneg]
          exact le_trans (stoppedValue_lowerCrossingTime heq) hf
      · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
        rw [Finset.mem_range, not_lt] at hi
        exact lt_of_le_of_ne hi (Ne.symm hi')
refine' le_trans _ h₂
rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ k in Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
[PROOFSTEP]
by_cases hN : N = 0
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ k in Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
[PROOFSTEP]
simp [hN]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ k in Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω
[PROOFSTEP]
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]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x in Finset.range N,
      ∑ x_1 in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N x_1 ω) (upperCrossingTime a b f N (x_1 + 1) ω))
          (fun a => f (a + 1) ω - f a ω) x
[PROOFSTEP]
rw [Finset.sum_comm]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ y in Finset.range N,
      ∑ x in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω))
          (fun a => f (a + 1) ω - f a ω) x
[PROOFSTEP]
have h₁ :
  ∀ k,
    ∑ n in 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) ω :=
  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
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
⊢ ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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) ω
[PROOFSTEP]
intro k
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ ∑ n in Finset.range N,
      Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
        (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) ω
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
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) ω
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
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) ω)
[PROOFSTEP]
ext i
[GOAL]
case a
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
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) ω)
[PROOFSTEP]
simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico, and_iff_right_iff_imp, and_imp]
[GOAL]
case a
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
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
[PROOFSTEP]
exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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) ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ y in Finset.range N,
      ∑ x in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N y ω) (upperCrossingTime a b f N (y + 1) ω))
          (fun a => f (a + 1) ω - f a ω) x
[PROOFSTEP]
simp_rw [h₁]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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) ω
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (x + 1)) ω - stoppedValue f (lowerCrossingTime a b f N x) ω)
[PROOFSTEP]
have h₂ :
  ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
  by
  calc
    ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
        ∑ k in Finset.range (upcrossingsBefore a b f N ω),
          (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
      by
      refine' Finset.sum_le_sum fun i hi => le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab _
      rwa [Finset.mem_range] at hi
    _ ≤
        ∑ k in Finset.range N,
          (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
      by
      refine'
        Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_subset.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => _
      by_cases hi' : i = upcrossingsBefore a b f N ω
      · subst hi'
        simp only [stoppedValue]
        rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
        by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
        · rw [heq, sub_self]
        · rw [sub_nonneg]
          exact le_trans (stoppedValue_lowerCrossingTime heq) hf
      · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
        rw [Finset.mem_range, not_lt] at hi
        exact lt_of_le_of_ne hi (Ne.symm hi')
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)
[PROOFSTEP]
calc
  ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
      ∑ k in Finset.range (upcrossingsBefore a b f N ω),
        (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
    by
    refine' Finset.sum_le_sum fun i hi => le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab _
    rwa [Finset.mem_range] at hi
  _ ≤
      ∑ k in Finset.range N,
        (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
    by
    refine' Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_subset.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => _
    by_cases hi' : i = upcrossingsBefore a b f N ω
    · subst hi'
      simp only [stoppedValue]
      rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
      by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
      · rw [heq, sub_self]
      · rw [sub_nonneg]
        exact le_trans (stoppedValue_lowerCrossingTime heq) hf
    · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
      rw [Finset.mem_range, not_lt] at hi
      exact lt_of_le_of_ne hi (Ne.symm hi')
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k in Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)
[PROOFSTEP]
refine' Finset.sum_le_sum fun i hi => le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω
[PROOFSTEP]
rwa [Finset.mem_range] at hi
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 in 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 in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)
[PROOFSTEP]
refine' Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_subset.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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) ω
[PROOFSTEP]
by_cases hi' : i = upcrossingsBefore a b f N ω
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω)
hi' : i = upcrossingsBefore a b f N ω
⊢ 0 ≤ stoppedValue f (upperCrossingTime a b f N (i + 1)) ω - stoppedValue f (lowerCrossingTime a b f N i) ω
[PROOFSTEP]
subst hi'
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ≤
    stoppedValue f (upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1)) ω -
      stoppedValue f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω)) ω
[PROOFSTEP]
simp only [stoppedValue]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 (upperCrossingTime a b f N (upcrossingsBefore a b f N ω + 1) ω) ω -
      f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) ω
[PROOFSTEP]
rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω) ω) ω
[PROOFSTEP]
by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω) ω) ω
[PROOFSTEP]
rw [heq, sub_self]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω) ω) ω
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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
⊢ f (lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω) ω ≤ f N ω
[PROOFSTEP]
exact le_trans (stoppedValue_lowerCrossingTime heq) hf
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω)
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ 0 ≤ stoppedValue f (upperCrossingTime a b f N (i + 1)) ω - stoppedValue f (lowerCrossingTime a b f N i) ω
[PROOFSTEP]
rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 ω)
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ upcrossingsBefore a b f N ω < i
[PROOFSTEP]
rw [Finset.mem_range, not_lt] at hi
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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 : upcrossingsBefore a b f N ω ≤ i
hi' : ¬i = upcrossingsBefore a b f N ω
⊢ upcrossingsBefore a b f N ω < i
[PROOFSTEP]
exact lt_of_le_of_ne hi (Ne.symm hi')
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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) ω
h₂ :
  ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤
    ∑ x in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (x + 1)) ω - stoppedValue f (lowerCrossingTime a b f N x) ω)
[PROOFSTEP]
refine' le_trans _ h₂
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n in Finset.range N,
        Set.indicator (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω))
          (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) ω
h₂ :
  ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k in Finset.range N,
      (stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω)
⊢ (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ _k in Finset.range (upcrossingsBefore a b f N ω), (b - a)
[PROOFSTEP]
rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_comm]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤
    ∫ (x : Ω), Finset.sum (Finset.range N) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
rw [← integral_mul_left]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ ∫ (a_1 : Ω), (b - a) * ↑(upcrossingsBefore a b f N a_1) ∂μ ≤
    ∫ (x : Ω), Finset.sum (Finset.range N) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
[PROOFSTEP]
refine' integral_mono_of_nonneg _ ((hf.sum_upcrossingStrat_mul a b N).integrable N) _
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ 0 ≤ᵐ[μ] fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)
[PROOFSTEP]
exact eventually_of_forall fun ω => mul_nonneg (sub_nonneg.2 hab.le) (Nat.cast_nonneg _)
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
⊢ (fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)) ≤ᵐ[μ] fun x =>
    Finset.sum (Finset.range N) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x
[PROOFSTEP]
refine' eventually_of_forall fun ω => _
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hfN : ∀ (ω : Ω), a ≤ f N ω
hfzero : 0 ≤ f 0
hab : a < b
ω : Ω
⊢ (fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)) ω ≤
    (fun x => Finset.sum (Finset.range N) (fun k => upcrossingStrat a b f N k * (f (k + 1) - f k)) x) ω
[PROOFSTEP]
simpa using mul_upcrossingsBefore_le (hfN ω) hab
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
[PROOFSTEP]
have hab' : 0 < b - a := sub_pos.2 hab
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
[PROOFSTEP]
have hf : ∀ ω i, b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω := by
  intro i ω
  refine' ⟨fun h => _, fun h => _⟩
  · rwa [← sub_le_sub_iff_right a, ← LatticeOrderedGroup.pos_eq_self_of_pos_pos (lt_of_lt_of_le hab' h)]
  · rw [← sub_le_sub_iff_right a] at h
    rwa [LatticeOrderedGroup.pos_of_nonneg _ (le_trans hab'.le h)]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
⊢ ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
[PROOFSTEP]
intro i ω
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
⊢ b ≤ f ω i
[PROOFSTEP]
rwa [← sub_le_sub_iff_right a, ← LatticeOrderedGroup.pos_eq_self_of_pos_pos (lt_of_lt_of_le hab' h)]
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b ≤ f ω i
⊢ b - a ≤ (f ω i - a)⁺
[PROOFSTEP]
rw [← sub_le_sub_iff_right a] at h
[GOAL]
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ f ω i - a
⊢ b - a ≤ (f ω i - a)⁺
[PROOFSTEP]
rwa [LatticeOrderedGroup.pos_of_nonneg _ (le_trans hab'.le h)]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
[PROOFSTEP]
have hf' : ∀ ω i, (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by
  intro ω i
  rw [LatticeOrderedGroup.pos_nonpos_iff, sub_nonpos]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
⊢ ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
[PROOFSTEP]
intro ω i
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
ω : Ω
i : ℕ
⊢ (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
[PROOFSTEP]
rw [LatticeOrderedGroup.pos_nonpos_iff, sub_nonpos]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n
[PROOFSTEP]
induction' n with k ih
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N Nat.zero = upperCrossingTime a b f N Nat.zero ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N Nat.zero = lowerCrossingTime a b f N Nat.zero
[PROOFSTEP]
refine' ⟨rfl, _⟩
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
⊢ lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N Nat.zero = lowerCrossingTime a b f N Nat.zero
[PROOFSTEP]
simp only [lowerCrossingTime_zero, hitting, Set.mem_Icc, Set.mem_Iic, Nat.zero_eq]
[GOAL]
case zero
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
⊢ (fun x =>
      if ∃ j, j ∈ Set.Icc ⊥ N ∧ (f j x - a)⁺ ∈ Set.Iic 0 then sInf (Set.Icc ⊥ N ∩ {i | (f i x - a)⁺ ≤ 0}) else N) =
    fun x => if ∃ j, j ∈ Set.Icc ⊥ N ∧ f j x ∈ Set.Iic a then sInf (Set.Icc ⊥ N ∩ {i | f i x ≤ a}) else N
[PROOFSTEP]
ext ω
[GOAL]
case zero.h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
⊢ (if ∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ∈ Set.Iic 0 then sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) else N) =
    if ∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ∈ Set.Iic a then sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a}) else N
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
h₁ : ∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})
[PROOFSTEP]
simp_rw [hf']
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
h₁ : ∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N
[PROOFSTEP]
simp_rw [Set.mem_Iic, ← hf' _ _] at h₂
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
h₁ : ∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ≤ 0
⊢ sInf (Set.Icc ⊥ N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N
[PROOFSTEP]
exact False.elim (h₂ h₁)
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
h₁ : ¬∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})
[PROOFSTEP]
simp_rw [Set.mem_Iic, hf' _ _] at h₁
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
h₂ : ∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ∈ Set.Iic a
h₁ : ¬∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ≤ a
⊢ N = sInf (Set.Icc ⊥ N ∩ {i | f i ω ≤ a})
[PROOFSTEP]
exact False.elim (h₁ h₂)
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
ω : Ω
h₁ : ¬∃ j, j ∈ Set.Icc ⊥ N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j, j ∈ Set.Icc ⊥ N ∧ f j ω ∈ Set.Iic a
⊢ N = N
[PROOFSTEP]
rfl
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) = upperCrossingTime a b f N (Nat.succ k) ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) = lowerCrossingTime a b f N (Nat.succ k)
[PROOFSTEP]
have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1) :=
  by
  ext ω
  simp only [upperCrossingTime_succ_eq, ← ih.2, hitting, Set.mem_Ici, tsub_le_iff_right]
  split_ifs with h₁ h₂ h₂
  · simp_rw [← sub_le_iff_le_add, hf ω]
  · refine' False.elim (h₂ _)
    simp_all only [Set.mem_Ici]
  · refine' False.elim (h₁ _)
    simp_all only [Set.mem_Ici]
  · rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
[PROOFSTEP]
ext ω
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) ω = upperCrossingTime a b f N (k + 1) ω
[PROOFSTEP]
simp only [upperCrossingTime_succ_eq, ← ih.2, hitting, Set.mem_Ici, tsub_le_iff_right]
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
⊢ (if
        ∃ j,
          j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧
            (f j ω - a)⁺ ∈ Set.Ici (b - a) then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a})
    else N) =
    if ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b then
      sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})
    else N
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) =
    sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})
[PROOFSTEP]
simp_rw [← sub_le_iff_le_add, hf ω]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
⊢ sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ (f i ω - a)⁺ + a}) = N
[PROOFSTEP]
refine' False.elim (h₂ _)
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
⊢ ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
[PROOFSTEP]
simp_all only [Set.mem_Ici]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
⊢ N = sInf (Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∩ {i | b ≤ f i ω})
[PROOFSTEP]
refine' False.elim (h₁ _)
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
⊢ ∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
[PROOFSTEP]
simp_all only [Set.mem_Ici]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
ω : Ω
h₁ : ¬∃ j, j ∈ Set.Icc (lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k ω) N ∧ (f j ω - a)⁺ ∈ Set.Ici (b - a)
h₂ : ¬∃ j, j ∈ Set.Icc (lowerCrossingTime a b f N k ω) N ∧ f j ω ∈ Set.Ici b
⊢ N = N
[PROOFSTEP]
rfl
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
⊢ upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) = upperCrossingTime a b f N (Nat.succ k) ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) = lowerCrossingTime a b f N (Nat.succ k)
[PROOFSTEP]
refine' ⟨this, _⟩
[GOAL]
case succ
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
⊢ lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) = lowerCrossingTime a b f N (Nat.succ k)
[PROOFSTEP]
ext ω
[GOAL]
case succ.h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
⊢ lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω = lowerCrossingTime a b f N (Nat.succ k) ω
[PROOFSTEP]
simp only [lowerCrossingTime, this, hitting, Set.mem_Iic]
[GOAL]
case succ.h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
⊢ (if
        ∃ j,
          j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧
            (f j ω - a)⁺ ∈ Set.Iic 0 then
      sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0})
    else N) =
    if ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a then
      sInf (Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∩ {i | f i ω ≤ a})
    else N
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ∃ j, j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) =
    sInf (Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∩ {i | f i ω ≤ a})
[PROOFSTEP]
simp_rw [hf' ω]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ∃ j, j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
⊢ sInf (Set.Icc (upperCrossingTime a b f N (k + 1) ω) N ∩ {i | (f i ω - a)⁺ ≤ 0}) = N
[PROOFSTEP]
refine' False.elim (h₂ _)
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ∃ j, j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
⊢ ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
[PROOFSTEP]
simp_all only [Set.mem_Iic]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j,
      j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
⊢ N = sInf (Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∩ {i | f i ω ≤ a})
[PROOFSTEP]
refine' False.elim (h₁ _)
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j,
      j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
⊢ ∃ j, j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
[PROOFSTEP]
simp_all only [Set.mem_Iic]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hab : a < b
hab' : 0 < b - a
hf : ∀ (ω : Ω) (i : ℕ), b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω
hf' : ∀ (ω : Ω) (i : ℕ), (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a
k : ℕ
ih :
  upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = upperCrossingTime a b f N k ∧
    lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N k = lowerCrossingTime a b f N k
this : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1)
ω : Ω
h₁ :
  ¬∃ j,
      j ∈ Set.Icc (upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (Nat.succ k) ω) N ∧ (f j ω - a)⁺ ∈ Set.Iic 0
h₂ : ¬∃ j, j ∈ Set.Icc (upperCrossingTime a b f N (Nat.succ k) ω) N ∧ f j ω ∈ Set.Iic a
⊢ N = N
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
⊢ upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω
[PROOFSTEP]
simp_rw [upcrossingsBefore, (crossing_pos_eq hab).1]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
[PROOFSTEP]
refine'
  le_trans (le_of_eq _)
    (integral_mul_upcrossingsBefore_le_integral (hf.sub_martingale (martingale_const _ _ _)).pos
      (fun ω => LatticeOrderedGroup.pos_nonneg _) (fun ω => LatticeOrderedGroup.pos_nonneg _) (sub_pos.2 hab))
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ =
    (b - a - 0) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ
[PROOFSTEP]
simp_rw [sub_zero, ← upcrossingsBefore_pos_eq hab]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N x) ∂μ =
    (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
[PROOFSTEP]
by_cases hab : a < b
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
[PROOFSTEP]
exact mul_integral_upcrossingsBefore_le_integral_pos_part_aux hf hab
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : ¬a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
[PROOFSTEP]
rw [not_lt, ← sub_nonpos] at hab
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab✝ : b ≤ a
hab : b - a ≤ 0
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
[PROOFSTEP]
exact
  le_trans (mul_nonpos_of_nonpos_of_nonneg hab (integral_nonneg fun ω => Nat.cast_nonneg _))
    (integral_nonneg fun ω => LatticeOrderedGroup.pos_nonneg _)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
⊢ upcrossingsBefore a b f N ω = ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
by_cases hN : N = 0
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : N = 0
⊢ upcrossingsBefore a b f N ω = ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
simp [hN]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω = ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
rw [← Finset.sum_Ico_consecutive _ (Nat.succ_le_succ zero_le') (Nat.succ_le_succ (upcrossingsBefore_le f ω hab))]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω =
    ∑ i in Finset.Ico (Nat.succ 0) (Nat.succ (upcrossingsBefore a b f N ω)),
        Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i +
      ∑ i in Finset.Ico (Nat.succ (upcrossingsBefore a b f N ω)) (Nat.succ N),
        Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
have h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1 :=
  by
  rintro k hk
  rw [Finset.mem_Ico] at hk
  rw [Set.indicator_of_mem]
  · rfl
  · exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab (Nat.lt_succ_iff.1 hk.2)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
⊢ ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
[PROOFSTEP]
rintro k hk
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
k : ℕ
hk : k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)
⊢ Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
[PROOFSTEP]
rw [Finset.mem_Ico] at hk
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
[PROOFSTEP]
rw [Set.indicator_of_mem]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ OfNat.ofNat 1 k = 1
[PROOFSTEP]
rfl
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ k ∈ {n | upperCrossingTime a b f N n ω < N}
[PROOFSTEP]
exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab (Nat.lt_succ_iff.1 hk.2)
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
⊢ upcrossingsBefore a b f N ω =
    ∑ i in Finset.Ico (Nat.succ 0) (Nat.succ (upcrossingsBefore a b f N ω)),
        Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i +
      ∑ i in Finset.Ico (Nat.succ (upcrossingsBefore a b f N ω)) (Nat.succ N),
        Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
have h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0 :=
  by
  rintro k hk
  rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
  rw [Set.indicator_of_not_mem]
  simp only [Set.mem_setOf_eq, not_lt]
  exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
⊢ ∀ (k : ℕ),
    k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1) →
      Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 0
[PROOFSTEP]
rintro k hk
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
k : ℕ
hk : k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)
⊢ Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 0
[PROOFSTEP]
rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 0
[PROOFSTEP]
rw [Set.indicator_of_not_mem]
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ ¬k ∈ {n | upperCrossingTime a b f N n ω < N}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, not_lt]
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ N ≤ upperCrossingTime a b f N k ω
[PROOFSTEP]
exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1) → Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 1
h₂ :
  ∀ (k : ℕ),
    k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1) →
      Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 k = 0
⊢ upcrossingsBefore a b f N ω =
    ∑ i in Finset.Ico (Nat.succ 0) (Nat.succ (upcrossingsBefore a b f N ω)),
        Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i +
      ∑ i in Finset.Ico (Nat.succ (upcrossingsBefore a b f N ω)) (Nat.succ N),
        Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
⊢ Measurable (upcrossingsBefore a b f N)
[PROOFSTEP]
have :
  upcrossingsBefore a b f N = fun ω =>
    ∑ i in Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i :=
  by
  ext ω
  exact upcrossingsBefore_eq_sum hab
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
⊢ upcrossingsBefore a b f N = fun ω =>
    ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
ext ω
[GOAL]
case h
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω = ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
exact upcrossingsBefore_eq_sum hab
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω =>
    ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
⊢ Measurable (upcrossingsBefore a b f N)
[PROOFSTEP]
rw [this]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω =>
    ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
⊢ Measurable fun ω => ∑ i in Finset.Ico 1 (N + 1), Set.indicator {n | upperCrossingTime a b f N n ω < N} 1 i
[PROOFSTEP]
exact
  Finset.measurable_sum _ fun i _ =>
    Measurable.indicator measurable_const <| ℱ.le N _ (hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N)
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖↑(upcrossingsBefore a b f N ω)‖ ≤ ↑N
[PROOFSTEP]
refine' eventually_of_forall fun ω => _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ ‖↑(upcrossingsBefore a b f N ω)‖ ≤ ↑N
[PROOFSTEP]
rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω✝ : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω ≤ N
[PROOFSTEP]
refine' upcrossingsBefore_le _ _ hab
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ upcrossings a b f ω < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
[PROOFSTEP]
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
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ upcrossings a b f ω < ⊤ → ∃ k, upcrossings a b f ω ≤ ↑k
[PROOFSTEP]
intro h
[GOAL]
case mp
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
h : upcrossings a b f ω < ⊤
⊢ ∃ k, upcrossings a b f ω ≤ ↑k
[PROOFSTEP]
lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
[GOAL]
case mp.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
r : ℝ≥0
hr : ↑r = upcrossings a b f ω
upcrossings_lt_top_iff✝ upcrossings_lt_top_iff : ↑r < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
h✝ h : ↑r < ⊤
⊢ ∃ k, ↑r ≤ ↑k
[PROOFSTEP]
exact ⟨r, le_rfl⟩
[GOAL]
case mpr
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
⊢ (∃ k, upcrossings a b f ω ≤ ↑k) → upcrossings a b f ω < ⊤
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mpr.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
k : ℝ≥0
hk : upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ⊤
[PROOFSTEP]
exact lt_of_le_of_lt hk ENNReal.coe_lt_top
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
[PROOFSTEP]
simp_rw [this, upcrossings, iSup_le_iff]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) → ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mpr
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ (∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k) → ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mp.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_nat_ge k
[GOAL]
case mp.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m✝ : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
[PROOFSTEP]
refine' ⟨m, fun N => Nat.cast_le.1 ((hk N).trans _)⟩
[GOAL]
case mp.intro.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m✝ : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
N : ℕ
⊢ ↑k ≤ ↑m
[PROOFSTEP]
rwa [← ENNReal.coe_nat, ENNReal.coe_le_coe]
[GOAL]
case mpr.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
⊢ ∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
[PROOFSTEP]
refine' ⟨k, fun N => _⟩
[GOAL]
case mpr.intro
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℕ
hk : ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
N : ℕ
⊢ ↑(upcrossingsBefore a b f N ω) ≤ ↑↑k
[PROOFSTEP]
simp only [ENNReal.coe_nat, Nat.cast_le, hk N]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
by_cases hab : a < b
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
simp_rw [upcrossings]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), ⨆ (N : ℕ), ↑(upcrossingsBefore a b f N ω) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
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 ω => LatticeOrderedGroup.pos_nonneg _
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
⊢ ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
[PROOFSTEP]
intro N
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
[PROOFSTEP]
rw [ofReal_integral_eq_lintegral_ofReal]
[GOAL]
case hfi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ Integrable fun ω => (f N ω - a)⁺
[PROOFSTEP]
exact (hf.sub_martingale (martingale_const _ _ _)).pos.integrable _
[GOAL]
case f_nn
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
N : ℕ
⊢ 0 ≤ᵐ[μ] fun ω => (f N ω - a)⁺
[PROOFSTEP]
exact eventually_of_forall fun ω => LatticeOrderedGroup.pos_nonneg _
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : 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 ω) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
rw [lintegral_iSup']
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : 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) ∂μ ≤
    ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ (i : ℕ),
    ENNReal.ofReal (b - a) * ∫⁻ (a_1 : Ω), ↑(upcrossingsBefore a b f i a_1) ∂μ ≤
      ⨆ (N : ℕ), ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
[PROOFSTEP]
intro N
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : 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)⁺ ∂μ)
[PROOFSTEP]
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]
[GOAL]
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : 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 ω) ∂μ = ∫⁻ (ω : Ω), ↑↑(upcrossingsBefore a b f N ω) ∂μ
[PROOFSTEP]
simp
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : 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)⁺ ∂μ)
[PROOFSTEP]
simp_rw [NNReal.coe_nat_cast]
[GOAL]
case pos
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : 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)⁺ ∂μ)
[PROOFSTEP]
exact
  (ENNReal.ofReal_le_ofReal (hf.mul_integral_upcrossingsBefore_le_integral_pos_part a b N)).trans
    (le_iSup (α := ℝ≥0∞) _ N)
[GOAL]
case pos.hfi
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω : Ω
ℱ : 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 : ℕ
⊢ Integrable fun x => ↑↑(upcrossingsBefore a b f N x)
[PROOFSTEP]
simp only [NNReal.coe_nat_cast, hf.adapted.integrable_upcrossingsBefore hab]
[GOAL]
case pos.hf
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : 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 : ℕ), AEMeasurable fun ω => ↑(upcrossingsBefore a b f n ω)
[PROOFSTEP]
exact fun n => measurable_from_top.comp_aemeasurable (hf.adapted.measurable_upcrossingsBefore hab).aemeasurable
[GOAL]
case pos.h_mono
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
⊢ ∀ᵐ (x : Ω) ∂μ, Monotone fun n => ↑(upcrossingsBefore a b f n x)
[PROOFSTEP]
refine' eventually_of_forall fun ω N M hNM => _
[GOAL]
case pos.h_mono
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : 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 M : ℕ
hNM : N ≤ M
⊢ (fun n => ↑(upcrossingsBefore a b f n ω)) N ≤ (fun n => ↑(upcrossingsBefore a b f n ω)) M
[PROOFSTEP]
rw [Nat.cast_le]
[GOAL]
case pos.h_mono
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N✝ n m : ℕ
ω✝ : Ω
ℱ : 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 M : ℕ
hNM : N ≤ M
⊢ upcrossingsBefore a b f N ω ≤ upcrossingsBefore a b f M ω
[PROOFSTEP]
exact upcrossingsBefore_mono hab hNM ω
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : ¬a < b
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
rw [not_lt, ← sub_nonpos] at hab
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab✝ : b ≤ a
hab : b - a ≤ 0
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
rw [ENNReal.ofReal_of_nonpos hab, zero_mul]
[GOAL]
case neg
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
a✝ b✝ : ℝ
f : ℕ → Ω → ℝ
N n m : ℕ
ω : Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab✝ : b ≤ a
hab : b - a ≤ 0
⊢ 0 ≤ ⨆ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
[PROOFSTEP]
exact zero_le _