eLpNorm_top_piecewise — Mathlib

English

Let s be measurable and f,g: α → ε. Then the Lp-norm with exponent ∞ of the piecewise function equals the maximum of the ∞-norms on the restricted pieces: μ|s and μ|sᶜ.

Русский

Пусть s измеримо и f,g: α → ε. Тогда ∥s.piecewise(f,g)∥_{Lp,∞,μ} = max(∥f∥_{Lp,∞,μ|s}, ∥g∥_{Lp,∞,μ|sᶜ}).

LaTeX

$$$\\mathrm{eLpNorm}(\\mathrm{piecewise}(s,f,g))\\,μ = \\max\\big( \\mathrm{eLpNorm}(f,∞, μ\\restriction s), \\mathrm{eLpNorm}(g,∞, μ\\restriction s^{c}) \\big).$$$

Lean4

theorem eLpNorm_top_piecewise (f g : α → ε) [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :
    eLpNorm (Set.piecewise s f g) ∞ μ = max (eLpNorm f ∞ (μ.restrict s)) (eLpNorm g ∞ (μ.restrict sᶜ)) :=
  eLpNormEssSup_piecewise f g hs

Похожие утверждения