Theorem: Function.hasTemperateGrowth_pow (ForML/HasTemperateGrowth.lean)

State before:
n : ℕ
⊢ HasTemperateGrowth fun x => x ^ n
Tactic:
refine And.intro (contDiff_id.pow n) ?_
State after:
n : ℕ
⊢ ∀ (n_1 : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n_1 (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
n : ℕ
⊢ ∀ (n_1 : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n_1 (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro i
State after:
n i : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k

State before:
n i : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
use n - i, Nat.descFactorial n i
State after:
case h
n i : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)

State before:
case h
n i : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
intro x
State after:
case h
n i : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)

State before:
case h
n i : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ i (fun x => x ^ n) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv, iteratedDeriv_pow]
State after:
case h
n i : ℕ
x : ℝ
⊢ ‖(fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)

State before:
case h
n i : ℕ
x : ℝ
⊢ ‖(fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
rw [norm_mul, IsROrC.norm_natCast]
State after:
case h
n i : ℕ
x : ℝ
⊢ ↑(Nat.descFactorial n i) * ‖x ^ (n - i)‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)

State before:
case h
n i : ℕ
x : ℝ
⊢ ↑(Nat.descFactorial n i) * ‖x ^ (n - i)‖ ≤ ↑(Nat.descFactorial n i) * (1 + ‖x‖) ^ (n - i)
Tactic:
refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)
State after:
case h
n i : ℕ
x : ℝ
⊢ ‖x ^ (n - i)‖ ≤ (1 + ‖x‖) ^ (n - i)

State before:
case h
n i : ℕ
x : ℝ
⊢ ‖x ^ (n - i)‖ ≤ (1 + ‖x‖) ^ (n - i)
Tactic:
simp [pow_le_pow_left]
State after:
no goals