continuous_sumCoeffsExp — Mathlib

English

Let α be a finite index set. For real numbers a_i and positive b_i (i ∈ α), the function p ↦ ∑_{i∈α} a_i b_i^p is continuous on ℝ.

Русский

Пусть α — конечный индексный множество. Для вещественных коэффициентов a_i и положительных b_i (для всех i ∈ α) функция p ↦ ∑_{i∈α} a_i b_i^p непрерывна на ℝ.

LaTeX

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

Lean4

@[continuity, fun_prop]
theorem continuous_sumCoeffsExp : Continuous (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) :=
  by
  refine continuous_finset_sum Finset.univ fun i _ => Continuous.mul (by fun_prop) ?_
  exact Continuous.rpow continuous_const continuous_id (fun x => Or.inl (ne_of_gt (R.b_pos i)))

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