Running a Computation Multiple Times

This file defines a function replicate oa n that runs the computation oa a total of n times, returning the result as a list of length n.

Note that while the executions are independent, they may no longer be after calling simulate.

theorem OracleComp.probFailure_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] : Pr[⊥ | replicate n oa] = 1 - (1 - Pr[⊥ | oa]) ^ n

@[simp]

theorem OracleComp.probOutput_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] (xs : List α) : Pr[= xs | replicate n oa] = if xs.length = n then (List.map (fun (x : α) => Pr[= x | oa]) xs).prod else 0

The probability of getting a list from replicate is the product of the chances of getting each of the individual elements.

theorem OracleComp.probEvent_replicate_of_probEvent_cons {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] (p : List α → Prop) (hp : p []) (q : α → Prop) (hq : ∀ (x : α) (xs : List α), p (x :: xs) ↔ q x ∧ p xs) : probEvent (replicate n oa) p = probEvent oa q ^ n

@[simp]

theorem OracleComp.support_replicate {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) : support (replicate n oa) = {xs : List α | xs.length = n ∧ ∀ x ∈ xs, x ∈ support oa}

Possible outputs of replicate n oa are lists of length n where each element in the list is a possible output of oa.

@[simp]

theorem OracleComp.mem_finSupport_replicate {ι : Type u_1} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) [spec.IsUniformSpec] [DecidableEq α] (xs : List α) : xs ∈ finSupport (replicate n oa) ↔ xs.length = n ∧ ∀ x ∈ xs, x ∈ finSupport oa

theorem OracleComp.probOutput_replicate_uniformSample {α : Type} [Fintype α] [SampleableType α] {n : ℕ} {xs : List α} (hlen : xs.length = n) : Pr[= xs | replicate n ($ᵗ α)] = (↑(Fintype.card α ^ n))⁻¹

SimulateQ distributivity

theorem OracleComp.simulateQ_replicate {ι : Type u_2} {spec : OracleSpec ι} {α : Type v} (oa : OracleComp spec α) (n : ℕ) {r : Type v → Type u_1} [Monad r] [LawfulMonad r] (impl : QueryImpl spec r) : simulateQ impl (replicate n oa) = List.mapM (fun (x : Unit) => simulateQ impl oa) (List.replicate n ())

simulateQ distributes over replicate: simulating a replicated computation equals running the simulated body n times via monadic recursion.

theorem OracleComp.support_ofFn_mapM_index {ι α : Type} {spec : OracleSpec ι} {L : ℕ} (f : Fin L → OracleComp spec α) {v : Vector α L} (hv : v ∈ support (Vector.mapM f (Vector.ofFn id))) (i : Fin L) : v[i] ∈ support (f i)

Index-extraction for (Vector.ofFn id).mapM over an OracleComp: any element in the support of the monadic mapM has each component lying in the support of the corresponding inner computation.