hundred_lt_pow_initialBound_mul — Mathlib

English

For ε > 0, we have 100 < 4^{initialBound(ε, l)} · ε^5.

Русский

При ε > 0 выполняется 100 < 4^{initialBound(ε, l)} · ε^5.

LaTeX

$$$100 < 4^{\mathrm{initialBound}(\varepsilon, l)} \cdot \varepsilon^{5}$$$

Lean4

theorem hundred_lt_pow_initialBound_mul {ε : ℝ} (hε : 0 < ε) (l : ℕ) : 100 < ↑4 ^ initialBound ε l * ε ^ 5 :=
  by
  rw [← rpow_natCast 4, ← div_lt_iff₀ (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ← div_lt_iff₀, initialBound,
    Nat.cast_max, Nat.cast_max]
  · push_cast
    exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)
  · exact log_pos (by simp)
  · exact div_pos (by simp) (pow_pos hε 5)

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