upcrossingsBefore_zero'

Mathlib.Probability.Martingale.Upcrossing

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

English

For every a,b,f and N, the function upcrossingsBefore a b f N is identically zero at N=0, i.e., upcrossingsBefore a b f 0 = 0 as a function of ω.

Русский

Для любого a,b,f и N функция upcrossingsBefore(a,b,f,N) нулевая при N=0 как функция от ω.

LaTeX

$$$upcrossingsBefore(a,b,f,0)=0$$$

Lean4

@[simp]
theorem upcrossingsBefore_zero' : upcrossingsBefore a b f 0 = 0 := by ext ω; exact upcrossingsBefore_zero

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

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

Разделы

Аффилиация

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