Documentation

VCVio.EvalDist.Prod

Evaluation Distributions of Computations with Prod #

Lemmas about evalDist and support involving Prod, ported to generic [HasEvalSPMF m].

source
theorem probOutput_prod_mk_eq_probEvent {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α β : Type u} [DecidableEq α] [DecidableEq β] (mx : m (α × β)) (x : α) (y : β) :
Pr[=(x, y) | mx] = Pr[fun (z : α × β) => z.1 = x ∧ z.2 = y | mx]
source
@[simp]
theorem fst_map_prod_map {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ δ : Type u} (mx : m (α × β)) (f : α → γ) (g : β → δ) :
Prod.fst <$> Prod.map f g <$> mx = (f ∘ Prod.fst) <$> mx
source
@[simp]
theorem snd_map_prod_map {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ δ : Type u} (mx : m (α × β)) (f : α → γ) (g : β → δ) :
Prod.snd <$> Prod.map f g <$> mx = (g ∘ Prod.snd) <$> mx
source
@[simp]
theorem probOutput_fst_map_eq_tsum {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m (α × β)) (x : α) :
Pr[=x | Prod.fst <$> mx] = ∑' (y : β), Pr[=(x, y) | mx]
source
@[simp]
theorem probOutput_fst_map_eq_sum {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} [Fintype β] (mx : m (α × β)) (x : α) :
Pr[=x | Prod.fst <$> mx] = ∑ y : β, Pr[=(x, y) | mx]
source
@[simp]
theorem probOutput_snd_map_eq_tsum {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m (α × β)) (y : β) :
Pr[=y | Prod.snd <$> mx] = ∑' (x : α), Pr[=(x, y) | mx]
source
@[simp]
theorem probOutput_snd_map_eq_sum {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} [Fintype α] (mx : m (α × β)) (y : β) :
Pr[=y | Prod.snd <$> mx] = ∑ x : α, Pr[=(x, y) | mx]
source
theorem probEvent_fst_eq_snd {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} [DecidableEq α] (mx : m (α × α)) :
Pr[fun (z : α × α) => z.1 = z.2 | mx] = ∑' (x : α), Pr[=(x, x) | mx]
source
@[simp]
theorem probOutput_seq_map_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} [DecidableEq α] [DecidableEq β] (mx : m α) (my : m β) (x : α) (y : β) :
Pr[=(x, y) | Prod.mk <$> mx <*> my] = Pr[=x | mx] * Pr[=y | my]
source
theorem probOutput_seq_map_prod_map_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : Type u} [DecidableEq γ] [DecidableEq δ] (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (z : γ × δ) :
Pr[=z | (fun (a : α) (b : β) => (f a, g b)) <$> mx <*> my] = Pr[=z.1 | f <$> mx] * Pr[=z.2 | g <$> my]
source
theorem probOutput_bind_bind_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : Type u} [DecidableEq γ] [DecidableEq δ] (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (z : γ × δ) :
Pr[=z | do let x ← mx let y ← my pure (f x, g y)] = Pr[=z.1 | f <$> mx] * Pr[=z.2 | g <$> my]
source
@[simp]
theorem probOutput_bind_bind_prod_mk_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : Type u} [DecidableEq γ] [DecidableEq δ] (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (x : γ) (y : δ) :
Pr[=(x, y) | do let a ← mx let b ← my pure (f a, g b)] = Pr[=x | f <$> mx] * Pr[=y | g <$> my]
source
@[simp]
theorem probOutput_prod_mk_fst_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} [DecidableEq α] [DecidableEq β] (mx : m α) (y : β) (z : α × β) :
Pr[=z | (fun (x : α) => (x, y)) <$> mx] = if z.2 = y then Pr[=z.1 | mx] else 0
source
@[simp]
theorem probOutput_prod_mk_snd_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} [DecidableEq α] [DecidableEq β] (my : m β) (x : α) (z : α × β) :
Pr[=z | (fun (x_1 : β) => (x, x_1)) <$> my] = if z.1 = x then Pr[=z.2 | my] else 0