Expected query cost

OracleComp.expectedCost h cost program is the expected total cost of the calls of program when each call q is answered by an independent sample of h q and costs cost q. It is the average-case companion of the worst-case budget OracleComp.IsCostBounded: a budget of n bounds the expected cost by n (OracleComp.expectedCost_le_of_isCostBounded). Unlike a budget, the expected cost depends on the answers, so it is taken with respect to the distributions h, as in OracleComp.evalWith.

The expected cost is defined by recursion on the tree of calls. It is additive under sequencing, weighting the continuation by the output distribution of the first program (Wald's identity, OracleComp.expectedCost_bind), linear in the cost, and monotone in it. Replacing each call by a program over another interface turns the expected cost into the expected cost of the original calls, each priced at the expected cost of its replacement (OracleComp.expectedCost_interpret).

With a cost that is 1 on the reads of one position of an oracle and 0 elsewhere, the expected cost is the expected number of times a program reads that position, which is how the smoothness of a local decoder is measured.

Cslib.DataStructure.RandomizedSpec.expectedCost is the stateful counterpart, for calls to a randomized data structure whose answers depend on its state, with its own Wald identity (RandomizedSpec.expectedCost_bind) and budget bound (RandomizedSpec.expectedCost_le_of_isCostBounded).

Main definitions

• Cslib.OracleComp.expectedCost: the expected total cost of the calls.

Main results

• Cslib.OracleComp.expectedCost_bind: expected costs add under sequencing.
• Cslib.OracleComp.expectedCost_le_of_isCostBounded: a budget bounds the expected cost.
• Cslib.OracleComp.expectedCost_sum, Cslib.OracleComp.expectedCost_mono: linearity and monotonicity in the cost.
• Cslib.OracleComp.expectedCost_interpret: the expected cost of a program run through a handler.

noncomputable def Cslib.OracleComp.expectedCost {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) : OracleComp spec α → ENNReal

The expected total cost of the calls of program when each call q is answered by an independent sample of h q and costs cost q.

@[simp]

theorem Cslib.OracleComp.expectedCost_pure {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) (a : α) : expectedCost h cost (pure a) = 0

Returning a value makes no call.

theorem Cslib.OracleComp.expectedCost_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) (q : ι) (cont : spec q → OracleComp spec α) : expectedCost h cost (query q >>= cont) = cost q + ∑' (a : spec q), (h q) a * expectedCost h cost (cont a)

A call costs its cost, followed by the expected cost of the continuation at its answer.

@[simp]

theorem Cslib.OracleComp.expectedCost_query {ι : Type u} {spec : OracleSpec ι} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) (q : ι) : expectedCost h cost (query q) = cost q

A single call costs its cost.

theorem Cslib.OracleComp.expectedCost_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) (program : OracleComp spec α) (next : α → OracleComp spec β) : expectedCost h cost (program >>= next) = expectedCost h cost program + ∑' (a : α), (evalWith h program) a * expectedCost h cost (next a)

Wald's identity for oracle programs: the expected cost of a sequence is the expected cost of the first program plus the expected cost of the continuation at its result.

@[simp]

theorem Cslib.OracleComp.expectedCost_map {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) (f : α → β) (program : OracleComp spec α) : expectedCost h cost (f <$> program) = expectedCost h cost program

Postprocessing the result makes no call.

theorem Cslib.OracleComp.expectedCost_le_of_isCostBounded {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) {cost : ι → ℕ} {program : OracleComp spec α} {n : ℕ} (hb : IsCostBounded cost program n) : expectedCost h (fun (q : ι) => ↑(cost q)) program ≤ ↑n

A budget bounds the expected cost, whatever the distributions of the answers.

theorem Cslib.OracleComp.expectedCost_eq_zero_of_isCostBounded {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (cost : ι → ENNReal) {cost' : ι → ℕ} {program : OracleComp spec α} (hb : IsCostBounded cost' program 0) (hcost : ∀ (q : ι), cost' q = 0 → cost q = 0) : expectedCost h cost program = 0

A program whose calls all cost nothing under one cost has zero expected cost under every cost that vanishes on the same calls.

@[simp]

theorem Cslib.OracleComp.expectedCost_zero {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (program : OracleComp spec α) : expectedCost h 0 program = 0

Calls that cost nothing have zero expected cost.

theorem Cslib.OracleComp.expectedCost_add {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) (cost cost' : ι → ENNReal) (program : OracleComp spec α) : expectedCost h (cost + cost') program = expectedCost h cost program + expectedCost h cost' program

The expected cost is additive in the cost.

theorem Cslib.OracleComp.expectedCost_sum {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) {κ : Type u_1} (s : Finset κ) (cost : κ → ι → ENNReal) (program : OracleComp spec α) : expectedCost h (∑ k ∈ s, cost k) program = ∑ k ∈ s, expectedCost h (cost k) program

The expected cost of a finite sum of costs is the sum of the expected costs.

theorem Cslib.OracleComp.expectedCost_mono {ι : Type u} {spec : OracleSpec ι} {α : Type v} (h : (q : ι) → PMF (spec q)) {cost cost' : ι → ENNReal} (hcost : cost ≤ cost') (program : OracleComp spec α) : expectedCost h cost program ≤ expectedCost h cost' program

The expected cost is monotone in the cost.

theorem Cslib.OracleComp.expectedCost_interpret {ι : Type u} {spec : OracleSpec ι} {α : Type v} {κ : Type u} {target : OracleSpec κ} (handler : (q : ι) → OracleComp target (spec q)) (h : (q : κ) → PMF (target q)) (cost : κ → ENNReal) (program : OracleComp spec α) : expectedCost h cost (interpret handler program) = expectedCost (fun (q : ι) => evalWith h (handler q)) (fun (q : ι) => expectedCost h cost (handler q)) program

The expected cost of a program whose calls were replaced by programs over another interface is the expected cost of the original calls, each priced at the expected cost of its replacement and answered with the distribution of its replacement.

@[simp]

theorem Cslib.ProbOracleComp.expectedCost_sample {Query α : Type} {spec : Query → Type} (h : (q : ℕ ⊕ Query) → PMF (probOracleSpec spec q)) (cost : Query → ENNReal) (program : ProbComp α) : OracleComp.expectedCost h (Sum.elim 0 cost) (sample program) = 0

Private coins are free: a closed sampler has zero expected cost under every cost of the external queries.