Documentation

VCVio.EvalDist.Prod

Evaluation Distributions of Computations with Prod #

Lemmas about evalSPMF and support involving Prod, ported to generic [MonadLiftT m SPMF].

source
theorem probOutput_prod_mk_eq_probEvent {m : Type u → Type v} [MonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (x : α) (y : β) :
Pr[= (x, y) | mx] = probEvent mx fun (z : α × β) => z.1 = x ∧ z.2 = y
source
theorem probOutput_fst_map_eq_tsum {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (x : α) :
Pr[= x | Prod.fst <$> mx] = ∑' (y : β), Pr[= (x, y) | mx]
source
theorem probOutput_fst_map_eq_sum {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} [Fintype β] (mx : m (α × β)) (x : α) :
Pr[= x | Prod.fst <$> mx] = ∑ y : β, Pr[= (x, y) | mx]
source
theorem probOutput_snd_map_eq_tsum {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (y : β) :
Pr[= y | Prod.snd <$> mx] = ∑' (x : α), Pr[= (x, y) | mx]
source
theorem probOutput_snd_map_eq_sum {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} [Fintype α] (mx : m (α × β)) (y : β) :
Pr[= y | Prod.snd <$> mx] = ∑ x : α, Pr[= (x, y) | mx]
source
theorem probOutput_fst_map_eq_probEvent {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (x : α) :
Pr[= x | Prod.fst <$> mx] = probEvent mx fun (z : α × β) => z.1 = x
source
@[simp]
theorem probEvent_fst_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (p : α → Prop) :
probEvent (Prod.fst <$> mx) p = probEvent mx fun (x : α × β) => p x.1

Unlike probEvent_map this unfolds the function composition automatically.

source
theorem probOutput_snd_map_eq_probEvent {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (y : β) :
Pr[= y | Prod.snd <$> mx] = probEvent mx fun (z : α × β) => z.2 = y
source
@[simp]
theorem probEvent_snd_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m (α × β)) (p : β → Prop) :
probEvent (Prod.snd <$> mx) p = probEvent mx fun (y : α × β) => p y.2

Unlike probEvent_map this unfolds the function composition automatically.

source
@[simp]
theorem probEvent_fst_eq_snd {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx : m (α × α)) :
(probEvent mx fun (z : α × α) => z.1 = z.2) = ∑' (x : α), Pr[= (x, x) | mx]
source
@[simp]
theorem probOutput_seq_map_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (mx : m α) (my : m β) (z : α × β) :
Pr[= z | Prod.mk <$> mx <*> my] = Pr[= z.1 | mx] * Pr[= z.2 | my]
source
@[simp]
theorem support_seq_map_prod_mk {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (mx : m α) (my : m β) [MonadAttach m] [ExactMonadAttach m] :
support (Prod.mk <$> mx <*> my) = support mx ×ˢ support my
source
theorem finSupport_seq_map_prod_mk {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} (mx : m α) (my : m β) [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] :
finSupport (Prod.mk <$> mx <*> my) = (finSupport mx).product (finSupport my)
source
@[simp]
theorem probOutput_seq_map_prod_mk_map_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (z : γ × δ) :
Pr[= z | (fun (x1 : α) (x2 : β) => (f x1, g x2)) <$> mx <*> my] = Pr[= z.1 | f <$> mx] * Pr[= z.2 | g <$> my]
source
@[simp]
theorem probOutput_seq_map_prod_mk_map_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (z : γ × δ) :
Pr[= z | (fun (y : β) (x : α) => (f x, g y)) <$> my <*> mx] = Pr[= z.1 | f <$> mx] * Pr[= z.2 | g <$> my]
source
@[simp]
theorem probOutput_bind_map_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (z : γ × δ) :
Pr[= z | do let x ← mx (fun (x_1 : β) => (f x, g x_1)) <$> my] = Pr[= z.1 | f <$> mx] * Pr[= z.2 | g <$> my]
source
@[simp]
theorem probOutput_bind_map_prod_mk_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) (z : γ × δ) :
Pr[= z | do let y ← my (fun (x : α) => (f x, g y)) <$> mx] = Pr[= z.1 | f <$> mx] * Pr[= z.2 | g <$> my]
source
@[simp]
theorem support_seq_map_prod_mk_eq_sprod {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) [MonadAttach m] [ExactMonadAttach m] :
support ((fun (x1 : α) (x2 : β) => (f x1, g x2)) <$> mx <*> my) = (f '' support mx) ×ˢ (g '' support my)
source
theorem finSupport_seq_map_prod_mk_eq_product {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) [MonadAttach m] [ExactMonadAttach m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] [DecidableEq γ] [DecidableEq δ] :
finSupport ((fun (x1 : α) (x2 : β) => (f x1, g x2)) <$> mx <*> my) = (Finset.image f (finSupport mx)).product (Finset.image g (finSupport my))
source
theorem probOutput_bind_bind_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β γ δ : Type u} (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
theorem probOutput_bind_bind_prod_mk_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β γ δ : Type u} (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
theorem sq_probOutput_bind_le_probOutput_bind_prod {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} (source : m α) (kernel : α → m β) (y : β) :
Pr[= y | source >>= kernel] ^ 2 ≤ Pr[= (y, y) | do let x ← source let a ← kernel x let b ← kernel x pure (a, b)]

Two conditionally independent executions dominate the square of the corresponding single-execution output probability.

source
@[simp]
theorem probOutput_prod_mk_fst_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} [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] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] {α β : Type u} [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