English
The map p ↦ ∑_{i∈α} a_i b_i^p is strictly monotone (hence injective) under suitable positivity conditions.
Русский
Отображение p ↦ ∑_{i∈α} a_i b_i^p при определённых условиях на знаки коэффициентов является строгомонотонным (значит инъективным).
LaTeX
$$$\text{Injective}\Bigl(p \mapsto \sum_{i \in \alpha} a_i b_i^p\Bigr)$, under appropriate positivity constraints on $a_i$ and $b_i$ with $b_i>0$.$$
Lean4
theorem tendsto_atTop_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) atBot atTop :=
by
have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
Tendsto.const_mul_atTop (R.a_pos (max_bi b)) <|
tendsto_rpow_atBot_of_base_lt_one _ (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _)
refine tendsto_atTop_mono (fun p => ?_) h₁
refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)
have h₁ : 0 < a i := R.a_pos i
have h₂ : 0 < b i := R.b_pos i
positivity
