Denotational Semantics for Output Distributions

This file gives definitions for the output distribution or computations with uniform oracles. Given a computation oa : OracleComp spec α we define a distribution evalDist oa : PMF α expressing the probability of getting an output x : α if the oracles in spec were to respond uniformly to all queries.

We also define functions probOutput oa x and probEvent oa p for the probabilities of a specific output of of a specific predicate holding on the output respectively. We introduce notation [= x | oa] and [p | oa] for these defintions as well. λ α ↦ (α → β) The behavior of more complex oracles should first be implemented using OracleComp.simulate before applying these constructions.

These definitons are compatible with OracleComp.support and OracleComp.finSupport in the sense that values are in the support iff they have non-zero probability under evalDist.

We give many simp lemmas involving tsum a lower priority, as otherwise the simplifier will always choose them over versions involving sum (as they require DecidableEq or Fintype)

noncomputable def OracleComp.evalDistWhen {ι : Type u} {spec : OracleSpec ι} {α : Type w} (oa : OracleComp spec α) (query_dist : {α : Type w} → spec.OracleQuery α → OptionT PMF α) : OptionT PMF α

Equations

• oa.evalDistWhen query_dist = OracleComp.simulateQ { impl := fun {α : Type ?u.52} => query_dist } oa

noncomputable def OracleComp.evalDist {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : OptionT PMF α

Associate a probability mass function to a computation, where the probability is the odds of getting a given output assuming all oracles responded uniformly at random. Implemented by simulating queries in the PMF monad.

Equations

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

@[simp]

theorem OracleComp.evalDist_pure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (x : α) : (pure x).evalDist = pure x

@[simp]

theorem OracleComp.evalDist_liftM {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Nonempty α] [Fintype α] (q : spec.OracleQuery α) : (liftM q).evalDist = OptionT.lift (PMF.uniformOfFintype α)

@[simp]

theorem OracleComp.evalDist_query {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] (i : ι) (t : spec.domain i) : (liftM (OracleSpec.query i t)).evalDist = OptionT.lift (PMF.uniformOfFintype (spec.range i))

@[simp]

theorem OracleComp.evalDist_failure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] : failure.evalDist = failure

@[simp]

theorem OracleComp.evalDist_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) : (oa >>= ob).evalDist = oa.evalDist >>= evalDist ∘ ob

