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

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

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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rcases decay₁ f k n 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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)

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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
refine And.intro ?_ ?_
State after:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C

case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)

State before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C

case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
. specialize hC 0  simp at hC
  exact le_trans (norm_nonneg _) hC
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
. intro x
  specialize hC x
  have h_pos : 0 < 1 + ‖x‖ := add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
  rw [Real.rpow_neg h_pos.le]
  rw [mul_comm, inv_mul_eq_div]
  rw [le_div_iff' (Real.rpow_pos_of_pos h_pos _)]
  refine le_trans ?_ hC
  refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
  rw [← Real.rpow_nat_cast]
  refine Real.rpow_le_rpow_of_exponent_le (by simp) ?_
  simp [← hk]
  exact Nat.le_ceil _
State after:
no goals

State before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ 0 ≤ C
Tactic:
specialize hC 0
State after:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : (1 + ‖0‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C

State before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : (1 + ‖0‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
Tactic:
simp at hC
State after:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C

State before:
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
Tactic:
exact le_trans (norm_nonneg _) hC
State after:
no goals

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
intro x
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ∀ (x : E), (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
specialize hC x
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
have h_pos : 0 < 1 + ‖x‖ := add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rw [Real.rpow_neg h_pos.le]
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * ((1 + ‖x‖) ^ r)⁻¹

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * ((1 + ‖x‖) ^ r)⁻¹
Tactic:
rw [mul_comm, inv_mul_eq_div]
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C / (1 + ‖x‖) ^ r

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C / (1 + ‖x‖) ^ r
Tactic:
rw [le_div_iff' (Real.rpow_pos_of_pos h_pos _)]
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
Tactic:
refine le_trans ?_ hC
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r * ‖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.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ k

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ k
Tactic:
rw [← Real.rpow_nat_cast]
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ ↑k

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ (1 + ‖x‖) ^ r ≤ (1 + ‖x‖) ^ ↑k
Tactic:
refine Real.rpow_le_rpow_of_exponent_le (by simp) ?_
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑k

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑k
Tactic:
simp [← hk]
State after:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑⌈r⌉₊

State before:
case h.refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ r ≤ ↑⌈r⌉₊
Tactic:
exact Nat.le_ceil _
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)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C
h_pos : 0 < 1 + ‖x‖
⊢ 1 ≤ 1 + ‖x‖
Tactic:
simp
State after:
no goals