eventually_atTop_exists_int_between

English

A composition bound via eventual monotonicity gives a certain inequality relating linearGrowthInf and products.

Русский

Через eventually монотонность композиции получается неравенство между линейным ростом и произведениями.

LaTeX

$$$(\text{hu} : 0 \leqslantᵇ u) \Rightarrow (linearGrowthInf (u) \cdot linearGrowthInf v) \le linearGrowthInf (u \circ v)$$$

Lean4

theorem eventually_atTop_exists_int_between {a b : ℝ} (h : a < b) : ∀ᶠ x : ℝ in atTop, ∃ n : ℤ, a * x ≤ n ∧ n ≤ b * x :=
  by
  refine (eventually_ge_atTop (b - a)⁻¹).mono fun x ab_x ↦ ?_
  rw [inv_le_iff_one_le_mul₀ (sub_pos_of_lt h), mul_comm, sub_mul, le_sub_iff_add_le'] at ab_x
  obtain ⟨n, n_bx, hn⟩ := (b * x).exists_floor
  refine ⟨n, ?_, n_bx⟩
  specialize hn (n + 1)
  simp only [Int.cast_add, Int.cast_one, add_le_iff_nonpos_right, Int.reduceLE, imp_false, not_le] at hn
  exact le_of_add_le_add_right (ab_x.trans hn.le)

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