one_mem_range_sumCoeffsExp — Mathlib

English

The exponent p associated with an Akra–Bazzi recurrence is characterized as the unique real number solving ∑ a_i b_i^p = 1.

Русский

Порядковый показатель p для рекуррентной формулы Ака–Баззи определяется как уникальное действительное число, удовлетворяющее равенству ∑ a_i b_i^p = 1.

LaTeX

$$$\text{p is the unique real number such that } \sum_{i \in \alpha} a_i b_i^p = 1$$$

Lean4

theorem one_mem_range_sumCoeffsExp : 1 ∈ Set.range (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) :=
  by
  refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_one
  case le_one => exact R.tendsto_zero_sumCoeffsExp.eventually_le_const zero_lt_one |>.exists
  case ge_one => exact R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists

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