English
If the support of f is contained in s, then restricting the measure to s does not change the Lp-norm of f.
Русский
Если опора функции f содержится в s, то ограничение меры до s не меняет норму Lp функции f.
LaTeX
$$$\\mathrm{supp}(f) \\subseteq s \\implies \\|f\\|_{Lp(p, μ|_s)} = \\|f\\|_{Lp(p, μ)}.$$$
Lean4
/-- For a function `f` with support in `s`, the Lᵖ norms of `f` with respect to `μ` and
`μ.restrict s` are the same. -/
theorem eLpNorm_restrict_eq_of_support_subset {s : Set α} {f : α → ε} (hsf : f.support ⊆ s) :
eLpNorm f p (μ.restrict s) = eLpNorm f p μ :=
by
by_cases hp0 : p = 0
· simp [hp0]
by_cases hp_top : p = ∞
· simp only [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
exact ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx
· simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top, eLpNorm'_eq_lintegral_enorm]
congr 1
apply setLIntegral_eq_of_support_subset
have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top
simpa [this] using hsf
