strictMonoOn_one_sub_smoothingFn

Mathlib.Computability.AkraBazzi.SumTransform

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

← MathLib Explorer

English

The map x ↦ 1 − ε(x) is strictly increasing on (1, ∞).

Русский

Отображение x ↦ 1 − ε(x) строго возрастает на (1, ∞).

LaTeX

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

Lean4

theorem strictMonoOn_one_sub_smoothingFn : StrictMonoOn (fun (x : ℝ) => (1 : ℝ) - ε x) (Set.Ioi 1) :=
  by
  simp_rw [sub_eq_add_neg]
  exact StrictMonoOn.const_add (StrictAntiOn.neg <| strictAntiOn_smoothingFn) 1

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

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

Разделы

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

Аффилиация

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