def GeneralIterativeScheme.IsAnalyticalComplexity {Query : Type u} {Answer : Type v} (scheme : GeneralIterativeScheme Query Answer) (N : ℕ) : Prop

Definition 1.2.11: a natural number N is the analytical complexity of a general iterative scheme when N is the first oracle-call count at which the scheme reaches the chosen stopping criterion. If the scheme never reaches that stopping criterion, no such N exists.

@[simp]

theorem GeneralIterativeScheme.isAnalyticalComplexity_iff {Query : Type u} {Answer : Type v} {scheme : GeneralIterativeScheme Query Answer} {N : ℕ} : scheme.IsAnalyticalComplexity N ↔ scheme.HaltsAt N ∧ ∀ m < N, ¬scheme.HaltsAt m

Analytical complexity means that the scheme reaches the chosen stopping criterion at N and at no smaller oracle-call count.