English
Let f be NullMeasurable with respect to μ|s and equal to a constant b almost everywhere on sᶜ. Then for every measurable t with b ∉ t, μ(f⁻¹ t) = μ|s(f⁻¹ t).
Русский
Пусть f измеримо нулевым образом относительно μ|s и а.е. на sᶜ тождественно равно константе b. Тогда для любого измеримого t с отсутствием b в t выполняется μ(f⁻¹ t) = μ|s(f⁻¹ t).
LaTeX
$$$\\text{NullMeasurable}(f, \\mu \\restriction s) \\wedge (f =_{\\mathrm{ae}}^{\\mu \\restriction s^{c}} b) \\Rightarrow \\forall t,\\ MeasurableSet\\ t \\Rightarrow b \\notin t \\Rightarrow μ(f^{-1} t) = μ\\restriction s (f^{-1} t)$$$
Lean4
theorem measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const {β : Type*} [MeasurableSpace β] {b : β}
{f : α → β} {s : Set α} (f_mble : NullMeasurable f (μ.restrict s)) (hs : f =ᵐ[Measure.restrict μ sᶜ] (fun _ ↦ b))
{t : Set β} (t_mble : MeasurableSet t) (ht : b ∉ t) : μ (f ⁻¹' t) = μ.restrict s (f ⁻¹' t) :=
by
rw [Measure.restrict_apply₀ (f_mble t_mble)]
rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs
· apply le_antisymm _ (measure_mono inter_subset_left)
apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans
apply (measure_union_le _ _).trans
have obs : μ ((f ⁻¹' t) ∩ sᶜ) = 0 := by
apply le_antisymm _ (zero_le _)
rw [← hs]
apply measure_mono (inter_subset_inter_left _ _)
intro x hx hfx
simp only [mem_preimage] at hx hfx
exact ht (hfx ▸ hx)
simp only [obs, add_zero, le_refl]
· exact NullMeasurableSet.of_null hs
