Theorem: norm_iteratedFDeriv_clm_const_apply (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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ‖iteratedFDeriv 𝕜 n (fun y => c (u y)) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n u x‖
Tactic:
refine le_trans (norm_iteratedFDeriv_clm_apply contDiff_const hu x (le_refl _)) ?_
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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∑ i in Finset.range (n + 1),
      ↑(Nat.choose n i) * ‖iteratedFDeriv 𝕜 i (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - i) u x‖ ≤
    ‖c‖ * ‖iteratedFDeriv 𝕜 n u 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∑ i in Finset.range (n + 1),
      ↑(Nat.choose n i) * ‖iteratedFDeriv 𝕜 i (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - i) u x‖ ≤
    ‖c‖ * ‖iteratedFDeriv 𝕜 n u x‖
Tactic:
rw [Finset.sum_eq_single 0]
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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ ≤
    ‖c‖ * ‖iteratedFDeriv 𝕜 n u x‖

case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∀ b ∈ Finset.range (n + 1),
    b ≠ 0 → ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0

case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0

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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ ≤
    ‖c‖ * ‖iteratedFDeriv 𝕜 n u x‖

case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∀ b ∈ Finset.range (n + 1),
    b ≠ 0 → ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0

case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0
Tactic:
. simp
State after:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∀ b ∈ Finset.range (n + 1),
    b ≠ 0 → ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0

case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0

State before:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∀ b ∈ Finset.range (n + 1),
    b ≠ 0 → ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0

case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0
Tactic:
. intro b _ hb
  rw [iteratedFDeriv_const_of_ne hb]
  simp
State after:
case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0

State before:
case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0
Tactic:
. simp
State after:
no goals

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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ ≤
    ‖c‖ * ‖iteratedFDeriv 𝕜 n u x‖
Tactic:
simp
State after:
no goals

State before:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ ∀ b ∈ Finset.range (n + 1),
    b ≠ 0 → ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0
Tactic:
intro b _ hb
State after:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
b : ℕ
a✝ : b ∈ Finset.range (n + 1)
hb : b ≠ 0
⊢ ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0

State before:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
b : ℕ
a✝ : b ∈ Finset.range (n + 1)
hb : b ≠ 0
⊢ ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0
Tactic:
rw [iteratedFDeriv_const_of_ne hb]
State after:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
b : ℕ
a✝ : b ∈ Finset.range (n + 1)
hb : b ≠ 0
⊢ ↑(Nat.choose n b) * ‖0 x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0

State before:
case h₀
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
b : ℕ
a✝ : b ∈ Finset.range (n + 1)
hb : b ≠ 0
⊢ ↑(Nat.choose n b) * ‖0 x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0
Tactic:
simp
State after:
no goals

State before:
case h₁
𝕜 : 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 : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
⊢ 0 ∉ Finset.range (n + 1) →
    ↑(Nat.choose n 0) * ‖iteratedFDeriv 𝕜 0 (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - 0) u x‖ = 0
Tactic:
simp
State after:
no goals