Theorems · Definition · computer science
AkraBazziRecurrence.GrowsPolynomially
(ℝ → ℝ) → Prop
The growth condition that the function g must satisfy for the Akra-Bazzi theorem to apply.
It roughly states that c₁ g(n) ≤ g(u) ≤ c₂ g(n), for u between b * n and n, for any
constant b ∈ (0, 1).
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Filter.Eventuallyproof · cited by 3,134
- Filter.atTopproof · cited by 2,405
- Set.Iccproof · cited by 1,702
- Set.Iooproof · cited by 1,214
Cited by46
Results whose statement or proof uses this declaration.
- AkraBazziRecurrence.growsPolynomially_idstatement · cited by 5
- AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonposstatement and proof · cited by 4
- AkraBazziRecurrence.GrowsPolynomially.negstatement and proof · cited by 4
- AkraBazziRecurrence.GrowsPolynomially.absstatement and proof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEqstatement and proof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEqstatement and proof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.invstatement and proof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.powstatement and proof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.rpowstatement and proof · cited by 3
- AkraBazziRecurrence.g_grows_polystatement · cited by 2
- AkraBazziRecurrence.growsPolynomially_conststatement · cited by 2
- AkraBazziRecurrence.growsPolynomially_logstatement · cited by 2