summable_exp_nat_mul_of_ge — Mathlib

English

If c < 0 and f(n) ≥ n for all n, then ∑ exp(c f(n)) converges.

Русский

Пусть c < 0 и f(n) ≥ n для всех n. Тогда сумма ∑ e^{c f(n)} сходится.

LaTeX

$$$ c < 0, \ \forall n: \mathbb{N},\ n \le f(n) \implies \sum_{n=0}^{\infty} e^{c f(n)} \text{ converges}$$$

Lean4

theorem summable_exp_nat_mul_of_ge {c : ℝ} (hc : c < 0) {f : ℕ → ℝ} (hf : ∀ i, i ≤ f i) :
    Summable fun i : ℕ ↦ exp (c * f i) :=
  by
  refine (Real.summable_exp_nat_mul_iff.mpr hc).of_nonneg_of_le (fun _ ↦ by positivity) fun i ↦ ?_
  refine Real.exp_monotone ?_
  conv_rhs => rw [mul_comm]
  exact mul_le_mul_of_nonpos_left (hf i) hc.le

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