Theorems · Theorem · computer science

AkraBazziRecurrence.a_pos

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (i : α), 0 < a i

The coefficients a i are positive.

Defined in

Mathlib.Computability.AkraBazzi.SumTransform

Cited by

5 results in Mathlib

Foundations

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

Assumes

FintypeNonempty