English
If f is AEMeasurable and f(x) ∈ t a.e., with t nonempty, there exists a measurable g with range(g) ⊆ t and f =ᵐ g.
Русский
Если f — AЕ-измеримая и f(x) ∈ t почти во всех x, при условии непустоты t существует измеримая g с range(g)⊆t и f =ᵐ g.
LaTeX
$$$\mathrm{AEMeasurable}(f, \mu) \rightarrow \Big( \forall t, (\forall^\text{ae} x, f x ∈ t) \rightarrow t \neq \emptyset \rightarrow \exists g, \mathrm{Measurable}(g) \land \mathrm{range}(g) \subseteq t \land f =^\text{ae}_\mu g \Big)$$$
Lean4
theorem exists_ae_eq_range_subset (H : AEMeasurable f μ) {t : Set β} (ht : ∀ᵐ x ∂μ, f x ∈ t) (h₀ : t.Nonempty) :
∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g := by
classical
let s : Set α := toMeasurable μ {x | f x = H.mk f x ∧ f x ∈ t}ᶜ
let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
refine ⟨g, ?_, ?_, ?_⟩
· exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
· rintro _ ⟨x, rfl⟩
by_cases hx : x ∈ s
· simpa [g, hx] using h₀.some_mem
· simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
contrapose! hx
apply subset_toMeasurable
simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and, not_false_iff, imp_true_iff]
· have A : μ (toMeasurable μ {x | f x = H.mk f x ∧ f x ∈ t}ᶜ) = 0 :=
by
rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
exact H.ae_eq_mk.and ht
filter_upwards [compl_mem_ae_iff.2 A] with x hx
rw [mem_compl_iff] at hx
simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
contrapose! hx
apply subset_toMeasurable
simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]
