bi_min_div_two_lt_one

Mathlib.Computability.AkraBazzi.SumTransform

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

← MathLib Explorer

English

For the index achieving the minimum, b(min_bi b) / 2 < 1.

Русский

Для минимума индекса выполняется b(min_bi b) / 2 < 1.

LaTeX

$$$\dfrac{b(\min_bi b)}{2} < 1$$$

Lean4

theorem bi_min_div_two_lt_one : b (min_bi b) / 2 < 1 :=
  by
  have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
  calc
    b (min_bi b) / 2
    _ < b (min_bi b) := by aesop (add safe apply div_two_lt_of_pos)
    _ < 1 := R.b_lt_one _

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

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

Разделы

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

Аффилиация

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