English
For any integer m and any x with x ≠ 0 or m ≥ 0, the function t ↦ t^m has a strict derivative at x equal to m x^{m−1}.
Русский
Для любого целого m и точки x, где x ≠ 0 или m ≥ 0, производная функции t ↦ t^m в точке x равна m x^{m−1}.
LaTeX
$$$x \\neq 0 \\lor 0 \\le m \\Rightarrow \\operatorname{HasStrictDerivAt} (\\lambda t, t^m) ((m:\\\\mathbb{K}) \\cdot x^{m-1})\, x$$$
Lean4
theorem hasStrictDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
HasStrictDerivAt (fun x => x ^ m) ((m : 𝕜) * x ^ (m - 1)) x :=
by
have : ∀ m : ℤ, 0 < m → HasStrictDerivAt (· ^ m) ((m : 𝕜) * x ^ (m - 1)) x := fun m hm ↦
by
lift m to ℕ using hm.le
simp only [zpow_natCast, Int.cast_natCast]
convert hasStrictDerivAt_pow m x using 2
rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]
norm_cast at hm
rcases lt_trichotomy m 0 with (hm | hm | hm)
· have hx : x ≠ 0 := h.resolve_right hm.not_ge
have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm)) <;> [skip; exact zpow_ne_zero _ hx]
simp only [Function.comp_def, zpow_neg, inv_inv, smul_eq_mul] at this
convert this using 1
rw [sq, mul_inv, inv_inv, Int.cast_neg, neg_mul, neg_mul_neg, ← zpow_add₀ hx, mul_assoc, ← zpow_add₀ hx]
congr
abel
· simp only [hm, zpow_zero, Int.cast_zero, zero_mul, hasStrictDerivAt_const]
· exact this m hm
