English
If p ≠ 0, then for each i, the coordinate norm satisfies ‖f i‖ ≤ ‖f‖ (with a suitable real exponent if p ≠ ∞).
Русский
Если p ≠ 0, то для каждого i выполняется ‖f_i‖ ≤ ‖f‖ (с учётом соответствующего вещественного показателя, когда p ≠ ∞).
LaTeX
$$$$ \|f_i\| \le \|f\|, \quad \text{для каждого } i. $$$$
Lean4
theorem norm_apply_le_norm (hp : p ≠ 0) (f : lp E p) (i : α) : ‖f i‖ ≤ ‖f‖ :=
by
rcases eq_or_ne p ∞ with (rfl | hp')
· haveI : Nonempty α := ⟨i⟩
exact (isLUB_norm f).1 ⟨i, rfl⟩
have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp hp'
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _
rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']
convert le_hasSum (hasSum_norm hp'' f) i fun i _ => this i
