le_sub_of_le_upcrossingsBefore — Mathlib

English

Under suitable regularity, b − a ≤ stoppedValue f (upperCrossingTime N(n+1)) − stoppedValue f (lowerCrossingTime n).

Русский

Справедливость: b−a меньше или равно разности остановленного значения между верхним временем пересечения и нижним временем пересечения.

LaTeX

$$$b - a \\le \\StoppedValue(f, \\mathrm{upperCrossingTime}(a,b,f,N,n+1)) - \\StoppedValue(f, \\mathrm{lowerCrossingTime}(a,b,f,N,n)).$$$

Lean4

theorem le_sub_of_le_upcrossingsBefore (hN : 0 < N) (hab : a < b) (hn : n < upcrossingsBefore a b f N ω) :
    b - a ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω - stoppedValue f (lowerCrossingTime a b f N n) ω :=
  sub_le_sub (stoppedValue_upperCrossingTime (upperCrossingTime_lt_of_le_upcrossingsBefore hN hab hn).ne)
    (stoppedValue_lowerCrossingTime (lowerCrossingTime_lt_of_lt_upcrossingsBefore hN hab hn).ne)

Похожие утверждения