Theorem: Function.HasTemperateGrowth.fderiv (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
⊢ HasTemperateGrowth fun x => _root_.fderiv ℝ f x
Tactic:
refine ⟨hf.1.fderiv_right le_top, ?_⟩
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
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f 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
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f 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
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f 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
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases bound_forall_range (n + 2) hf with ⟨k, C, ⟨_, hC⟩⟩
State after:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨k, C, ?_⟩
State after:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro x
State after:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
suffices : ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
State after:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
this : ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k

case this
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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
this : ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k

case this
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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
. simpa [iteratedFDeriv_succ_eq_comp_right] using this
State after:
case this
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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
case this
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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine hC (n + 1) ?_ x
State after:
case this
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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ n + 1 ∈ Finset.range (n + 2)

State before:
case this
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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
⊢ n + 1 ∈ Finset.range (n + 2)
Tactic:
exact Finset.self_mem_range_succ (n + 1)
State after:
no goals

State before:
case 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
n k : ℕ
C : ℝ
left✝ : 0 ≤ C
hC : ∀ i ∈ Finset.range (n + 2), ∀ (x : E), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
x : E
this : ‖iteratedFDeriv ℝ (n + 1) (fun x => f x) x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ‖iteratedFDeriv ℝ n (fun x => _root_.fderiv ℝ f x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
simpa [iteratedFDeriv_succ_eq_comp_right] using this
State after:
no goals