nnnorm_eq_zero_iff — Mathlib

English

Let p > 0. For every f in Lp, the nonnegative norm vanishes if and only if f = 0.

Русский

Пусть p > 0. Для каждого f в Lp нормa по неконечному модулю ноль тогда и только тогда, когда f = 0.

LaTeX

$$$\forall f \in Lp\, E\, p\ μ\, (hp : 0 < p): \; ‖f‖_+ = 0 \iff f = 0$$$

Lean4

theorem nnnorm_eq_zero_iff {f : Lp E p μ} (hp : 0 < p) : ‖f‖₊ = 0 ↔ f = 0 :=
  by
  refine ⟨fun hf => ?_, fun hf => by simp [hf]⟩
  rw [nnnorm_def, ENNReal.toNNReal_eq_zero_iff] at hf
  cases hf with
  | inl hf =>
    rw [eLpNorm_eq_zero_iff (Lp.aestronglyMeasurable f) hp.ne.symm] at hf
    exact Subtype.eq (AEEqFun.ext (hf.trans AEEqFun.coeFn_zero.symm))
  | inr hf => exact absurd hf (eLpNorm_ne_top f)

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