upcrossingsBefore_zero

Mathlib.Probability.Martingale.Upcrossing

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

English

For every a,b,f, and ω, upcrossingsBefore a b f 0 ω = 0.

Русский

Для любых a,b,f и ω выполняется upcrossingsBefore a b f 0 ω = 0.

LaTeX

$$$\\mathrm{upcrossingsBefore}(a,b,f,0,\\omega)=0.$$$

Lean4

theorem upcrossingsBefore_zero : upcrossingsBefore a b f 0 ω = 0 := by simp [upcrossingsBefore]

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

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

Разделы

Аффилиация

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