normThreshold_strictMono

Mathlib.Probability.Distributions.Fernique

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Fernique.normThreshold_strictMono

← MathLib Explorer

English

For ha_pos > 0, the function n ↦ normThreshold(a,n) is strictly increasing in n (i.e., StrictMono).

Русский

При ha_pos > 0 функция n ↦ normThreshold(a,n) строго возрастает по n.

LaTeX

$$StrictMono(\\n\\t{\\mathsf{normThreshold}}(a))$$

Lean4

theorem normThreshold_strictMono (ha_pos : 0 < a) : StrictMono (normThreshold a) :=
  arithGeom_strictMono Real.one_lt_sqrt_two (lt_normThreshold_zero ha_pos)

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

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

Разделы

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

Аффилиация

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