English
For a ≤ f(N) and a < b, the product (b − a) · upcrossingsBefore a b f N ω is bounded by the sum ∑_{k=0}^{N−1} upcrossingStrat a b f N k ω · (f(k+1) − f(k)) ω.
Русский
При a ≤ f(N) и a < b, произведение (b−a) на число восходящих до момента N ограничено суммой по k от 0 до N−1.
LaTeX
$$$(b - a) \\cdot UpcrossingsBefore(a,b,f,N,\\omega) \\le \\sum_{k=0}^{N-1} UpcrossingStrat(a,b,f,N,k,\\omega)\\,(f(k+1,\\omega) - f(k,\\omega)).$$$
Lean4
theorem mul_upcrossingsBefore_le (hf : a ≤ f N ω) (hab : a < b) :
(b - a) * upcrossingsBefore a b f N ω ≤ ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω :=
by
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 ∈ 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 ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
∑ k ∈ Finset.range N,
(stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
by
calc
∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
(stoppedValue f (upperCrossingTime a b f N (k + 1)) ω - stoppedValue f (lowerCrossingTime a b f N k) ω) :=
by
gcongr ∑ k ∈ _, ?_ with i hi
refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_
rwa [Finset.mem_range] at hi
_ ≤
∑ k ∈ 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_range.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]
