Upper and Lower Bounds for Query Complexity

Definitions of upper and lower bounds on the number of queries a program makes, quantified over oracles.

def Cslib.Query.UpperBound {α : Type w} {Q : Type u → Type v} {β : Type u} (prog : α → FreeM Q β) (size : α → ℕ) (bound : ℕ → ℕ) : Prop

Upper bound: for all oracles, inputs of size ≤ n make at most bound n queries.

Equations

• Cslib.Query.UpperBound prog size bound = ∀ (oracle : {ι : Type ?u.3} → Q ι → ι) (n : ℕ) (x : α), size x ≤ n → Cslib.FreeM.countQueries (fun {ι : Type ?u.3} => oracle) (prog x) ≤ bound n

def Cslib.Query.LowerBound {α : Type w} {Q : Type u → Type v} {β : Type u} (prog : α → FreeM Q β) (size : α → ℕ) (bound : ℕ → ℕ) : Prop

Lower bound: for every size n, there exists an input of size at most n and an oracle making the program perform ≥ bound n queries.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Query.UpperBound.of_pointwise {α : Type w} {Q : Type u → Type v} {β : Type u} {prog : α → FreeM Q β} {size : α → ℕ} {bound : ℕ → ℕ} (hmono : Monotone bound) (h : ∀ (oracle : {ι : Type u} → Q ι → ι) (x : α), FreeM.countQueries (fun {ι : Type u} => oracle) (prog x) ≤ bound (size x)) : UpperBound prog size bound

To prove an UpperBound with a monotone bound function, it suffices to bound the query count of each input by bound at its own size.

theorem Cslib.Query.LowerBound.le_upperBound {α : Type w} {Q : Type u → Type v} {β : Type u} {prog : α → FreeM Q β} {size : α → ℕ} {l u : ℕ → ℕ} (hl : LowerBound prog size l) (hu : UpperBound prog size u) (n : ℕ) : l n ≤ u n

A lower bound for a program never exceeds an upper bound for the same program and size function.