Applied mathematics

TheoremAkra–Bazzi theorem#

The Akra-Bazzi theorem: T ∈ O(n^p (1 + ∑_u^n g(u) / u^{p+1}))

AkraBazziRecurrence.isBigO_asympBound.{u_1} {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ}
  {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) :
  T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b
Sources
MathlibAkraBazziRecurrence.isBigO_asympBound
Uses 11
Statement usesLogarithm
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Completeness · Convex subsets · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Holomorphic functions · Normed vector space over a normed field · Ordered ring · The Triangle Inequality

TheoremMyhill–Nerode theorem#

Myhill–Nerode theorem. A language is regular if and only if the set of left quotients is finite.

Language.isRegular_iff_finite_range_leftQuotient.{u} {α : Type u} {L : Language α} :
  L.IsRegular ↔ (Set.range L.leftQuotient).Finite
Sources
MathlibLanguage.isRegular_iff_finite_range_leftQuotient
Uses 2
Statement usesNatural number · Regular language

TheoremSmn theorem#

The \(S_n^m\) theorem: There is a computable function, namely Nat.Partrec.Code.curry, that takes a program and a ℕ n, and returns a new program using n as the first argument.

Nat.Partrec.Code.smn :
  ∃ f, Computable₂ f ∧ ∀ (c : Nat.Partrec.Code) (n x : ℕ), (f c n).eval x = c.eval (Nat.pair n x)
Sources
MathlibNat.Partrec.Code.smn
Uses 2
Statement usesIn terms of general recursive functions
Proof usesPrimitive recursive function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.