eq_of_absolutelyContinuous_measure_univ_eq

English

Given ergodicity and absolute continuity, equality of univ measures implies equality of measures themselves.

Русский

При эргодичности и абсолютной непрерывности равенство мер на все множество означает равенство самих мер.

LaTeX

$$$\mathrm{Ergodic}(f,\mu) \land \mathrm{MeasurePreserving}(f,\nu,\nu) \land \nu \ll \mu \land \nu(\mathrm{univ}) = \mu(\mathrm{univ}) \Rightarrow \nu = \mu$$$

Lean4

theorem eq_of_absolutelyContinuous_measure_univ_eq [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμ : Ergodic f μ)
    (hfν : MeasurePreserving f ν ν) (hνμ : ν ≪ μ) (huniv : ν univ = μ univ) : ν = μ :=
  by
  rcases hμ.eq_smul_of_absolutelyContinuous hfν hνμ with ⟨c, rfl⟩
  rcases eq_or_ne μ 0 with rfl | hμ₀
  · simp
  · simp_all [ENNReal.mul_eq_right]

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