differentiableOn_one_sub_smoothingFn

Mathlib.Computability.AkraBazzi.SumTransform

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

← MathLib Explorer

English

The function 1 − ε is differentiable on the interval (1, ∞).

Русский

Функция 1 − ε дифференцируема на интервале (1, ∞).

LaTeX

$$$$\text{DifferentiableOn}(1-\varepsilon, (1,\infty)).$$$$

Lean4

theorem differentiableOn_one_sub_smoothingFn : DifferentiableOn ℝ (fun z => 1 - ε z) (Set.Ioi 1) := fun _ hx =>
  (differentiableAt_one_sub_smoothingFn hx).differentiableWithinAt

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

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

Разделы

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

Аффилиация

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