Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_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
q : ℝ
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)

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
q : ℝ
n : ℕ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
generalize hr : q / p = r
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
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)

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
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
rcases norm_iteratedFDeriv_le_pow_one_add_norm f r n with ⟨C, ⟨hC_nonneg, hC⟩⟩
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)

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

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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
have hC_pow : 0 ≤ C ^ p := Real.rpow_nonneg hC_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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)

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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ 0 ≤ C ^ p ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
refine And.intro hC_pow ?_
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)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)

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

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

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)
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)
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
have hq : q = p * r := by rw [← hr, mul_div, mul_div_cancel_left _ hp.ne']
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)
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‖) ^ (-q)

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)
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‖) ^ (-q)
Tactic:
rw [hq]
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)
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))

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)
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))
Tactic:
have hb_pos : 0 < 1 + ‖x‖
State after:
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))

State before:
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))
Tactic:
. exact add_pos_of_pos_of_nonneg zero_lt_one (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)
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))

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)
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))
Tactic:
rw [mul_comm p r, ← neg_mul, Real.rpow_mul hb_pos.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)
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‖) ^ (-r)) ^ p

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)
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‖) ^ (-r)) ^ p
Tactic:
rw [← Real.mul_rpow hC_nonneg (Real.rpow_nonneg hb_pos.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)
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 * (1 + ‖x‖) ^ (-r)) ^ p

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)
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 * (1 + ‖x‖) ^ (-r)) ^ p
Tactic:
exact Real.rpow_le_rpow (norm_nonneg _) hC hp.le
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)
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)
⊢ q = p * r
Tactic:
rw [← hr, mul_div, mul_div_cancel_left _ hp.ne']
State after:
no goals

State before:
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‖
Tactic:
exact add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
State after:
no goals