English
If a function f is almost everywhere strongly measurable and its range is almost everywhere contained in a nonempty measurable set s, then there exists a strongly measurable representative g with values in s (i.e., g(x) ∈ s for all x) such that f = g almost everywhere.
Русский
Если функция f почти везде сильно измерима и её значения почти всюду lie в ненулевом измеримом множестве s, тогда существует сильно измеримая замена g, чьи значения лежат в s, и f = g почти всюду.
LaTeX
$$$\exists g:\alpha \to \beta,\; \text{StronglyMeasurable}(g) \land (\forall x, g(x) \in s) \land f =_{\mu} g.$$$
Lean4
/-- If `f` is almost everywhere strongly measurable and its range is almost everywhere contained
in a nonempty measurable set `s`, then there is a strongly measurable representative `g` of `f`
whose range is contained in `s`. -/
theorem exists_stronglyMeasurable_range_subset {α β : Type*} [TopologicalSpace β] [PseudoMetrizableSpace β]
[mb : MeasurableSpace β] [BorelSpace β] [m : MeasurableSpace α] {μ : Measure α} {f : α → β}
(hf : AEStronglyMeasurable f μ) {s : Set β} (hs : MeasurableSet s) (h_nonempty : s.Nonempty)
(h_mem : ∀ᵐ x ∂μ, f x ∈ s) : ∃ g : α → β, StronglyMeasurable g ∧ (∀ x, g x ∈ s) ∧ f =ᵐ[μ] g :=
by
obtain ⟨f', hf', hff'⟩ := hf
classical
refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const
case subset =>
rw [← Set.range_subset_iff]
simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem
case ae_eq =>
apply hff'.trans
filter_upwards [h_mem, hff'] with x hx hx'
exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)
