English
Let f be a null-measurable function with values almost surely in a set t such that t is countably generated. If f x ∈ t a.e., then f is a.e.-measurable.
Русский
Пусть f — нулево измеримая функция и значения встречаются почти наверняка в множестве t, где σ-алгебра t порождается счетно. Тогда f а.е.-измерима.
LaTeX
$$$\mathrm{NullMeasurable}(f, μ) \land \text{range}(f) \subseteq t \Rightarrow \mathrm{AEMeasurable}(f, μ)$ for countably generated t.$$
Lean4
/-- Let `f : α → β` be a null measurable function
such that a.e. all values of `f` belong to a set `t`
such that the restriction of the `σ`-algebra in the codomain to `t` is countably generated,
then `f` is a.e.-measurable. -/
theorem aemeasurable_of_aerange {f : α → β} {t : Set β} [MeasurableSpace.CountablyGenerated t] (h : NullMeasurable f μ)
(hft : ∀ᵐ x ∂μ, f x ∈ t) : AEMeasurable f μ :=
by
rcases eq_empty_or_nonempty t with rfl | hne
· obtain rfl : μ = 0 := by simpa using hft
apply aemeasurable_zero_measure
· rw [← μ.ae_completion] at hft
obtain ⟨f', hf'm, hf't, hff'⟩ : ∃ f' : α → β, NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᵐ[μ] f' :=
h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne
rw [range_subset_iff] at hf't
lift f' to α → t using hf't
replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk
exact (measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm
