English
Let f be a continuous affine map from V to W and g a continuous affine map from W2 to V. Then the operator norm of their composition satisfies ||f ∘ g|| ≤ ||f|| · ||g|| + ||f(0)||.
Русский
Пусть f — непрерывная аффинная отображение V → W, а g — непрерывное аффинное отображение W2 → V. Тогда нормa отображения композиции удовлетворяет неравенству ||f ∘ g|| ≤ ||f|| · ||g|| + ||f(0)||.
LaTeX
$$$\\|f \\circ g\\| \\leq \\|f\\| \\cdot \\|g\\| + \\|f(0)\\|$$$
Lean4
theorem norm_comp_le (g : W₂ →ᴬ[𝕜] V) : ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ :=
by
rw [norm_def, max_le_iff]
constructor
·
calc
‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
_ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
_ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := ((norm_add_le _ _).trans (add_le_add_right (f.contLinear.le_opNorm _) _))
_ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ :=
add_le_add_right (mul_le_mul f.norm_contLinear_le g.norm_image_zero_le (norm_nonneg _) (norm_nonneg _)) _
·
calc
‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
(g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
_ ≤ ‖f‖ * ‖g‖ := (mul_le_mul f.norm_contLinear_le g.norm_contLinear_le (norm_nonneg _) (norm_nonneg _))
_ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg
