Theorem: norm_iteratedFDeriv_clm_comp_const (ForML/ContinuousLinearMap.lean)

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n (fun y => ContinuousLinearMap.comp (c y) u) x‖ ≤ ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
conv => lhs; arg 1; arg 3; intro y; rw [← ContinuousLinearMap.compL_apply]
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n (fun y => ((ContinuousLinearMap.compL 𝕜 E F G) (c y)) u) x‖ ≤ ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n (fun y => ((ContinuousLinearMap.compL 𝕜 E F G) (c y)) u) x‖ ≤ ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
change ‖iteratedFDeriv 𝕜 n (fun y => (ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G) u).comp (ContinuousLinearMap.compL 𝕜 E F G) (c y)) x‖ ≤ _
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n
        (fun y =>
          (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G))
            (c y))
        x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n
        (fun y =>
          (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G))
            (c y))
        x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
refine le_trans (norm_iteratedFDeriv_clm_const_apply hc) ?_
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ *
      ‖iteratedFDeriv 𝕜 n (fun y => c y) x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ *
      ‖iteratedFDeriv 𝕜 n (fun y => c y) x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ ≤ ‖u‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ ≤ ‖u‖
Tactic:
refine le_trans (ContinuousLinearMap.opNorm_comp_le _ _) ?_
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖
Tactic:
rw [← mul_one ‖u‖]
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖ * 1

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖ * 1
Tactic:
exact mul_le_mul ContinuousLinearMap.opNorm_apply_le (ContinuousLinearMap.norm_compL_le 𝕜 E F G) (norm_nonneg _) (norm_nonneg _)
State after:
no goals