adapted_zero

Mathlib.Probability.Process.Adapted

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

English

Let f be a filtration on Ω with β a type having a zero element. Then the process i ↦ 0 is Adapted to f.

Русский

Пусть f — фильтрация на Ω, β — вид множества с нулём. Тогда процесс i ↦ 0 адаптирован к f.

LaTeX

$$$\\mathrm{Adapted}(f, 0)$$$

Lean4

theorem adapted_zero [Zero β] (f : Filtration ι m) : Adapted f (0 : ι → Ω → β) := fun i =>
  @stronglyMeasurable_zero Ω β (f i) _ _

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

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

Разделы

Аффилиация

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