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

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, ?_⟩
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

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
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

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⟩
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

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⟩
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

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
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

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
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

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
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 hC_g_nonneg : 0 ≤ C_g
State after:
case hC_g_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
hC_f_nonneg : 0 ≤ C_f
⊢ 0 ≤ C_g

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
hC_g_nonneg : 0 ≤ C_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case hC_g_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
hC_f_nonneg : 0 ≤ C_f
⊢ 0 ≤ C_g

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
hC_g_nonneg : 0 ≤ C_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
. have := le_trans (norm_nonneg _) (hC_g 0)
  simpa using this
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
hC_g_nonneg : 0 ≤ C_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k

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
hC_f_nonneg : 0 ≤ C_f
hC_g_nonneg : 0 ≤ C_g
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
use max k_f k_g
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
⊢ ∃ C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
⊢ ∃ C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ C * (1 + ‖x‖) ^ max k_f k_g
Tactic:
use C_f + C_g
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g
Tactic:
intro x
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => f x + g x) x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g
Tactic:
change ‖iteratedFDeriv ℝ n (f + g) x‖ ≤ _
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n (f + g) x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n (f + g) x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g
Tactic:
rw [iteratedFDeriv_add_apply (hf.1.of_le le_top) (hg.1.of_le le_top)]
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x + iteratedFDeriv ℝ n g x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x + iteratedFDeriv ℝ n g x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine le_trans (norm_add_le _ _) ?_
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ + ‖iteratedFDeriv ℝ n g x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ + ‖iteratedFDeriv ℝ n g x‖ ≤ (C_f + C_g) * (1 + ‖x‖) ^ max k_f k_g
Tactic:
simp [add_mul]
State after:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ + ‖iteratedFDeriv ℝ n g x‖ ≤ C_f * (1 + ‖x‖) ^ max k_f k_g + C_g * (1 + ‖x‖) ^ max k_f k_g

State before:
case h
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ + ‖iteratedFDeriv ℝ n g x‖ ≤ C_f * (1 + ‖x‖) ^ max k_f k_g + C_g * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine add_le_add ?_ ?_
State after:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ max k_f k_g

case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g

State before:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ max k_f k_g

case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g
Tactic:
. refine le_trans (hC_f x) ?_
  refine mul_le_mul_of_nonneg_left ?_ hC_f_nonneg
  exact pow_le_pow_right (by simp) (by simp)
State after:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g

State before:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g
Tactic:
. refine le_trans (hC_g x) ?_
  refine mul_le_mul_of_nonneg_left ?_ hC_g_nonneg
  exact pow_le_pow_right (by simp) (by simp)
State after:
no goals

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
Tactic:
have := le_trans (norm_nonneg _) (hC_f 0)
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
this : 0 ≤ C_f * (1 + ‖0‖) ^ k_f
⊢ 0 ≤ C_f

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
this : 0 ≤ C_f * (1 + ‖0‖) ^ k_f
⊢ 0 ≤ C_f
Tactic:
simpa using this
State after:
no goals

State before:
case hC_g_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
hC_f_nonneg : 0 ≤ C_f
⊢ 0 ≤ C_g
Tactic:
have := le_trans (norm_nonneg _) (hC_g 0)
State after:
case hC_g_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
hC_f_nonneg : 0 ≤ C_f
this : 0 ≤ C_g * (1 + ‖0‖) ^ k_g
⊢ 0 ≤ C_g

State before:
case hC_g_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
hC_f_nonneg : 0 ≤ C_f
this : 0 ≤ C_g * (1 + ‖0‖) ^ k_g
⊢ 0 ≤ C_g
Tactic:
simpa using this
State after:
no goals

State before:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n f x‖ ≤ C_f * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine le_trans (hC_f x) ?_
State after:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ C_f * (1 + ‖x‖) ^ k_f ≤ C_f * (1 + ‖x‖) ^ max k_f k_g

State before:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ C_f * (1 + ‖x‖) ^ k_f ≤ C_f * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine mul_le_mul_of_nonneg_left ?_ hC_f_nonneg
State after:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ (1 + ‖x‖) ^ k_f ≤ (1 + ‖x‖) ^ max k_f k_g

State before:
case h.refine_1
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ (1 + ‖x‖) ^ k_f ≤ (1 + ‖x‖) ^ max k_f k_g
Tactic:
exact pow_le_pow_right (by simp) (by simp)
State after:
no goals

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_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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ 1 ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals

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_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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ k_f ≤ max k_f k_g
Tactic:
simp
State after:
no goals

State before:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ ‖iteratedFDeriv ℝ n g x‖ ≤ C_g * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine le_trans (hC_g x) ?_
State after:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ C_g * (1 + ‖x‖) ^ k_g ≤ C_g * (1 + ‖x‖) ^ max k_f k_g

State before:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ C_g * (1 + ‖x‖) ^ k_g ≤ C_g * (1 + ‖x‖) ^ max k_f k_g
Tactic:
refine mul_le_mul_of_nonneg_left ?_ hC_g_nonneg
State after:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ (1 + ‖x‖) ^ k_g ≤ (1 + ‖x‖) ^ max k_f k_g

State before:
case h.refine_2
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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ (1 + ‖x‖) ^ k_g ≤ (1 + ‖x‖) ^ max k_f k_g
Tactic:
exact pow_le_pow_right (by simp) (by simp)
State after:
no goals

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_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
hC_g_nonneg : 0 ≤ C_g
x : E
⊢ k_g ≤ max k_f k_g
Tactic:
simp
State after:
no goals