upcrossingStrat_nonneg

Mathlib.Probability.Martingale.Upcrossing

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

English

The upcrossingStrat(a,b,f,N,n,ω) is always between 0 and 1, in particular nonnegative.

Русский

Стратегия upcrossingStrat принимает значения в диапазоне [0,1], в частности неотрицательна.

LaTeX

$$$0 \le upcrossingStrat(a,b,f,N,n,\omega)$$$

Lean4

theorem upcrossingStrat_nonneg : 0 ≤ upcrossingStrat a b f N n ω :=
  Finset.sum_nonneg fun _ _ => Set.indicator_nonneg (fun _ _ => zero_le_one) _

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

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

Разделы

Аффилиация

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