leastGE_le

Mathlib.Probability.Martingale.BorelCantelli

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

English

For any π and r, when π ω ≤ n, the value leastGE f r (π ω) ω equals min(π ω, leastGE f r n ω).

Русский

Для любого π и r, если π ω ≤ n, то leastGE f r (π ω) ω равно min(π ω, leastGE f r n ω).

LaTeX

$$Eq (leastGE f r (π ω) ω) (min (π ω) (leastGE f r n ω)).$$

Lean4

theorem leastGE_le {i : ℕ} {r : ℝ} (ω : Ω) : leastGE f r i ω ≤ i :=
  hitting_le ω

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

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

Разделы

Аффилиация

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