English
If the codomain σ-algebra is countably generated, then every null-measurable function is almost everywhere measurable.
Русский
Если σ-алгебра кодомона достижимого объёма счетно порождена, то любая нулево измеримая функция является а.е.-измеримой.
LaTeX
$$$\mathrm{NullMeasurable}(f, μ) \Rightarrow \mathrm{AEMeasurable}(f, μ)$ under the assumption that the codomain is countably generated.$$
Lean4
/-- If the `σ`-algebra of the codomain of a null measurable function is countably generated,
then the function is a.e.-measurable. -/
theorem aemeasurable {f : α → β} [hc : MeasurableSpace.CountablyGenerated β] (h : NullMeasurable f μ) :
AEMeasurable f μ := by
classical
nontriviality β; inhabit β
rcases hc.1 with ⟨S, hSc, rfl⟩
choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq
choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq
set v := ⋃ s ∈ S, U s \ T s
have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
have hvμ : μ v = 0 :=
(measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <| ((hUeq s hs).trans (hTeq s hs).symm).le
refine
⟨v.piecewise (fun _ ↦ default) f, ?_,
measure_mono_null (fun x ↦ not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
· rw [restrict_piecewise]
apply measurable_const
· rw [restrict_piecewise_compl, restrict_eq]
refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
rw [preimage_comp, Subtype.image_preimage_coe]
convert (hTm s hs).diff hvm using 1
rw [inter_comm]
refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩
