div_lt_floor — Mathlib

English

If x ∈ ℝ satisfies 2 / (1 − 2 / e) ≤ x, then x / e < ⌊x / 2⌋.

Русский

Пусть x ∈ ℝ и выполняется 2 / (1 − 2 / e) ≤ x. Тогда x / e < ⌊x / 2⌋.

LaTeX

$$$$ \\frac{x}{e} < \\Big\\lfloor \\frac{x}{2} \\Big\\rfloor \quad\\text{for}\\quad x \\ge \\frac{2}{1 - \\frac{2}{e}}. $$$$

Lean4

theorem div_lt_floor {x : ℝ} (hx : 2 / (1 - 2 / exp 1) ≤ x) : x / exp 1 < (⌊x / 2⌋₊ : ℝ) :=
  by
  apply lt_of_le_of_lt _ (sub_one_lt_floor _)
  have : 0 < 1 - 2 / exp 1 := by
    rw [sub_pos, div_lt_one (exp_pos _)]
    exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9
  rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ← div_eq_mul_one_div,
    mul_div_assoc', one_le_div, ← div_le_iff₀ this]
  · exact zero_lt_two
  · exact two_ne_zero

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