English
If s is measurable and f,g satisfy MemLp on μ|s and μ|sᶜ respectively, then the piecewise function that agrees with f on s and g on the complement belongs to MemLp on μ.
Русский
Пусть s измеримо и f,g имеют принадлежность MemLp на μ|s и μ|sᶜ соответственно, тогда кусочно заданная функция принадлежит MemLp на μ.
LaTeX
$$$\\text{MeasurableSet } s \\to \\big(\\mathrm{MemLp}(f,p, μ|_s)\\to \\mathrm{MemLp}(g,p, μ|_{s^{c}})\\to \\mathrm{MemLp}(s\\text{.piecewise } f\\, g, p, μ)\\big).$$$
Lean4
protected theorem piecewise {f : α → ε} [DecidablePred (· ∈ s)] {g} (hs : MeasurableSet s)
(hf : MemLp f p (μ.restrict s)) (hg : MemLp g p (μ.restrict sᶜ)) : MemLp (s.piecewise f g) p μ :=
by
by_cases hp_zero : p = 0
· simp only [hp_zero, memLp_zero_iff_aestronglyMeasurable]
exact AEStronglyMeasurable.piecewise hs hf.1 hg.1
refine ⟨AEStronglyMeasurable.piecewise hs hf.1 hg.1, ?_⟩
obtain rfl | hp_top := eq_or_ne p ∞
· rw [eLpNorm_top_piecewise f g hs]
exact max_lt hf.2 hg.2
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_zero hp_top, ← lintegral_add_compl _ hs, ENNReal.add_lt_top]
constructor
· have h (x) (hx : x ∈ s) : ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal := by simp [hx]
rw [setLIntegral_congr_fun hs h]
exact lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hf.2
· have h (x) (hx : x ∈ sᶜ) : ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal :=
by
have hx' : x ∉ s := hx
simp [hx']
rw [setLIntegral_congr_fun hs.compl h]
exact lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hg.2
