memLp_norm_iff — Mathlib

English

Let f: α → E be AEStronglyMeasurable with respect to μ. Then f belongs to Lp(μ) if and only if the function x ↦ ∥f(x)∥ belongs to Lp(μ).

Русский

Пусть f: α → E измерима по μ в сильном смысле. Тогда f ∈ Lp(μ) тогда и только тогда, когда x ↦ ∥f(x)∥ ∈ Lp(μ).

LaTeX

$$$\\operatorname{MemLp}(\\lambda x. \\|f(x)\\|)\\,p\\,\\mu \\;\\Longleftrightarrow\\; \\operatorname{MemLp}(f)\\,p\\,\\mu$$$

Lean4

theorem memLp_norm_iff {f : α → E} (hf : AEStronglyMeasurable f μ) : MemLp (fun x => ‖f x‖) p μ ↔ MemLp f p μ :=
  ⟨fun h => ⟨hf, by rw [← eLpNorm_norm]; exact h.2⟩, fun h => h.norm⟩

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