English
If p is a real number and n is a natural number with n ≤ p, then the map x ↦ x^p is ContDiff of order n on the real line.
Русский
Если p — действительное число и n ∈ ℕ с n ≤ p, тогда x ↦ x^p имеет дифференциацию порядка n на ℝ.
LaTeX
$$$\\forall p\\in\\mathbb{R},\\forall n\\in\\mathbb{N},\\ n\\le p\\Rightarrow ContDiff\\mathbb{R}\\,n\\ (x\\mapsto x^p).$$$
Lean4
theorem contDiff_rpow_const_of_le {p : ℝ} {n : ℕ} (h : ↑n ≤ p) : ContDiff ℝ n fun x : ℝ => x ^ p := by
induction n generalizing p with
| zero => exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)
| succ n ihn =>
have h1 : 1 ≤ p := le_trans (by simp) h
rw [Nat.cast_succ, ← le_sub_iff_add_le] at h
rw [show ((n + 1 : ℕ) : WithTop ℕ∞) = n + 1 from rfl, contDiff_succ_iff_deriv, deriv_rpow_const' h1]
simp only [WithTop.natCast_ne_top, analyticOn_univ, IsEmpty.forall_iff, true_and]
exact ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩
