Documentation

VCVio.OracleComp.DistSemantics.Prod

Lemmas About the Distribution Semantics Involving Prod #

This file collects various lemmas about computations involving Prod.

NOTE: A lot of these could be implemented for more general functors/monads to mathlib TODO: Variables

source
theorem OracleComp.probOutput_prod_mk_eq_probEvent {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] [DecidableEq α] [DecidableEq β] (oa : OracleComp spec (α × β)) (x : α) (y : β) :
[=(x, y)|oa] = [fun (z : α × β) => z.1 = x ∧ z.2 = y|oa]
source
@[simp]
theorem OracleComp.fst_map_prod_map {ι : Type u} {spec : OracleSpec ι} {α β γ δ : Type v} (oa : OracleComp spec (α × β)) (f : α → γ) (g : β → δ) :
Prod.fst <$> Prod.map f g <$> oa = (f ∘ Prod.fst) <$> oa
source
@[simp]
theorem OracleComp.snd_map_prod_map {ι : Type u} {spec : OracleSpec ι} {α β γ δ : Type v} (oa : OracleComp spec (α × β)) (f : α → γ) (g : β → δ) :
Prod.snd <$> Prod.map f g <$> oa = (g ∘ Prod.snd) <$> oa
source
@[simp]
theorem OracleComp.probOutput_fst_map_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec (α × β)) (x : α) :
[=x|Prod.fst <$> oa] = ∑' (y : β), [=(x, y)|oa]
source
@[simp]
theorem OracleComp.probOutput_fst_map_eq_sum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] [Fintype β] (oa : OracleComp spec (α × β)) (x : α) :
[=x|Prod.fst <$> oa] = ∑ y : β, [=(x, y)|oa]
source
@[simp]
theorem OracleComp.probOutput_snd_map_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec (α × β)) (y : β) :
[=y|Prod.snd <$> oa] = ∑' (x : α), [=(x, y)|oa]
source
@[simp]
theorem OracleComp.probOutput_snd_map_eq_sum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] [Fintype α] (oa : OracleComp spec (α × β)) (y : β) :
[=y|Prod.snd <$> oa] = ∑ x : α, [=(x, y)|oa]
source
@[simp]
theorem OracleComp.probOutput_seq_map_prod_mk_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (x : α) (y : β) :
[=(x, y)|Prod.mk <$> oa <*> ob] = [=x|oa] * [=y|ob]
source
theorem OracleComp.probOutput_seq_map_prod_mk_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (x : α) (y : β) :
[=(x, y)|(fun (x : β) (y : α) => (y, x)) <$> ob <*> oa] = [=x|oa] * [=y|ob]
source
@[simp]
theorem OracleComp.probEvent_seq_map_prod_mk_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (p : α → Prop) (q : β → Prop) :
[fun (z : α × β) => p z.1 ∧ q z.2|Prod.mk <$> oa <*> ob] = [p|oa] * [q|ob]
source
theorem OracleComp.probEvent_seq_map_prod_mk_eq_mul' {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (p : α → Prop) (q : β → Prop) :
[fun (z : α × β) => p z.1 ∧ q z.2|(fun (x : β) (y : α) => (y, x)) <$> ob <*> oa] = [p|oa] * [q|ob]
source
@[simp]
theorem OracleComp.fst_map_prod_mk_of_subsingleton {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [Subsingleton β] (oa : OracleComp spec α) (y : β) :
Prod.fst <$> (fun (x : α) => (x, y)) <$> oa = oa
source
@[simp]
theorem OracleComp.snd_map_prod_mk_of_subsingleton {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [Subsingleton α] (ob : OracleComp spec β) (x : α) :
Prod.snd <$> (fun (x_1 : β) => (x, x_1)) <$> ob = ob
source
theorem OracleComp.probEvent_fst_eq_snd {ι : Type u} {spec : OracleSpec ι} {α : Type v} [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec (α × α)) :
[fun (z : α × α) => z.1 = z.2|oa] = ∑' (x : α), [=(x, x)|oa]