theorem OracleComp.evalDist_query_bind {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (i : ι) (t : spec.domain i) (ou : spec.range i → OracleComp spec α) : (liftM (OracleSpec.query i t) >>= ou).evalDist = OptionT.lift (PMF.uniformOfFintype (spec.range i)) >>= evalDist ∘ ou

@[simp]

theorem OracleComp.evalDist_map {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) : (f <$> oa).evalDist = f <$> oa.evalDist

@[simp]

theorem OracleComp.evalDist_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (og : OracleComp spec (α → β)) : (og <*> oa).evalDist = og.evalDist <*> oa.evalDist

@[simp]

theorem OracleComp.evalDist_eqRec {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (h : α = β) (oa : OracleComp spec α) : (h ▸ oa).evalDist = h ▸ oa.evalDist

@[simp]

theorem OracleComp.evalDist_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) : (if p then oa else oa').evalDist = if p then oa.evalDist else oa'.evalDist

@[simp]

theorem OracleComp.evalDist_coin : coin.evalDist = OptionT.lift (PMF.uniformOfFintype Bool)

@[simp]

theorem OracleComp.evalDist_uniformFin (n : ℕ) : evalDist $[0..n] = OptionT.lift (PMF.uniformOfFintype (Fin (n + 1)))

noncomputable def OracleComp.probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : ENNReal

[= x | oa] is the probability of getting the given output x from the computation oa, assuming all oracles respond uniformly at random.

Equations

• [=x|oa] = oa.evalDist.run (some x)

def OracleComp.«term[=_|_]» : Lean.ParserDescr

Equations

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

theorem OracleComp.probOutput_def {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|oa] = oa.evalDist.run (some x)

theorem OracleComp.evalDist_apply_some {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : oa.evalDist.run (some x) = [=x|oa]

@[simp]

theorem OracleComp.evalDist_comp_some {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : ⇑oa.evalDist.run ∘ some = fun (x : α) => [=x|oa]

noncomputable def OracleComp.probFailure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : ENNReal

[⊥ | oa] is the probability of the computation oa failing.

Equations

• [⊥|oa] = oa.evalDist.run none

def OracleComp.«term[⊥|_]» : Lean.ParserDescr

Equations

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

theorem OracleComp.probFailure_def {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [⊥|oa] = oa.evalDist.run none

theorem OracleComp.evalDist_apply_none {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : oa.evalDist.run none = [⊥|oa]

noncomputable def OracleComp.probEvent {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : ENNReal

[p | oa] is the probability of getting a result that satisfies a predicate p after running the computation oa, assuming all oracles respond uniformly at random.

Equations

• [p|oa] = oa.evalDist.run.toOuterMeasure (some '' {x : α | p x})

def OracleComp.«term[_|_]» : Lean.ParserDescr

Equations

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

theorem OracleComp.probEvent_def {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = oa.evalDist.run.toOuterMeasure (some '' {x : α | p x})

theorem OracleComp.probEvent_eq_tsum_indicator {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = ∑' (x : α), {x : α | p x}.indicator (fun (x : α) => [=x|oa]) x

theorem OracleComp.probEvent_eq_tsum_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : [p|oa] = ∑' (x : α), if p x then [=x|oa] else 0

More explicit form of probEvent_eq_tsum_indicator when the predicate p is decidable.

@[simp]

theorem OracleComp.probFailure_add_tsum_probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [⊥|oa] + ∑' (x : α), [=x|oa] = 1

@[simp]

theorem OracleComp.tsum_probOutput_add_probFailure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : ∑' (x : α), [=x|oa] + [⊥|oa] = 1

@[simp]

theorem OracleComp.probOutput_le_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {x : α} : [=x|oa] ≤ 1

@[simp]

theorem OracleComp.probFailure_le_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : [⊥|oa] ≤ 1

@[simp]

theorem OracleComp.tsum_probOutput_le_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : ∑' (x : α), [=x|oa] ≤ 1

@[simp]

theorem OracleComp.tsum_probOutput_ne_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : ∑' (x : α), [=x|oa] ≠ ⊤

@[simp]

theorem OracleComp.probEvent_le_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p : α → Prop} : [p|oa] ≤ 1

@[simp]

theorem OracleComp.probOutput_ne_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {x : α} : [=x|oa] ≠ ⊤

@[simp]

theorem OracleComp.probOutput_lt_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {x : α} : [=x|oa] < ⊤

@[simp]

theorem OracleComp.not_one_lt_probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {x : α} : ¬1 < [=x|oa]

@[simp]

theorem OracleComp.probEvent_ne_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p : α → Prop} : [p|oa] ≠ ⊤

@[simp]

theorem OracleComp.probEvent_lt_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p : α → Prop} : [p|oa] < ⊤

@[simp]

theorem OracleComp.not_one_lt_probEvent {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p : α → Prop} : ¬1 < [p|oa]

@[simp]

theorem OracleComp.probFailure_ne_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : [⊥|oa] ≠ ⊤

@[simp]

theorem OracleComp.probFailure_lt_top {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : [⊥|oa] < ⊤

@[simp]

theorem OracleComp.not_one_lt_probFailure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : ¬1 < [⊥|oa]

@[simp]

theorem OracleComp.one_le_probOutput_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {x : α} : 1 ≤ [=x|oa] ↔ [=x|oa] = 1

@[simp]

theorem OracleComp.one_le_probEvent_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p : α → Prop} : 1 ≤ [p|oa] ↔ [p|oa] = 1

@[simp]

theorem OracleComp.one_le_probFailure_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : 1 ≤ [⊥|oa] ↔ [⊥|oa] = 1

theorem OracleComp.tsum_probOutput_eq_sub {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : ∑' (x : α), [=x|oa] = 1 - [⊥|oa]

theorem OracleComp.sum_probOutput_eq_sub {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (oa : OracleComp spec α) : ∑ x : α, [=x|oa] = 1 - [⊥|oa]

theorem OracleComp.probFailure_eq_sub_tsum {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [⊥|oa] = 1 - ∑' (x : α), [=x|oa]

theorem OracleComp.probFailure_eq_sub_sum {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (oa : OracleComp spec α) : [⊥|oa] = 1 - ∑ x : α, [=x|oa]

theorem OracleComp.tsum_probOutput_eq_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (h : [⊥|oa] = 0) : ∑' (x : α), [=x|oa] = 1

theorem OracleComp.sum_probOutput_eq_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (oa : OracleComp spec α) (h : [⊥|oa] = 0) : ∑ x : α, [=x|oa] = 1

@[simp]

theorem OracleComp.mem_support_evalDist_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : some x ∈ oa.evalDist.run.support ↔ x ∈ oa.support

An output has non-zero probability iff it is in the support of the computation.

theorem OracleComp.mem_support_of_mem_support_evalDist {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : some x ∈ oa.evalDist.run.support → x ∈ oa.support

Alias of the forward direction of OracleComp.mem_support_evalDist_iff.

---

An output has non-zero probability iff it is in the support of the computation.

theorem OracleComp.mem_support_evalDist {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∈ oa.support → some x ∈ oa.evalDist.run.support

Alias of the reverse direction of OracleComp.mem_support_evalDist_iff.

---

An output has non-zero probability iff it is in the support of the computation.

@[simp]

theorem OracleComp.mem_support_evalDist_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (oa : OracleComp spec α) (x : α) : some x ∈ oa.evalDist.run.support ↔ x ∈ oa.finSupport

An output has non-zero probability iff it is in the finSupport of the computation.

theorem OracleComp.mem_finSupport_of_mem_support_evalDist {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (oa : OracleComp spec α) (x : α) : some x ∈ oa.evalDist.run.support → x ∈ oa.finSupport

Alias of the forward direction of OracleComp.mem_support_evalDist_iff'.

---

An output has non-zero probability iff it is in the finSupport of the computation.

theorem OracleComp.mem_support_evalDist' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] (oa : OracleComp spec α) (x : α) : x ∈ oa.finSupport → some x ∈ oa.evalDist.run.support

Alias of the reverse direction of OracleComp.mem_support_evalDist_iff'.

---

An output has non-zero probability iff it is in the finSupport of the computation.

@[simp]

theorem OracleComp.evalDist_apply_eq_zero_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : Option α) : oa.evalDist.run x = 0 ↔ Option.rec ([⊥|oa] = 0) (fun (x : α) => x ∉ oa.support) x

@[simp]

theorem OracleComp.evalDist_apply_eq_zero_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) [spec.DecidableEq] [DecidableEq α] (x : Option α) : oa.evalDist.run x = 0 ↔ Option.rec ([⊥|oa] = 0) (fun (x : α) => x ∉ oa.finSupport) x

theorem OracleComp.support_evalDist {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : oa.evalDist.run.support = if [⊥|oa] = 0 then some '' oa.support else insert none (some '' oa.support)

The support of evalDist oa is exactly support oa.

theorem OracleComp.support_evalDist' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) [spec.DecidableEq] [DecidableEq α] : oa.evalDist.run.support = ↑(if [⊥|oa] = 0 then Finset.image some oa.finSupport else insert none (Finset.image some oa.finSupport))

@[simp]

theorem OracleComp.probOutput_eq_zero_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|oa] = 0 ↔ x ∉ oa.support

theorem OracleComp.probOutput_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∉ oa.support → [=x|oa] = 0

Alias of the reverse direction of OracleComp.probOutput_eq_zero_iff.

theorem OracleComp.not_mem_support_of_probOutput_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|oa] = 0 → x ∉ oa.support

Alias of the forward direction of OracleComp.probOutput_eq_zero_iff.

@[simp]

theorem OracleComp.zero_eq_probOutput_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : 0 = [=x|oa] ↔ x ∉ oa.support

theorem OracleComp.zero_eq_probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∉ oa.support → 0 = [=x|oa]

Alias of the reverse direction of OracleComp.zero_eq_probOutput_iff.

@[simp]

theorem OracleComp.probOutput_eq_zero_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : [=x|oa] = 0 ↔ x ∉ oa.finSupport

theorem OracleComp.not_mem_fin_support_of_probOutput_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|oa] = 0 → x ∉ oa.support

Alias of the forward direction of OracleComp.probOutput_eq_zero_iff.

theorem OracleComp.probOutput_eq_zero' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∉ oa.support → [=x|oa] = 0

Alias of the reverse direction of OracleComp.probOutput_eq_zero_iff.

@[simp]

theorem OracleComp.zero_eq_probOutput_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : 0 = [=x|oa] ↔ x ∉ oa.finSupport

theorem OracleComp.zero_eq_probOutput' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : x ∉ oa.finSupport → 0 = [=x|oa]

Alias of the reverse direction of OracleComp.zero_eq_probOutput_iff'.

theorem OracleComp.probOutput_ne_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) (h : x ∈ oa.support) : [=x|oa] ≠ 0

theorem OracleComp.probOutput_ne_zero' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [DecidableEq α] (h : x ∈ oa.finSupport) : [=x|oa] ≠ 0

@[simp]

theorem OracleComp.probEvent_eq_zero_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = 0 ↔ ∀ x ∈ oa.support, ¬p x

theorem OracleComp.not_of_mem_support_of_probEvent_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = 0 → ∀ x ∈ oa.support, ¬p x

Alias of the forward direction of OracleComp.probEvent_eq_zero_iff.

theorem OracleComp.probEvent_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : (∀ x ∈ oa.support, ¬p x) → [p|oa] = 0

Alias of the reverse direction of OracleComp.probEvent_eq_zero_iff.

@[simp]

theorem OracleComp.zero_eq_probEvent_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : 0 = [p|oa] ↔ ∀ x ∈ oa.support, ¬p x

theorem OracleComp.zero_eq_probEvent {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : (∀ x ∈ oa.support, ¬p x) → 0 = [p|oa]

Alias of the reverse direction of OracleComp.zero_eq_probEvent_iff.

@[simp]

theorem OracleComp.probEvent_eq_zero_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : [p|oa] = 0 ↔ ∀ x ∈ oa.finSupport, ¬p x

theorem OracleComp.not_of_mem_finSupport_of_probEvent_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : [p|oa] = 0 → ∀ x ∈ oa.finSupport, ¬p x

Alias of the forward direction of OracleComp.probEvent_eq_zero_iff'.

theorem OracleComp.probEvent_eq_zero' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : (∀ x ∈ oa.finSupport, ¬p x) → [p|oa] = 0

Alias of the reverse direction of OracleComp.probEvent_eq_zero_iff'.

@[simp]

theorem OracleComp.zero_eq_probEvent_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : 0 = [p|oa] ↔ ∀ x ∈ oa.finSupport, ¬p x

theorem OracleComp.zero_eq_probEvent' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : (∀ x ∈ oa.finSupport, ¬p x) → 0 = [p|oa]

Alias of the reverse direction of OracleComp.zero_eq_probEvent_iff'.

@[simp]

theorem OracleComp.probOutput_pos_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : 0 < [=x|oa] ↔ x ∈ oa.support

theorem OracleComp.probOutput_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∈ oa.support → 0 < [=x|oa]

Alias of the reverse direction of OracleComp.probOutput_pos_iff.

theorem OracleComp.mem_support_of_probOutput_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : 0 < [=x|oa] → x ∈ oa.support

Alias of the forward direction of OracleComp.probOutput_pos_iff.

@[simp]

theorem OracleComp.probOutput_pos_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : 0 < [=x|oa] ↔ x ∈ oa.finSupport

theorem OracleComp.probOutput_pos' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : x ∈ oa.finSupport → 0 < [=x|oa]

Alias of the reverse direction of OracleComp.probOutput_pos_iff'.

theorem OracleComp.mem_finSupport_of_probOutput_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : 0 < [=x|oa] → x ∈ oa.finSupport

Alias of the forward direction of OracleComp.probOutput_pos_iff'.

@[simp]

theorem OracleComp.probEvent_pos_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : 0 < [p|oa] ↔ ∃ x ∈ oa.support, p x

theorem OracleComp.probEvent_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : (∃ x ∈ oa.support, p x) → 0 < [p|oa]

Alias of the reverse direction of OracleComp.probEvent_pos_iff.

theorem OracleComp.exists_mem_support_of_probEvent_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : 0 < [p|oa] → ∃ x ∈ oa.support, p x

Alias of the forward direction of OracleComp.probEvent_pos_iff.

@[simp]

theorem OracleComp.probEvent_pos_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : 0 < [p|oa] ↔ ∃ x ∈ oa.finSupport, p x

theorem OracleComp.probEvent_pos' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : (∃ x ∈ oa.finSupport, p x) → 0 < [p|oa]

Alias of the reverse direction of OracleComp.probEvent_pos_iff'.

theorem OracleComp.exists_mem_finSupport_of_probEvent_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : 0 < [p|oa] → ∃ x ∈ oa.finSupport, p x

Alias of the forward direction of OracleComp.probEvent_pos_iff'.

@[simp]

theorem OracleComp.probOutput_eq_one_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [=x|oa] = 1 ↔ [⊥|oa] = 0 ∧ oa.support = {x}

theorem OracleComp.probOutput_eq_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [⊥|oa] = 0 ∧ oa.support = {x} → [=x|oa] = 1

Alias of the reverse direction of OracleComp.probOutput_eq_one_iff.

@[simp]

theorem OracleComp.one_eq_probOutput_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : 1 = [=x|oa] ↔ [⊥|oa] = 0 ∧ oa.support = {x}

theorem OracleComp.one_eq_probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [⊥|oa] = 0 ∧ oa.support = {x} → 1 = [=x|oa]

Alias of the reverse direction of OracleComp.one_eq_probOutput_iff.

@[simp]

theorem OracleComp.probOutput_eq_one_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : [=x|oa] = 1 ↔ [⊥|oa] = 0 ∧ oa.finSupport = {x}

theorem OracleComp.probOutput_eq_one' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : [⊥|oa] = 0 ∧ oa.finSupport = {x} → [=x|oa] = 1

Alias of the reverse direction of OracleComp.probOutput_eq_one_iff'.

@[simp]

theorem OracleComp.one_eq_probOutput_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : 1 = [=x|oa] ↔ [⊥|oa] = 0 ∧ oa.finSupport = {x}

theorem OracleComp.one_eq_probOutput' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : [⊥|oa] = 0 ∧ oa.finSupport = {x} → 1 = [=x|oa]

Alias of the reverse direction of OracleComp.one_eq_probOutput_iff'.

@[simp]

theorem OracleComp.probEvent_eq_one_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = 1 ↔ [⊥|oa] = 0 ∧ ∀ x ∈ oa.support, p x

theorem OracleComp.probEvent_eq_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : ([⊥|oa] = 0 ∧ ∀ x ∈ oa.support, p x) → [p|oa] = 1

Alias of the reverse direction of OracleComp.probEvent_eq_one_iff.

@[simp]

theorem OracleComp.one_eq_probEvent_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : 1 = [p|oa] ↔ [⊥|oa] = 0 ∧ ∀ x ∈ oa.support, p x

theorem OracleComp.one_eq_probEvent {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : ([⊥|oa] = 0 ∧ ∀ x ∈ oa.support, p x) → [p|oa] = 1

Alias of the reverse direction of OracleComp.probEvent_eq_one_iff.

@[simp]

theorem OracleComp.probEvent_eq_one_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : [p|oa] = 1 ↔ [⊥|oa] = 0 ∧ ∀ x ∈ oa.finSupport, p x

theorem OracleComp.probEvent_eq_one' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : ([⊥|oa] = 0 ∧ ∀ x ∈ oa.finSupport, p x) → [p|oa] = 1

Alias of the reverse direction of OracleComp.probEvent_eq_one_iff'.

@[simp]

theorem OracleComp.one_eq_probEvent_iff' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : 1 = [p|oa] ↔ [⊥|oa] = 0 ∧ ∀ x ∈ oa.finSupport, p x

theorem OracleComp.one_eq_probEvent' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidableEq α] : ([⊥|oa] = 0 ∧ ∀ x ∈ oa.finSupport, p x) → 1 = [p|oa]

Alias of the reverse direction of OracleComp.one_eq_probEvent_iff'.

theorem OracleComp.mem_support_iff_probOutput_ne_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∈ oa.support ↔ [=x|oa] ≠ 0

theorem OracleComp.mem_finSupport_iff_probOutput_ne_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) [spec.DecidableEq] [DecidableEq α] : x ∈ oa.finSupport ↔ [=x|oa] ≠ 0

theorem OracleComp.mem_support_iff_probOutput_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∈ oa.support ↔ 0 < [=x|oa]

theorem OracleComp.not_mem_support_iff_probOutput_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : x ∉ oa.support ↔ [=x|oa] = 0

theorem OracleComp.probEvent_mono {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p q : α → Prop} (h : ∀ x ∈ oa.support, p x → q x) : [p|oa] ≤ [q|oa]

If p implies q on the support of a computation then it is more likely to happen.

theorem OracleComp.probEvent_mono' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p q : α → Prop} [spec.DecidableEq] [DecidableEq α] (h : ∀ x ∈ oa.finSupport, p x → q x) : [p|oa] ≤ [q|oa]

If p implies q on the finSupport of a computation then it is more likely to happen.

theorem OracleComp.probEvent_congr {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'} {α : Type w} [spec.FiniteRange] [spec'.FiniteRange] {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h1 : ∀ (x : α), p x ↔ q x) (h2 : oa.evalDist = oa'.evalDist) : [p|oa] = [q|oa']

theorem OracleComp.probEvent_ext {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p q : α → Prop} (h : ∀ x ∈ oa.support, p x ↔ q x) : [p|oa] = [q|oa]

theorem OracleComp.probEvent_ext' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {p q : α → Prop} [spec.DecidableEq] [DecidableEq α] (h : ∀ x ∈ oa.finSupport, p x ↔ q x) : [p|oa] = [q|oa]

@[simp]

theorem OracleComp.function_support_probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} : (Function.support fun (x : α) => [=x|oa]) = oa.support

theorem OracleComp.mem_support_iff_of_evalDist_eq {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'} {α : Type w} [spec.FiniteRange] [spec'.FiniteRange] {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h : oa.evalDist = oa'.evalDist) (x : α) : x ∈ oa.support ↔ x ∈ oa'.support

theorem OracleComp.mem_finSupport_iff_of_evalDist_eq {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'} {α : Type w} [spec.FiniteRange] [spec'.FiniteRange] [spec.DecidableEq] [spec'.DecidableEq] [DecidableEq α] {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h : oa.evalDist = oa'.evalDist) (x : α) : x ∈ oa.finSupport ↔ x ∈ oa'.finSupport

@[simp]

theorem OracleComp.probEvent_eq_eq_probOutput {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [fun (x_1 : α) => x_1 = x|oa] = [=x|oa]

@[simp]

theorem OracleComp.probEvent_eq_eq_probOutput' {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (x : α) : [fun (x_1 : α) => x = x_1|oa] = [=x|oa]

theorem OracleComp.probEvent_eq_tsum_subtype {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = ∑' (x : ↑{x : α | p x}), [=↑x|oa]

The probability of an event written as a sum over the set {x | p x} viewed as a subtype. This notably doesn't require decidability of the predicate p unlike many other lemmas.

theorem OracleComp.probEvent_eq_tsum_subtype_mem_support {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = ∑' (x : ↑{x : α | x ∈ oa.support ∧ p x}), [=↑x|oa]

Version probEvent_eq_tsum_subtype that preemptively filters out elements that aren't in the support, since they will have no mass contribution anyways. This can make some proofs simpler by handling things on the level of subtypes.

theorem OracleComp.probEvent_eq_tsum_subtype_support_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : [p|oa] = ∑' (x : ↑oa.support), if p ↑x then [=↑x|oa] else 0

theorem OracleComp.probEvent_eq_sum_fintype_indicator {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (oa : OracleComp spec α) (p : α → Prop) : [p|oa] = ∑ x : α, {x : α | p x}.indicator (fun (x : α) => [=x|oa]) x

theorem OracleComp.probEvent_eq_sum_fintype_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] [Fintype α] : [p|oa] = ∑ x : α, if p x then [=x|oa] else 0

theorem OracleComp.probEvent_eq_sum_filter_univ {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] [Fintype α] : [p|oa] = ∑ x ∈ Finset.filter p Finset.univ, [=x|oa]

theorem OracleComp.probEvent_eq_sum_filter_finSupport {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidablePred p] [DecidableEq α] : [p|oa] = ∑ x ∈ Finset.filter p oa.finSupport, [=x|oa]

theorem OracleComp.probEvent_eq_sum_finSupport_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : α → Prop) [spec.DecidableEq] [DecidablePred p] [DecidableEq α] : [p|oa] = ∑ x ∈ oa.finSupport, if p x then [=x|oa] else 0

theorem OracleComp.probOutput_congr {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'} {α : Type w} [spec.FiniteRange] [spec'.FiniteRange] {x y : α} {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h1 : x = y) (h2 : oa.evalDist = oa'.evalDist) : [=x|oa] = [=y|oa']

theorem OracleComp.probEvent_congr' {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'} {α : Type w} [spec.FiniteRange] [spec'.FiniteRange] {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h1 : ∀ x ∈ oa.support, x ∈ oa'.support → (p x ↔ q x)) (h2 : oa.evalDist = oa'.evalDist) : [p|oa] = [q|oa']

@[simp]

theorem OracleComp.probEvent_const {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (p : Prop) [Decidable p] : [fun (x : α) => p|oa] = if p then 1 - [⊥|oa] else 0

theorem OracleComp.probEvent_true {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [fun (x : α) => true = true|oa] = 1 - [⊥|oa]

theorem OracleComp.probEvent_false {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [fun (x : α) => false = true|oa] = 0

theorem OracleComp.probFailure_eq_sub_probEvent {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [⊥|oa] = 1 - [fun (x : α) => true = true|oa]

theorem OracleComp.evalDist_ext_probEvent {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'} {α : Type w} [spec.FiniteRange] [spec'.FiniteRange] {oa : OracleComp spec α} {oa' : OracleComp spec' α} (h : ∀ (x : α), [=x|oa] = [=x|oa']) : oa.evalDist.run = oa'.evalDist.run

@[simp]

theorem OracleComp.probOutput_pure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (x : α) [DecidableEq α] (y : α) : [=y|pure x] = if y = x then 1 else 0

@[simp]

theorem OracleComp.probFailure_pure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (x : α) : [⊥|pure x] = 0

theorem OracleComp.probOutput_pure_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {x y : α} (h : y ≠ x) : [=y|pure x] = 0

theorem OracleComp.probOutput_pure_eq_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {x y : α} (h : y = x) : [=y|pure x] = 1

@[simp]

theorem OracleComp.probOutput_pure_self {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (x : α) : [=x|pure x] = 1

@[simp]

theorem OracleComp.probOutput_pure_subsingleton {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Subsingleton α] (x y : α) : [=x|pure y] = 1

@[simp]

theorem OracleComp.probEvent_pure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (x : α) (p : α → Prop) [DecidablePred p] : [p|pure x] = if p x then 1 else 0

theorem OracleComp.probEvent_pure_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {p : α → Prop} {x : α} (h : ¬p x) : [p|pure x] = 0

theorem OracleComp.probEvent_pure_eq_one {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {p : α → Prop} {x : α} (h : p x) : [p|pure x] = 1

theorem OracleComp.probOutput_bind_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : [=y|oa >>= ob] = ∑' (x : α), [=x|oa] * [=y|ob x]

theorem OracleComp.probFailure_bind_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) : [⊥|oa >>= ob] = [⊥|oa] + ∑' (x : α), [=x|oa] * [⊥|ob x]

theorem OracleComp.probEvent_bind_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) (q : β → Prop) : [q|oa >>= ob] = ∑' (x : α), [=x|oa] * [q|ob x]

theorem OracleComp.probOutput_bind_eq_tsum_subtype {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) : [=y|oa >>= ob] = ∑' (x : ↑oa.support), [=↑x|oa] * [=y|ob ↑x]

Version of probOutput_bind_eq_tsum that sums only over the subtype given by the support of the first computation. This can be useful to avoid looking at edge cases that can't actually happen in practice after the first computation. A common example is if the first computation does some error handling to avoids returning malformed outputs.

theorem OracleComp.probEvent_bind_eq_tsum_subtype {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) (q : β → Prop) : [q|oa >>= ob] = ∑' (x : ↑oa.support), [=↑x|oa] * [q|ob ↑x]

theorem OracleComp.probOutput_bind_eq_sum_fintype {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [Fintype α] (y : β) : [=y|oa >>= ob] = ∑ x : α, [=x|oa] * [=y|ob x]

theorem OracleComp.probFailure_bind_eq_sum_fintype {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [Fintype α] : [⊥|oa >>= ob] = [⊥|oa] + ∑ x : α, [=x|oa] * [⊥|ob x]

theorem OracleComp.probEvent_bind_eq_sum_fintype {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [Fintype α] (q : β → Prop) : [q|oa >>= ob] = ∑ x : α, [=x|oa] * [q|ob x]

theorem OracleComp.probOutput_bind_eq_sum_finSupport {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [spec.DecidableEq] [DecidableEq α] (y : β) : [=y|oa >>= ob] = ∑ x ∈ oa.finSupport, [=x|oa] * [=y|ob x]

theorem OracleComp.probEvent_bind_eq_sum_finSupport {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [spec.DecidableEq] [DecidableEq α] (q : β → Prop) : [q|oa >>= ob] = ∑ x ∈ oa.finSupport, [=x|oa] * [q|ob x]

theorem OracleComp.probOutput_bind_of_const {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) (r : ENNReal) (h : ∀ (x : α), [=y|ob x] = r) : [=y|oa >>= ob] = (1 - [⊥|oa]) * r

theorem OracleComp.probFailure_bind_of_const {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (ob : α → OracleComp spec β) [Nonempty α] (r : ENNReal) (h : ∀ (x : α), [⊥|ob x] = r) : [⊥|oa >>= ob] = [⊥|oa] + r - [⊥|oa] * r

theorem OracleComp.probFailure_bind_eq_sub_mul {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {ob : α → OracleComp spec β} (r : ENNReal) (h : ∀ (x : α), [⊥|ob x] = r) : [⊥|oa >>= ob] = 1 - (1 - [⊥|oa]) * (1 - r)

theorem OracleComp.probFailure_bind_le_of_forall {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {s : ENNReal} (h' : [⊥|oa] = s) (ob : α → OracleComp spec β) {r : ENNReal} (hr : ∀ x ∈ oa.support, [⊥|ob x] ≤ r) : [⊥|oa >>= ob] ≤ s + (1 - s) * r

theorem OracleComp.probFailure_bind_le_of_forall' {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {s : ENNReal} (h' : [⊥|oa] = s) (ob : α → OracleComp spec β) {r : ENNReal} (hr : ∀ x ∈ oa.support, [⊥|ob x] ≤ r) : [⊥|oa >>= ob] ≤ s + r

Version of probFailure_bind_le_of_forall with the 1 - s factor ommited for convenience.

theorem OracleComp.probFailure_bind_le_of_le_of_neverFails {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] {oa : OracleComp spec α} (h' : oa.neverFails) {ob : α → OracleComp spec β} {r : ENNReal} (hr : ∀ x ∈ oa.support, [⊥|ob x] ≤ r) : [⊥|oa >>= ob] ≤ r

Version of probFailure_bind_le_of_forall when oa never fails.

theorem OracleComp.probFailure_bind_of_neverFails {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] {oa : OracleComp spec α} (h : oa.neverFails) (ob : α → OracleComp spec β) : [⊥|oa >>= ob] = ∑' (x : α), [=x|oa] * [⊥|ob x]

theorem OracleComp.mul_le_probEvent_bind {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] {oa : OracleComp spec α} {ob : α → OracleComp spec β} {p : α → Prop} {q : β → Prop} {r r' : ENNReal} (h : r ≤ [p|oa]) (h' : ∀ x ∈ oa.support, p x → r' ≤ [q|ob x]) : r * r' ≤ [q|oa >>= ob]

@[simp]

theorem OracleComp.probOutput_liftM {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (q : spec.OracleQuery α) (u : α) : [=u|liftM q] = (↑(Fintype.card α))⁻¹

theorem OracleComp.probOutput_query {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] (i : ι) (t : spec.domain i) (u : spec.range i) : [=u|liftM (OracleSpec.query i t)] = (↑(Fintype.card (spec.range i)))⁻¹

@[simp]

theorem OracleComp.probFailure_liftM {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (q : spec.OracleQuery α) : [⊥|liftM q] = 0

theorem OracleComp.probFailure_query {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] (i : ι) (t : spec.domain i) : [⊥|liftM (OracleSpec.query i t)] = 0

@[simp]

theorem OracleComp.probEvent_liftM_eq_mul_inv {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (q : spec.OracleQuery α) (p : α → Prop) [DecidablePred p] : [p|liftM q] = ↑(Finset.filter p Finset.univ).card * (↑(Fintype.card α))⁻¹

theorem OracleComp.probEvent_query_eq_mul_inv {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] (i : ι) (t : spec.domain i) (p : spec.range i → Prop) [DecidablePred p] : [p|liftM (OracleSpec.query i t)] = ↑(Finset.filter p Finset.univ).card * (↑(Fintype.card (spec.range i)))⁻¹

theorem OracleComp.probEvent_liftM_eq_inv_mul {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (q : spec.OracleQuery α) (p : α → Prop) [DecidablePred p] : [p|liftM q] = (↑(Fintype.card α))⁻¹ * ↑(Finset.filter p Finset.univ).card

theorem OracleComp.probEvent_query_eq_inv_mul {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] (i : ι) (t : spec.domain i) [spec.DecidableEq] (p : spec.range i → Prop) [DecidablePred p] : [p|liftM (OracleSpec.query i t)] = (↑(Fintype.card (spec.range i)))⁻¹ * ↑(Finset.filter p Finset.univ).card

theorem OracleComp.probEvent_liftM_eq_div {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] [Fintype α] (q : spec.OracleQuery α) (p : α → Prop) [DecidablePred p] : [p|liftM q] = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card α)

theorem OracleComp.probEvent_query_eq_div {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] (i : ι) (t : spec.domain i) [spec.DecidableEq] (p : spec.range i → Prop) [DecidablePred p] : [p|liftM (OracleSpec.query i t)] = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card (spec.range i))

@[simp]

theorem OracleComp.probOutput_failure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (x : α) : [=x|failure] = 0

@[simp]

theorem OracleComp.probFailure_failure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] : [⊥|failure] = 1

@[simp]

theorem OracleComp.probEvent_failure {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (p : α → Prop) : [p|failure] = 0

theorem OracleComp.probOutput_map_eq_tsum_subtype {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) (y : β) : [=y|f <$> oa] = ∑' (x : ↑{x : α | x ∈ oa.support ∧ y = f x}), [=↑x|oa]

Write the probability of an output after mapping the result of a computation as a sum over all outputs such that they map to the correct final output, using subtypes. This lemma notably doesn't require decidable equality on the final type, unlike most lemmas about probability when mapping a computation.

theorem OracleComp.probOutput_map_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) (y : β) : [=y|f <$> oa] = ∑' (x : α), [=x|oa] * [=y|pure (f x)]

theorem OracleComp.probOutput_map_eq_tsum_subtype_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) [DecidableEq β] (y : β) : [=y|f <$> oa] = ∑' (x : ↑oa.support), if y = f ↑x then [=↑x|oa] else 0

theorem OracleComp.probOutput_map_eq_tsum_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) [DecidableEq β] (y : β) : [=y|f <$> oa] = ∑' (x : α), if y = f x then [=x|oa] else 0

theorem OracleComp.probOutput_map_eq_sum_fintype_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) [Fintype α] [DecidableEq β] (y : β) : [=y|f <$> oa] = ∑ x : α, if y = f x then [=x|oa] else 0

theorem OracleComp.probOutput_map_eq_sum_finSupport_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) [spec.DecidableEq] [DecidableEq α] [DecidableEq β] (y : β) : [=y|f <$> oa] = ∑ x ∈ oa.finSupport, if y = f x then [=x|oa] else 0

theorem OracleComp.probOutput_map_eq_sum_filter_finSupport {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) [spec.DecidableEq] [DecidableEq α] [DecidableEq β] (y : β) : [=y|f <$> oa] = ∑ x ∈ {x ∈ oa.finSupport | y = f x}, [=x|oa]

@[simp]

theorem OracleComp.probFailure_map {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) : [⊥|f <$> oa] = [⊥|oa]

@[simp]

theorem OracleComp.probEvent_map {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) (q : β → Prop) : [q|f <$> oa] = [q ∘ f|oa]

theorem OracleComp.probEvent_comp {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) (q : β → Prop) : [q ∘ f|oa] = [q|f <$> oa]

theorem OracleComp.probOutput_map_eq_probOutput_inverse {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (f : α → β) (g : β → α) (hl : Function.LeftInverse f g) (hr : Function.RightInverse f g) (y : β) : [=y|f <$> oa] = [=g y|oa]

@[simp]

theorem OracleComp.probFailure_eq_zero_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : [⊥|oa] = 0 ↔ oa.neverFails

@[simp]

theorem OracleComp.probFailure_pos_iff {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (oa : OracleComp spec α) : 0 < [⊥|oa] ↔ ¬oa.neverFails

theorem OracleComp.noFailure_of_probFailure_eq_zero {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} (h : [⊥|oa] = 0) : oa.neverFails

theorem OracleComp.not_noFailure_of_probFailure_pos {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] {oa : OracleComp spec α} (h : 0 < [⊥|oa]) : ¬oa.neverFails

theorem OracleComp.probOutput_eqRec {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (h : α = β) (y : β) : [=y|h ▸ oa] = [=⋯ ▸ y|oa]

@[simp]

theorem OracleComp.probFailure_eqRec {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (h : α = β) : [⊥|h ▸ oa] = [⊥|oa]

theorem OracleComp.probEvent_eqRec {ι : Type u} {spec : OracleSpec ι} {α β : Type w} [spec.FiniteRange] (oa : OracleComp spec α) (h : α = β) (q : β → Prop) : [q|h ▸ oa] = [fun (x : α) => q (h ▸ x)|oa]

@[simp]

theorem OracleComp.probOutput_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) (x : α) : [=x|if p then oa else oa'] = if p then [=x|oa] else [=x|oa']

@[simp]

theorem OracleComp.probFailure_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) : [⊥|if p then oa else oa'] = if p then [⊥|oa] else [⊥|oa']

@[simp]

theorem OracleComp.probEvent_ite {ι : Type u} {spec : OracleSpec ι} {α : Type w} [spec.FiniteRange] (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) (q : α → Prop) : [q|if p then oa else oa'] = if p then [q|oa] else [q|oa']

@[simp]

theorem OracleComp.probOutput_coin (b : Bool) : [=b|coin] = 2⁻¹

theorem OracleComp.probEvent_coin_eq_sum_subtype (p : Bool → Prop) : [p|coin] = ∑' (x : ↑{x : Bool | p x}), 2⁻¹

@[simp]

theorem OracleComp.probEvent_coin (p : Bool → Prop) [DecidablePred p] : [p|coin] = if p true then if p false then 1 else 2⁻¹ else if p false then 2⁻¹ else 0

theorem OracleComp.probEvent_coin_eq_add (p : Bool → Prop) [DecidablePred p] : [p|coin] = (if p true then 2⁻¹ else 0) + if p false then 2⁻¹ else 0

@[simp]

theorem OracleComp.probOutput_uniformFin (n : ℕ) (x : Fin (n + 1)) : [=x|$[0..n]] = (↑n + 1)⁻¹

@[simp]

theorem OracleComp.probFailure_uniformFin (n : ℕ) : [⊥|$[0..n]] = 0

@[simp]

theorem OracleComp.probEvent_uniformFin (n : ℕ) (p : Fin (n + 1) → Prop) [DecidablePred p] : [p|$[0..n]] = ↑(Finset.filter p Finset.univ).card * (↑n + 1)⁻¹

def OracleComp.HoareTriple {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] {α β : Type v} (P : α → Prop) (comp : α → OracleComp spec β) (Q : β → Prop) (r : ENNReal) : Prop

If pre-condition P holds fox x then comp x satisfies post-contdition Q with probability at least r

Equations

• (⦃P⦄ comp ⦃Q⦄ r) = ∀ (x : α), P x → r ≤ [Q|comp x]

def OracleComp.«term⦃_⦄_⦃_⦄_» : Lean.ParserDescr

Equations

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

def OracleComp.HoareTriple.bind {ι : Type u} {spec : OracleSpec ι} [spec.FiniteRange] {α β γ : Type v} {P : α → Prop} {comp₁ : α → OracleComp spec β} {Q : β → Prop} {comp₂ : α → β → OracleComp spec γ} {R : γ → Prop} {r r' : ENNReal} (h1 : ⦃P⦄ comp₁ ⦃Q⦄ r) (h2 : ∀ (x : α), ⦃Q⦄ comp₂ x ⦃R⦄ r') : ⦃P⦄ fun (x : α) => comp₁ x >>= comp₂ x ⦃R⦄ r * r'

Equations

• ⋯ = ⋯