Output Distribution of Computations

This file defines HasEvalDist and related instances for OracleComp.

def OracleComp.supportWhen {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (o : QueryImpl spec Set) (mx : OracleComp spec α) : Set α

The possible outputs of mx when queries can output values in the specified sets. NOTE: currently proofs using this should reduce to simulateQ. A full API would be better

instance OracleComp.hasEvalSet {ι : Type u_1} {spec : OracleSpec ι} : HasEvalSet (OracleComp spec)

The support instance for OracleComp, defined as

theorem OracleComp.support_eq_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (mx : OracleComp spec α) : support mx = simulateQ (fun (x : spec.Domain) => Set.univ) mx

@[simp]

theorem OracleComp.support_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (q : OracleQuery spec α) : support (liftM q) = Set.range q.cont

theorem OracleComp.support_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : support (liftM (query t)) = Set.univ

theorem OracleComp.mem_support_liftM_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (q : OracleQuery spec α) (u : α) : u ∈ support (liftM q) ↔ ∃ (t : spec.Range q.input), q.cont t = u

theorem OracleComp.mem_support_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) (u : spec.Range t) : u ∈ support (liftM (query t))

theorem OracleComp.support_liftM_query {ι : Type u_1} {spec : OracleSpec ι} (t : spec.Domain) : support (liftM (query t)) = Set.univ

Alias of OracleComp.support_query.

instance OracleComp.instHasEvalFinset {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] : HasEvalFinset (OracleComp spec)

Finite version of support for when oracles have a finite set of possible outputs. NOTE: we can't use simulateQ because Finset lacks a Monad instance.

@[simp]

theorem OracleComp.finSupport_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [DecidableEq α] (q : OracleQuery spec α) : finSupport (liftM q) = Finset.image q.cont Finset.univ

theorem OracleComp.finSupport_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.DecidableEq] (t : spec.Domain) : finSupport (liftM (query t)) = Finset.univ

theorem OracleComp.mem_finSupport_liftM_iff {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [DecidableEq α] (q : OracleQuery spec α) (x : α) : x ∈ finSupport (liftM q) ↔ ∃ (t : spec.Range q.input), q.cont t = x

theorem OracleComp.mem_finSupport_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.DecidableEq] (t : spec.Domain) (u : spec.Range t) : u ∈ finSupport (liftM (query t))

noncomputable def OracleComp.evalDistWhen {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} (d : QueryImpl spec SPMF) (mx : OracleComp spec α) : SPMF α

The output distribution of mx when queries follow the specified distribution. NOTE: currently proofs using this should reduce to simulateQ. A full API would be better

noncomputable instance OracleComp.instHasEvalPMF {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] : HasEvalPMF (OracleComp spec)

Embed OracleComp into SPMF by mapping queries to uniform distributions over their range.

theorem OracleComp.evalDist_eq_simulateQ {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (mx : OracleComp spec α) : evalDist mx = liftM (simulateQ (fun (t : spec.Domain) => PMF.uniformOfFintype (spec.Range t)) mx)

@[simp]

theorem OracleComp.evalDist_liftM {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (q : OracleQuery spec α) : evalDist (liftM q) = liftM (PMF.map q.cont (PMF.uniformOfFintype (spec.Range q.input)))

@[simp]

theorem OracleComp.evalDist_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) : evalDist (liftM (query t)) = liftM (PMF.uniformOfFintype (spec.Range t))

@[simp]

theorem OracleComp.probOutput_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (q : OracleQuery spec α) (x : α) : Pr[=x | liftM q] = (∑' (u : spec.Range q.input), Pr[=x | pure (q.cont u)]) / ↑(Fintype.card (spec.Range q.input))

theorem OracleComp.probEvent_liftM_eq_div {ι : Type u_1} {spec : OracleSpec ι} {α : Type w} [spec.Fintype] [spec.Inhabited] (q : OracleQuery spec α) (p : α → Prop) : Pr[p | liftM q] = (∑' (u : spec.Range q.input), Pr[p | pure (q.cont u)]) / ↑(Fintype.card (spec.Range q.input))

@[simp]

theorem OracleComp.probOutput_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (u : spec.Range t) : Pr[=u | liftM (query t)] = (↑(Fintype.card (spec.Range t)))⁻¹

theorem OracleComp.probOutput_query_eq_div {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (u : spec.Range t) : Pr[=u | liftM (query t)] = 1 / ↑(Fintype.card (spec.Range t))

@[simp]

theorem OracleComp.probEvent_query {ι : Type u_1} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (p : spec.Range t → Prop) [DecidablePred p] : Pr[p | liftM (query t)] = ↑{x : spec.Range t | p x}.card / ↑(Fintype.card (spec.Range t))