differentiableAt_smoothingFn — Mathlib

English

For x > 1, the map x ↦ ε(x) is differentiable, hence the map x ↦ x ↦ ε(x) is differentiable on (1, ∞).

Русский

Для x > 1 отображение ε(x) дифференцируемо, следовательно, отображение x ↦ ε(x) дифференцируемо на (1, ∞).

LaTeX

$$$$x>1 \Rightarrow \text{Differentiable}(\varepsilon)(x).$$$$

Lean4

@[aesop safe apply]
theorem differentiableAt_smoothingFn {x : ℝ} (hx : 1 < x) : DifferentiableAt ℝ ε x :=
  by
  have : log x ≠ 0 := Real.log_ne_zero_of_pos_of_ne_one (by positivity) (ne_of_gt hx)
  change DifferentiableAt ℝ (fun z => 1 / log z) x
  simp_rw [one_div]
  exact DifferentiableAt.inv (differentiableAt_log (by positivity)) this

Похожие утверждения