Theorem: SchwartzMap.decay_of_decay₁ (ForML/SchwartzLp.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
h : ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
intro k 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
h : ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
k n : ℕ
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

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
h : ∀ (k n : ℕ), ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
k n : ℕ
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
specialize h k 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
k n : ℕ
h : ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

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
k n : ℕ
h : ∃ C, ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
rcases h with ⟨C, hC⟩
State after:
case intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

State before:
case intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
use C
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
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

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
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
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
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

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
k n : ℕ
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
specialize hC 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
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C

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
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
Tactic:
refine le_trans ?_ hC
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
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖

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
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
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
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k

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
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
Tactic:
simp [pow_le_pow_left]
State after:
no goals