𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖ ∧ ‖contLinear (comp f g)‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖comp f g‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
rw [norm_def, max_le_iff]
case left
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖

case right
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖contLinear (comp f g)‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖ ∧ ‖contLinear (comp f g)‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
constructor
no goals
case left
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
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_op_norm _) _))
  _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ :=
    add_le_add_right
      (mul_le_mul f.norm_contLinear_le g.norm_image_zero_le (norm_nonneg _) (norm_nonneg _)) _
no goals
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑(comp f g) 0‖ = ‖↑f (↑g 0)‖
simp
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖(↑(contLinear f) + Function.const V (↑f 0)) (↑g 0)‖ =
    ‖↑(contLinear f) (↑g 0) + (↑(contLinear f) + Function.const V (↑f 0)) 0‖
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖↑f (↑g 0)‖ = ‖↑(contLinear f) (↑g 0) + ↑f 0‖
rw [f.decomp]
no goals
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖(↑(contLinear f) + Function.const V (↑f 0)) (↑g 0)‖ =
    ‖↑(contLinear f) (↑g 0) + (↑(contLinear f) + Function.const V (↑f 0)) 0‖
simp
no goals
case right
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖contLinear (comp f g)‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
calc
  ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
    (g.comp_contLinear f).symm ▸ f.contLinear.op_norm_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
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ 0 ≤ ‖↑f 0‖
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + ‖↑f 0‖
rw [le_add_iff_nonneg_right]
no goals
𝕜 : Type u_1
R : Type ?u.276372
V : Type u_3
W : Type u_4
W₂ : Type u_2
P : Type ?u.276384
Q : Type ?u.276387
Q₂ : Type ?u.276390
inst✝¹⁶ : NormedAddCommGroup V
inst✝¹⁵ : MetricSpace P
inst✝¹⁴ : NormedAddTorsor V P
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : MetricSpace Q
inst✝¹¹ : NormedAddTorsor W Q
inst✝¹⁰ : NormedAddCommGroup W₂
inst✝⁹ : MetricSpace Q₂
inst✝⁸ : NormedAddTorsor W₂ Q₂
inst✝⁷ : NormedField R
inst✝⁶ : NormedSpace R V
inst✝⁵ : NormedSpace R W
inst✝⁴ : NormedSpace R W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →A[𝕜] W
g : W₂ →A[𝕜] V
⊢ 0 ≤ ‖↑f 0‖
apply norm_nonneg