triangleRemovalBound_mul_cube_lt — Mathlib

English

The product of triangleRemovalBound and a cube term is strictly less than 1 for ε>0.

Русский

Произведение triangleRemovalBound и куба больше нуля не превосходит 1.

LaTeX

$$triangleRemovalBound ε * ⌈4 / ε⌉^3 < 1$$

Lean4

theorem triangleRemovalBound_mul_cube_lt (hε : 0 < ε) : triangleRemovalBound ε * ⌈4 / ε⌉₊ ^ 3 < 1 := by
  calc
    _ ≤ (2 * ⌈4 / ε⌉₊ ^ 3 : ℝ)⁻¹ * ↑⌈4 / ε⌉₊ ^ 3 := by gcongr; exact min_le_left _ _
    _ = 2⁻¹ := by rw [mul_inv, inv_mul_cancel_right₀]; positivity
    _ < 1 := by norm_num

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