English
If upperCrossingTime a b f N n ω < N then lower/upper crossing times satisfy certain equalities (two-way comparison with lower).
Русский
Если верхнее время пересечения меньше времени N, вместе с верхними и нижними временами выполняются равенства.
LaTeX
$$$\\text{crossing\_eq\_crossing\_of\_lowerCrossingTime\_lt} \\; (hNM) (h) : \\cdots$$$
Lean4
/-- **Doob's upcrossing estimate**: given a real-valued discrete submartingale `f` and real
values `a` and `b`, we have `(b - a) * 𝔼[upcrossingsBefore a b f N] ≤ 𝔼[(f N - a)⁺]` where
`upcrossingsBefore a b f N` is the number of times the process `f` crossed from below `a` to above
`b` before the time `N`. -/
theorem mul_integral_upcrossingsBefore_le_integral_pos_part [IsFiniteMeasure μ] (a b : ℝ) (hf : Submartingale f ℱ μ)
(N : ℕ) : (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[fun ω => (f N ω - a)⁺] :=
by
by_cases hab : a < b
· exact mul_integral_upcrossingsBefore_le_integral_pos_part_aux hf hab
· rw [not_lt, ← sub_nonpos] at hab
exact le_trans (mul_nonpos_of_nonpos_of_nonneg hab (by positivity)) (integral_nonneg fun ω => posPart_nonneg _)
