one_sub_div_pow_le_exp_neg — Mathlib

English

For n ∈ ℕ and t ∈ ℝ with t ≤ n, (1 − t/n)^n ≤ exp(−t).

Русский

Для n ∈ ℕ и t ∈ ℝ с t ≤ n, (1 − t/n)^n ≤ exp(−t).

LaTeX

$$$\\big(1 - \\frac{t}{n}\\big)^{n} \\leq \\exp(-t).$$$

Lean4

theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t / n) ^ n ≤ exp (-t) :=
  by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
    rwa [Nat.cast_zero] at ht'
  calc
    (1 - t / n) ^ n ≤ rexp (-(t / n)) ^ n := by
      gcongr
      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
      · exact one_sub_le_exp_neg _
    _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity

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