Query budgets on possible outputs

Connects query budgets (Cslib.OracleComp.IsCostBounded) with the possible outputs (Cslib.OracleComp.support) of an oracle computation, and records the unit query budget of Cslib.ProbComp.unifFin.

Main results

• Cslib.OracleComp.IsCostBounded.bind_on_support: query cost budgets add under sequencing when the continuation is bounded on every possible output of the first computation.
• Cslib.ProbComp.isQueryBounded_unifFin: ProbComp.unifFin n makes one oracle query.

theorem Cslib.OracleComp.IsCostBounded.bind_on_support {ι : Type u} {spec : OracleSpec ι} {α β : Type v} {cost : ι → ℕ} {program : OracleComp spec α} {next : α → OracleComp spec β} {n m : ℕ} (h : IsCostBounded cost program n) (hnext : ∀ a ∈ program.support, IsCostBounded cost (next a) m) : IsCostBounded cost (program >>= next) (n + m)

Query cost budgets add under sequencing when the continuation is bounded on every possible first-stage output.

theorem Cslib.ProbComp.isQueryBounded_unifFin (n : ℕ) : OracleComp.IsQueryBounded (unifFin n) 1

unifFin n makes one oracle query.