of_absolutelyContinuous — Mathlib

English

If f is Conservative with respect to μ, ν ≪ μ, and f is QuasiMeasurePreserving from ν to ν, then f is Conservative with respect to ν.

Русский

Если f консервативно относительно μ, ν ≪ μ, и f пересобирается в ν к ν через квази-измеряемое сохранение, то f консервативно относительно ν.

LaTeX

$$$\forall {f,\mu,\nu},\ [\mathrm{Conservative}(f,\mu)]\wedge (\nu \ll \mu)\wedge (\mathrm{QuasiMeasurePreserving}(f,\nu,\nu)) \Rightarrow \mathrm{Conservative}(f,\nu).$$$

Lean4

theorem of_absolutelyContinuous {ν : Measure α} (h : Conservative f μ) (hν : ν ≪ μ)
    (h' : QuasiMeasurePreserving f ν ν) : Conservative f ν :=
  ⟨h', fun _ hsm h0 ↦ h.exists_mem_iterate_mem' hsm (mt (@hν _) h0)⟩

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