English
For hp ≠ 0, and c ∈ 𝕜, f ∈ lp E p, the inequality ‖c • f‖ ≤ ‖c‖ · ‖f‖ holds, with refinement in the ENNReal and NNReal cases.
Русский
Пусть hp ≠ 0, тогда для любого c ∈ 𝕜, f ∈ lp(E,p) выполняется неравенство ‖c • f‖ ≤ ‖c‖ · ‖f‖ (с уточнениями в ENNReal/NNReal).
LaTeX
$$$\\|c\\cdot f\\|_p \\le \\|c\\| \\cdot \\|f\\|_p$$$
Lean4
theorem norm_const_smul (hp : p ≠ 0) {c : 𝕜} (f : lp E p) : ‖c • f‖ = ‖c‖ * ‖f‖ :=
by
obtain rfl | hc := eq_or_ne c 0
· simp
refine le_antisymm (norm_const_smul_le hp c f) ?_
have := mul_le_mul_of_nonneg_left (norm_const_smul_le hp c⁻¹ (c • f)) (norm_nonneg c)
rwa [inv_smul_smul₀ hc, norm_inv, mul_inv_cancel_left₀ (norm_ne_zero_iff.mpr hc)] at this
