quasiErgodic

Mathlib.Dynamics.Ergodic.Ergodic

URI: https://scilib.ai/kg/mathlib#Ergodic.quasiErgodic

← MathLib Explorer

English

An ergodic map is automatically quasi-ergodic.

Русский

Эргодический отображение автоматически является квазирегодичным.

LaTeX

$$$\mathrm{Ergodic}(f, \mu) \Rightarrow \mathrm{QuasiErgodic}(f, \mu)$$$

Lean4

/-- An ergodic map is quasi-ergodic. -/
theorem quasiErgodic (hf : Ergodic f μ) : QuasiErgodic f μ :=
  { hf.toPreErgodic, hf.toMeasurePreserving.quasiMeasurePreserving with }

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

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

Разделы

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

Аффилиация

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