English
The singular part of a finite invariant measure with respect to a σ-finite invariant measure is invariant under the same self-map.
Русский
Составная часть сингулярной части конечной инвариантной меры по отношению к сигма-фи-контролируемой инвариантной мере остаётся инвариантной при той же карте.
LaTeX
$$$\text{MeasurePreserving } f \; μ \; μ \rightarrow \text{MeasurePreserving } f \; (μ.singularPart ν) (μ.singularPart ν)$$$
Lean4
/-- The singular part of a finite invariant measure of a self-map
with respect to a σ-finite invariant measure is an invariant measure. -/
protected theorem singularPart [SigmaFinite ν] {f : X → X} (hfμ : MeasurePreserving f μ μ)
(hfν : MeasurePreserving f ν ν) : MeasurePreserving f (μ.singularPart ν) (μ.singularPart ν) :=
by
rcases (μ.mutuallySingular_singularPart ν).symm with ⟨s, hsm, hνs, hμs⟩
convert hfμ.restrict_preimage hsm using 1
· refine singularPart_eq_restrict ?_ (hfν.preimage_null hνs)
rw [← mem_ae_iff, ← Filter.eventuallyEq_univ, ae_eq_univ_iff_measure_eq (hfμ.measurable hsm).nullMeasurableSet]
calc
μ.singularPart ν (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) :=
by
rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs
rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
_ = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s := by
rw [rnDeriv_add_singularPart, hfμ.measure_preimage hsm.nullMeasurableSet]
_ = μ.singularPart ν s := by rw [add_apply, withDensity_absolutelyContinuous _ _ hνs, zero_add]
_ = μ.singularPart ν univ := by rw [← measure_add_measure_compl hsm, hμs, add_zero]
· exact singularPart_eq_restrict hμs hνs
