internlm/Lean-Github huggingface dataset:
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_1
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i ∈ Finset.range (n + 1)
Tactic:
simp
Proof state after:
case h.refine_1
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i < n + 1
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_1
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n - i < n + 1
Tactic:
exact Nat.sub_lt_succ n i
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.clm_apply
Proof state before:
case h.refine_2
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f_nonneg : 0 ≤ C_f
hC_f : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
left✝ : 0 ≤ C_g
hC_g : ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
x : D
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ 0 ≤ C_f * (1 + ‖x‖) ^ k_f
Tactic:
simp [hC_f_nonneg]
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_id
Proof 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, ?_⟩
Proof 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
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof 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
Theorem: Function.hasTemperateGrowth_id
Proof 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, ?_⟩
Proof 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
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof 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
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof 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‖
Theorem: Function.hasTemperateGrowth_id
Proof 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]
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_id
Proof 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]
Proof 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‖
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof 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‖
Theorem: Function.hasTemperateGrowth_id
Proof 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]
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof 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‖
Theorem: Function.hasTemperateGrowth_id
Proof 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)
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_id
Proof 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
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_id
Proof 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]
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_div_const
Proof 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
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra ℝ 𝔸
a : 𝔸
⊢ HasTemperateGrowth fun x => x / a
Tactic:
simp_rw [div_eq_mul_inv]
Proof 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
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra ℝ 𝔸
a : 𝔸
⊢ HasTemperateGrowth fun x => x * a⁻¹
Theorem: Function.hasTemperateGrowth_div_const
Proof 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
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra ℝ 𝔸
a : 𝔸
⊢ HasTemperateGrowth fun x => x * a⁻¹
Tactic:
exact hasTemperateGrowth_mul_const a⁻¹
Proof state after:
no goals
Theorem: Function.HasTemperateGrowth.add
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
⊢ HasTemperateGrowth fun x => f x + g x
Tactic:
refine ⟨ContDiff.add hf.1 hg.1, ?_⟩
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.add
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.add
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hf.2 n with ⟨k_f, C_f, hC_f⟩
Proof state after:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.add
Proof state before:
case intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hg.2 n with ⟨k_g, C_g, hC_g⟩
Proof state after:
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.add
Proof state before:
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hC_f_nonneg : 0 ≤ C_f
Proof state after:
case hC_f_nonneg
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ 0 ≤ C_f

case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.HasTemperateGrowth.add
Proof state before:
case hC_f_nonneg
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
⊢ 0 ≤ C_f

case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
. have := le_trans (norm_nonneg _) (hC_f 0)
  simpa using this
Proof state after:
case intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf : HasTemperateGrowth f
g : E → F
hg : HasTemperateGrowth g
n k_f : ℕ
C_f : ℝ
hC_f : ∀ (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ k_f
k_g : ℕ
C_g : ℝ
hC_g : ∀ (x : E), ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ k_g
hC_f_nonneg : 0 ≤ C_f
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k