English
For p ≠ 0 and c ∈ 𝕜, the norm of c • f equals the product of |c| and the norm of f, for f in lp E p.
Русский
При p ≠ 0 и c ∈ 𝕜 нормa элемента c•f равна произведению |c| на норму f, где f ∈ lp(E,p).
LaTeX
$$$\\|c \\cdot f\\| = \\|c\\| \\cdot \\|f\\|$$$
Lean4
theorem norm_const_smul_le (hp : p ≠ 0) (c : 𝕜) (f : lp E p) : ‖c • f‖ ≤ ‖c‖ * ‖f‖ :=
by
rcases p.trichotomy with (rfl | rfl | hp)
· exact absurd rfl hp
· cases isEmpty_or_nonempty α
· simp [lp.eq_zero' f]
have hcf := lp.isLUB_norm (c • f)
have hfc := (lp.isLUB_norm f).mul_left (norm_nonneg c)
simp_rw [← Set.range_comp, Function.comp_def] at hfc
refine hcf.right ?_
have := hfc.left
simp_rw [mem_upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] at this ⊢
intro a
exact (norm_smul_le _ _).trans (this a)
· letI inst : NNNorm (lp E p) := ⟨fun f => ⟨‖f‖, norm_nonneg' _⟩⟩
have coe_nnnorm : ∀ f : lp E p, ↑‖f‖₊ = ‖f‖ := fun _ => rfl
suffices ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal by rwa [NNReal.rpow_le_rpow_iff hp] at this
clear_value inst
rw [NNReal.mul_rpow]
have hLHS := lp.hasSum_norm hp (c • f)
have hRHS := (lp.hasSum_norm hp f).mul_left (‖c‖ ^ p.toReal)
simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.hasSum_coe] at hRHS hLHS
refine hasSum_mono hLHS hRHS fun i => ?_
dsimp only
rw [← NNReal.mul_rpow, lp.coeFn_smul, Pi.smul_apply]
gcongr
apply nnnorm_smul_le
