English
If a function is continuous on a set s and s is measurable, then the function is almost everywhere measurable with respect to the restricted measure μ.restrict s.
Русский
Если функция непрерывна на множестве s и множеста s измеримо, то функция является почти везде измеримой относительно ограниченной меры μ.restrict s.
LaTeX
$$$\\text{AEMeasurable } f \\, (\\mu \\restriction s)$, given that $f$ is continuous on $s$ and $s$ is measurable.$$
Lean4
/-- A function which is continuous on a set `s` is almost everywhere measurable with respect to
`μ.restrict s`. -/
theorem aemeasurable [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β]
[BorelSpace β] {f : α → β} {s : Set α} {μ : Measure α} (hf : ContinuousOn f s) (hs : MeasurableSet s) :
AEMeasurable f (μ.restrict s) := by
classical
nontriviality α; inhabit α
have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
refine ⟨Set.piecewise s f fun _ => f default, ?_, this.symm⟩
apply measurable_of_isOpen
intro t ht
obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s := _root_.continuousOn_iff'.1 hf t ht
rw [piecewise_preimage, Set.ite, hu]
exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)
