have hb_pos : 0 < 1 + ‖x‖
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
case hb_pos
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
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ 0 < 1 + ‖x‖

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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))