strictAnti_sumCoeffsExp — Mathlib

English

Let α be a finite index set with a_i > 0 and 0 < b_i < 1 for all i. Then the map p ↦ ∑_{i∈α} a_i b_i^p is strictly decreasing on ℝ.

Русский

Пусть для всех i ∈ α выполняются a_i > 0 и 0 < b_i < 1. Тогда отображение p ↦ ∑_{i∈α} a_i b_i^p строго убывает по p.

LaTeX

$$$\forall \alpha [\text{Finite}( \alpha )]\ ,\forall a,b : \alpha \to \mathbb{R},\ (\forall i, 0 < a_i)\ (0 < b_i < 1)\Rightarrow\ StrictAnti\bigl(p \mapsto \sum_{i \in \alpha} a_i b_i^p\bigr)$$$

Lean4

theorem strictAnti_sumCoeffsExp : StrictAnti (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) :=
  by
  rw [← Finset.sum_fn]
  refine Finset.sum_induction_nonempty _ _ (fun _ _ => StrictAnti.add) univ_nonempty ?terms
  refine fun i _ => StrictAnti.const_mul ?_ (R.a_pos i)
  exact Real.strictAnti_rpow_of_base_lt_one (R.b_pos i) (R.b_lt_one i)

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