lowerCrossingTime_le

Mathlib.Probability.Martingale.Upcrossing

URI: https://scilib.ai/kg/mathlib#MeasureTheory.lowerCrossingTime_le

English

The lower crossing time is always bounded by the terminal time N, i.e., it never exceeds N.

Русский

Нижнее время пересечения никогда не превышает фиксированное время N.

LaTeX

$$$ lowerCrossingTime(a,b,f,N,n) \\le N $$$

Lean4

theorem lowerCrossingTime_le : lowerCrossingTime a b f N n ω ≤ N := by simp only [lowerCrossingTime, hitting_le ω]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru