isMarkovKernel_deterministic

Mathlib.Probability.Kernel.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.isMarkovKernel_deterministic

← MathLib Explorer

English

Deterministic kernel is Markov: it satisfies the Markov property.

Русский

Детерминированное ядро удовлетворяет условию Маркова.

LaTeX

$$IsMarkovKernel (deterministic f hf)$$

Lean4

instance isMarkovKernel_deterministic {f : α → β} (hf : Measurable f) : IsMarkovKernel (deterministic f hf) :=
  ⟨fun a => by rw [deterministic_apply hf]; infer_instance⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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