English
For f in lp E ∞, the norm is zero if and only if f = 0.
Русский
Для f в lp E ∞ норма равна нулю тогда и только тогда, когда f = 0.
LaTeX
$$$$ \|f\| = 0 \iff f = 0. $$$$
Lean4
theorem norm_eq_zero_iff {f : lp E p} : ‖f‖ = 0 ↔ f = 0 :=
by
refine ⟨fun h => ?_, by rintro rfl; exact norm_zero⟩
rcases p.trichotomy with (rfl | rfl | hp)
· ext i
have : {i : α | ¬f i = 0} = ∅ := by simpa [lp.norm_eq_card_dsupport f] using h
have : (¬f i = 0) = False := congr_fun this i
tauto
· rcases isEmpty_or_nonempty α with _i | _i
· simp [eq_iff_true_of_subsingleton]
have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using lp.isLUB_norm f
ext i
have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)
simpa using this
· have hf : HasSum (fun i : α => ‖f i‖ ^ p.toReal) 0 :=
by
have := lp.hasSum_norm hp f
rwa [h, Real.zero_rpow hp.ne'] at this
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _
rw [hasSum_zero_iff_of_nonneg this] at hf
ext i
have : f i = 0 ∧ p.toReal ≠ 0 := by simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using congr_fun hf i
exact this.1
