eulerMascheroniConstant_lt_two_thirds

Mathlib.NumberTheory.Harmonic.EulerMascheroni

URI: https://scilib.ai/kg/mathlib#Real.eulerMascheroniConstant_lt_two_thirds

← MathLib Explorer

English

The Euler–Mascheroni constant γ is less than two thirds.

Русский

Пусть γ обозначает константу Эйлера–Машчерони; γ < 2/3.

LaTeX

$$\gamma < \tfrac{2}{3}$$

Lean4

/-- Upper bound for `γ`. (The true value is about 0.57.) -/
theorem eulerMascheroniConstant_lt_two_thirds : eulerMascheroniConstant < 2 / 3 :=
  (eulerMascheroniConstant_lt_eulerMascheroniSeq' _).trans eulerMascheroniSeq'_six_lt_two_thirds

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

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

Разделы

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

Аффилиация

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