internlm/Lean-Github huggingface dataset:
Theorem: hasFDerivAt_continuousMultilinearMap_apply_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → ContinuousMultilinearMap 𝕜 E G
v : (i : Fin n) → E i
x : α
c' : α →L[𝕜] ContinuousMultilinearMap 𝕜 E G
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (fun y => (c y) v) ((ContinuousLinearMap.flipMultilinear c') v) x
Tactic:
change HasFDerivAt (ContinuousMultilinearMap.apply 𝕜 E G v ∘ c) _ _
Proof state after:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → ContinuousMultilinearMap 𝕜 E G
v : (i : Fin n) → E i
x : α
c' : α →L[𝕜] ContinuousMultilinearMap 𝕜 E G
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (⇑(ContinuousMultilinearMap.apply 𝕜 E G v) ∘ c) ((ContinuousLinearMap.flipMultilinear c') v) x
Theorem: hasFDerivAt_continuousMultilinearMap_apply_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → ContinuousMultilinearMap 𝕜 E G
v : (i : Fin n) → E i
x : α
c' : α →L[𝕜] ContinuousMultilinearMap 𝕜 E G
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (⇑(ContinuousMultilinearMap.apply 𝕜 E G v) ∘ c) ((ContinuousLinearMap.flipMultilinear c') v) x
Tactic:
exact (HasFDerivAt.comp x (ContinuousLinearMap.hasFDerivAt _) hc)
Proof state after:
no goals
Theorem: HasFDerivAt.clm_apply_const
Proof 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
c : α → F →L[𝕜] G
v : F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (fun y => (c y) v) ((ContinuousLinearMap.flip c') v) x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.clm_apply hc (hasFDerivAt_const v x)) ?_
Proof 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
c : α → F →L[𝕜] G
v : F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ ContinuousLinearMap.comp (c x) 0 + (ContinuousLinearMap.flip c') v = (ContinuousLinearMap.flip c') v
Theorem: HasFDerivAt.clm_apply_const
Proof 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
c : α → F →L[𝕜] G
v : F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ ContinuousLinearMap.comp (c x) 0 + (ContinuousLinearMap.flip c') v = (ContinuousLinearMap.flip c') v
Tactic:
simp
Proof state after:
no goals
Theorem: fderiv_clm_apply_const
Proof 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
c : α → F →L[𝕜] G
v : F
x : α
hc : DifferentiableAt 𝕜 c x
⊢ fderiv 𝕜 (fun y => (c y) v) x = (ContinuousLinearMap.flip (fderiv 𝕜 c x)) v
Tactic:
simp [fderiv_clm_apply hc (differentiableAt_const v)]
Proof state after:
no goals
Theorem: fderiv_clm_apply_comm
Proof 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
c : α → F →L[𝕜] G
v : F
x m : α
hc : DifferentiableAt 𝕜 c x
⊢ (fderiv 𝕜 (fun y => (c y) v) x) m = ((fderiv 𝕜 c x) m) v
Tactic:
simp [fderiv_clm_apply_const hc]
Proof state after:
no goals
Theorem: HasFDerivAt.clm_comp_const
Proof 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
c : α → F →L[𝕜] G
u : E →L[𝕜] F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (fun y => ContinuousLinearMap.comp (c y) u)
    (ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) u) c') x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.clm_comp hc (hasFDerivAt_const u x)) ?_
Proof 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
c : α → F →L[𝕜] G
u : E →L[𝕜] F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) (c x)) 0 +
      ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) u) c' =
    ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) u) c'
Theorem: HasFDerivAt.clm_comp_const
Proof 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
c : α → F →L[𝕜] G
u : E →L[𝕜] F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) (c x)) 0 +
      ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) u) c' =
    ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) u) c'
Tactic:
rw [ContinuousLinearMap.comp_zero, zero_add]
Proof state after:
no goals
Theorem: HasFDerivAt.const_clm_comp
Proof 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
c : F →L[𝕜] G
u : α → E →L[𝕜] F
u' : α →L[𝕜] E →L[𝕜] F
x : α
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun y => ContinuousLinearMap.comp c (u y))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u') x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.clm_comp (hasFDerivAt_const c x) hu) ?_
Proof 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
c : F →L[𝕜] G
u : α → E →L[𝕜] F
u' : α →L[𝕜] E →L[𝕜] F
x : α
hu : HasFDerivAt u u' x
⊢ ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u' +
      ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) (u x)) 0 =
    ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u'
Theorem: HasFDerivAt.const_clm_comp
Proof 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
c : F →L[𝕜] G
u : α → E →L[𝕜] F
u' : α →L[𝕜] E →L[𝕜] F
x : α
hu : HasFDerivAt u u' x
⊢ ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u' +
      ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) (u x)) 0 =
    ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u'
Tactic:
rw [ContinuousLinearMap.comp_zero, add_zero]
Proof state after:
no goals
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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 _)) ?_
Proof 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‖
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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]
Proof 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
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof 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
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof 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
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof state after:
no goals
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof state after:
no goals
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof 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
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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]
Proof 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
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof state after:
no goals
Theorem: norm_iteratedFDeriv_clm_const_apply
Proof 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
Proof state after:
no goals
Theorem: ContinuousLinearMap.opNorm_apply_le
Proof 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
u : E
⊢ ‖(apply 𝕜 G) u‖ ≤ ‖u‖
Tactic:
rw [opNorm_le_iff (norm_nonneg _)]
Proof 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
u : E
⊢ ∀ (x : E →L[𝕜] G), ‖((apply 𝕜 G) u) x‖ ≤ ‖u‖ * ‖x‖
Theorem: ContinuousLinearMap.opNorm_apply_le
Proof 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
u : E
⊢ ∀ (x : E →L[𝕜] G), ‖((apply 𝕜 G) u) x‖ ≤ ‖u‖ * ‖x‖
Tactic:
intro c
Proof 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
u : E
c : E →L[𝕜] G
⊢ ‖((apply 𝕜 G) u) c‖ ≤ ‖u‖ * ‖c‖