Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_inv_one_add_norm (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)
p : ℝ
hp : 0 < p
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Tactic:
have := pow_norm_iteratedFDeriv_le_pow_one_add_norm f hp 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)
p : ℝ
hp : 0 < p
this : ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-1)
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹

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)
p : ℝ
hp : 0 < p
this : ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-1)
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Tactic:
simpa [Real.rpow_neg_one]
State after:
no goals