English
For any n and any x, log is ContDiffAt at x if and only if x ≠ 0.
Русский
Для любого n и любой точки x логарифм имеет непрерывно-дифференцируемость на точке x тогда и только тогда, когда x ≠ 0.
LaTeX
$$ContDiffAt ℝ n log x ⇔ x ≠ 0$$
Lean4
theorem contDiffAt_log {n : WithTop ℕ∞} {x : ℝ} : ContDiffAt ℝ n log x ↔ x ≠ 0 :=
by
refine ⟨fun h ↦ continuousAt_log_iff.1 h.continuousAt, fun hx ↦ ?_⟩
have A y (hy : 0 < y) : ContDiffAt ℝ n log y :=
by
apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)
· convert hasDerivAt_exp (log y)
rw [exp_log hy]
· exact analyticAt_rexp.contDiffAt
rcases hx.lt_or_gt with hx | hx
· have : ContDiffAt ℝ n (log ∘ (fun y ↦ -y)) x :=
by
apply ContDiffAt.comp
apply A _ (Left.neg_pos_iff.mpr hx)
apply contDiffAt_id.neg
convert this
ext x
simp
· exact A x hx
