English
If f is AEStronglyMeasurable on a measurable set s and g is AEStronglyMeasurable on the complement sᶜ (with respect to μ), then the piecewise function that equals f on s and g on sᶜ is AEStronglyMeasurable on the whole space with respect to μ.
Русский
Если на множестве s функция f имеет свойство AEStronglyMeasurable, а на дополнении sᶜ функция g имеет то же свойство, то функция, которая равна f на s и равна g на sᶜ, является AEStronglyMeasurable на всей области по мере μ.
LaTeX
$$$\text{Meas}(s) \Rightarrow (\text{AEStronglyMeasurable}(f,\mu|_s) \land \text{AEStronglyMeasurable}(g,\mu|_{s^c})) \Rightarrow \text{AEStronglyMeasurable}(s.\text{piecewise } f\; g,\mu).$$$
Lean4
theorem piecewise {s : Set α} [DecidablePred (· ∈ s)] (hs : MeasurableSet s)
(hf : AEStronglyMeasurable f (μ.restrict s)) (hg : AEStronglyMeasurable g (μ.restrict sᶜ)) :
AEStronglyMeasurable (s.piecewise f g) μ :=
by
refine
⟨s.piecewise (hf.mk f) (hg.mk g), StronglyMeasurable.piecewise hs hf.stronglyMeasurable_mk hg.stronglyMeasurable_mk,
?_⟩
refine ae_of_ae_restrict_of_ae_restrict_compl s ?_ ?_
· have h := hf.ae_eq_mk
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at h
rw [ae_restrict_iff' hs]
filter_upwards [h] with x hx
intro hx_mem
simp only [hx_mem, Set.piecewise_eq_of_mem, hx hx_mem]
· have h := hg.ae_eq_mk
rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at h
rw [ae_restrict_iff' hs.compl]
filter_upwards [h] with x hx
intro hx_mem
rw [Set.mem_compl_iff] at hx_mem
simp only [hx_mem, not_false_eq_true, Set.piecewise_eq_of_notMem, hx hx_mem]
