English
Let μ and ν be measures with countable index set ι and sets s_i; if ⋃ i s_i = univ, then μ = ν iff μ|_{s_i} = ν|_{s_i} for all i.
Русский
Пусть μ и ν — меры, индексующее множество счетно, множества s_i; если ⋃ i s_i = univ, то μ = ν тогда и только тогда, когда μ|_{s_i} = ν|_{s_i} для всех i.
LaTeX
$$$[Countable\, ι] (⋃ i, s i = \mathrm{univ}) \Rightarrow (μ = ν \iff ∀ i, μ.restrict (s i) = ν.restrict (s i))$$$
Lean4
/-- If a quasi-measure-preserving map `f` maps a set `s` to a set `t`,
then it is quasi-measure-preserving with respect to the restrictions of the measures. -/
theorem restrict {ν : Measure β} {f : α → β} (hf : QuasiMeasurePreserving f μ ν) {t : Set β} (hmaps : MapsTo f s t) :
QuasiMeasurePreserving f (μ.restrict s) (ν.restrict t)
where
measurable := hf.measurable
absolutelyContinuous := by
refine AbsolutelyContinuous.mk fun u hum ↦ ?_
suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]
refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)
rw [preimage_inter]
gcongr
assumption
