English
An AEStronglyMeasurable function is equivalent to being AEMeasurable together with the property that its range is contained in a separable set up to a.e. equality.
Русский
AEStronglyMeasurable эквивалентно AEMeasurable с условием, что диапазон лежит в сепарабельном множестве до а.е. равенства.
LaTeX
$$$AEStronglyMeasurable(f, \mu) \iff (AEMeasurable(f, \mu) \land \exists t, IsSeparable t \land ∀ᵐ x ∂\mu, f x ∈ t)$$$
Lean4
/-- A function is almost everywhere strongly measurable if and only if it is almost everywhere
measurable, and up to a zero measure set its range is contained in a separable set. -/
theorem _root_.aestronglyMeasurable_iff_aemeasurable_separable [PseudoMetrizableSpace β] [MeasurableSpace β]
[BorelSpace β] : AEStronglyMeasurable f μ ↔ AEMeasurable f μ ∧ ∃ t : Set β, IsSeparable t ∧ ∀ᵐ x ∂μ, f x ∈ t :=
by
refine ⟨fun H => ⟨H.aemeasurable, H.isSeparable_ae_range⟩, ?_⟩
rintro ⟨H, ⟨t, t_sep, ht⟩⟩
rcases eq_empty_or_nonempty t with (rfl | h₀)
· simp only [mem_empty_iff_false, eventually_false_iff_eq_bot, ae_eq_bot] at ht
rw [ht]
exact aestronglyMeasurable_zero_measure f
· obtain ⟨g, g_meas, gt, fg⟩ : ∃ g : α → β, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g :=
H.exists_ae_eq_range_subset ht h₀
refine ⟨g, ?_, fg⟩
exact stronglyMeasurable_iff_measurable_separable.2 ⟨g_meas, t_sep.mono gt⟩
