Theorem: Function.hasTemperateGrowth_id (ForML/HasTemperateGrowth.lean)

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
⊢ HasTemperateGrowth id
Tactic:
refine ⟨contDiff_id, ?_⟩
State after:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
State after:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨1, 1, ?_⟩
State after:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ 1 * (1 + ‖x‖) ^ 1

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n id x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Tactic:
intro x
State after:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n id x‖ ≤ 1 * (1 + ‖x‖) ^ 1

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n id x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Tactic:
simp
State after:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n id x‖ ≤ 1 + ‖x‖

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n id x‖ ≤ 1 + ‖x‖
Tactic:
cases n with
| zero => simp
| succ n =>
  rw [iteratedFDeriv_succ_eq_comp_right]
  simp
  cases n with
  | zero => simp; refine le_trans ContinuousLinearMap.norm_id_le (by simp)
  | succ n => simp [iteratedFDeriv_const_of_ne]
State after:
no goals

State before:
case zero
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero id x‖ ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals

State before:
case succ
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ (Nat.succ n) id x‖ ≤ 1 + ‖x‖
Tactic:
rw [iteratedFDeriv_succ_eq_comp_right]
State after:
case succ
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
n : ℕ
⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ n E E) ∘ iteratedFDeriv ℝ n fun y => fderiv ℝ id y) x‖ ≤ 1 + ‖x‖

State before:
case succ
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
n : ℕ
⊢ ‖(⇑(continuousMultilinearCurryRightEquiv' ℝ n E E) ∘ iteratedFDeriv ℝ n fun y => fderiv ℝ id y) x‖ ≤ 1 + ‖x‖
Tactic:
simp
State after:
case succ
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => ContinuousLinearMap.id ℝ E) x‖ ≤ 1 + ‖x‖

State before:
case succ
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => ContinuousLinearMap.id ℝ E) x‖ ≤ 1 + ‖x‖
Tactic:
cases n with
| zero => simp; refine le_trans ContinuousLinearMap.norm_id_le (by simp)
| succ n => simp [iteratedFDeriv_const_of_ne]
State after:
no goals

State before:
case succ.zero
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero (fun y => ContinuousLinearMap.id ℝ E) x‖ ≤ 1 + ‖x‖
Tactic:
simp
State after:
case succ.zero
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
⊢ ‖ContinuousLinearMap.id ℝ E‖ ≤ 1 + ‖x‖

State before:
case succ.zero
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
⊢ ‖ContinuousLinearMap.id ℝ E‖ ≤ 1 + ‖x‖
Tactic:
refine le_trans ContinuousLinearMap.norm_id_le (by simp)
State after:
no goals

State before:
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
⊢ 1 ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals

State before:
case succ.succ
E : Type u_1
F : Type u_2
G : Type u_3
𝔸 : Type u_4
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
𝕜 : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAlgebra ℝ 𝕜
inst✝¹ : IsScalarTower ℝ 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ (Nat.succ n) (fun y => ContinuousLinearMap.id ℝ E) x‖ ≤ 1 + ‖x‖
Tactic:
simp [iteratedFDeriv_const_of_ne]
State after:
no goals