tendsto_zero_sumCoeffsExp — Mathlib

English

Let α be finite with a_i ∈ ℝ and 0 < b_i < 1. Then p ↦ ∑ a_i b_i^p tends to 0 as p → +∞.

Русский

Пусть α конечно, и для всех i выполнены a_i ∈ ℝ и 0 < b_i < 1. Тогда сумма ∑ a_i b_i^p стремится к 0 при p → +∞.

LaTeX

$$$\forall \alpha [\text{Finite}( \alpha )],\forall a,b : \alpha \to \mathbb{R},\ (\forall i, 0 < b_i < 1)\Rightarrow\lim_{p \to +\infty} \sum_{i \in \alpha} a_i b_i^p = 0$$$

Lean4

theorem tendsto_zero_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) atTop (𝓝 0) :=
  by
  have h₁ : Finset.univ.sum (fun _ : α => (0 : ℝ)) = 0 := by simp
  rw [← h₁]
  refine tendsto_finset_sum (univ : Finset α) (fun i _ => ?_)
  rw [← mul_zero (a i)]
  refine Tendsto.mul (by simp) <| tendsto_rpow_atTop_of_base_lt_one _ ?_ (R.b_lt_one i)
  have := R.b_pos i
  linarith

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