Theorems · Theorem · computer science

AkraBazziRecurrence.injective_sumCoeffsExp

∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), Function.Injective fun p => ∑ i, a i * b i ^ p

The function x ↦ ∑ a_i b_i^x is injective. This implies the uniqueness of p.

Defined in

Mathlib.Computability.AkraBazzi.SumTransform

Cited by

0 results in Mathlib

Foundations

Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeNonempty