English
Let s be a measurable set and f,g be functions α → ε. Then the Lp-essential supremum of the piecewise function that equals f on s and g on the complement equals the maximum of the Lp-essential supremums on each piece with respect to the restricted measures.
Русский
Пусть s — измеримое множество, а функции f,g: α → ε. Тогда ess sup по Lp от кусочно заданной функции, равной f на s и g на дополнении, равен максимуму ess sup по Lp от f на μ|s и от g на μ|sᶜ.
LaTeX
$$$\\mathrm{eLpNormEssSup}(s\\,\\text{piecewise } f\\, g)\\,μ = \\max\\big( \\mathrm{eLpNormEssSup}(f, μ\\restriction s), \\mathrm{eLpNormEssSup}(g, μ\\restriction s^{c}) \\big).$$$
Lean4
theorem eLpNormEssSup_piecewise (f g : α → ε) [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :
eLpNormEssSup (Set.piecewise s f g) μ = max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ)) :=
by
simp only [eLpNormEssSup, ← ENNReal.essSup_piecewise hs]
congr with x
by_cases hx : x ∈ s <;> simp [hx]
