differentiableOn_one_add_smoothingFn

Mathlib.Computability.AkraBazzi.SumTransform

URI: https://scilib.ai/kg/mathlib#AkraBazziRecurrence.differentiableOn_one_add_smoothingFn

← MathLib Explorer

English

For x > 1, the function x ↦ 1 + ε(x) is differentiable.

Русский

Для x > 1 функция x ↦ 1 + ε(x) дифференцируема.

LaTeX

$$$$x>1 \Rightarrow \frac{d}{dx}(1+\varepsilon(x)) = \varepsilon'(x) = -\frac{1}{x(\log x)^2}.$$$$

Lean4

theorem differentiableOn_one_add_smoothingFn : DifferentiableOn ℝ (fun z => 1 + ε z) (Set.Ioi 1) := fun _ hx =>
  (differentiableAt_one_add_smoothingFn hx).differentiableWithinAt

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru