Evaluation Distributions of Computations with Prod

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

theorem probOutput_prod_mk_eq_probEvent {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α β : Type u} (mx : m (α × β)) (x : α) (y : β) : Pr[= (x, y) | mx] = probEvent mx fun (z : α × β) => z.1 = x ∧ z.2 = y

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]

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]

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]

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]

theorem probOutput_fst_map_eq_probEvent {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m (α × β)) (x : α) : Pr[= x | Prod.fst <$> mx] = probEvent mx fun (z : α × β) => z.1 = x

@[simp]

theorem probEvent_fst_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : 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.

theorem probOutput_snd_map_eq_probEvent {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m (α × β)) (y : β) : Pr[= y | Prod.snd <$> mx] = probEvent mx fun (z : α × β) => z.2 = y

@[simp]

theorem probEvent_snd_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : 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.

@[simp]

theorem probEvent_fst_eq_snd {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (mx : m (α × α)) : (probEvent mx fun (z : α × α) => z.1 = z.2) = ∑' (x : α), Pr[= (x, x) | mx]

@[simp]

theorem probOutput_seq_map_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m α) (my : m β) (z : α × β) : Pr[= z | Prod.mk <$> mx <*> my] = Pr[= z.1 | mx] * Pr[= z.2 | my]

@[simp]

theorem support_seq_map_prod_mk {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m α) (my : m β) : support (Prod.mk <$> mx <*> my) = support mx ×ˢ support my

theorem finSupport_seq_map_prod_mk {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m α) (my : m β) [HasEvalFinset m] [DecidableEq α] [DecidableEq β] : finSupport (Prod.mk <$> mx <*> my) = (finSupport mx).product (finSupport my)

@[simp]

theorem probOutput_seq_map_prod_mk_map_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : 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]

@[simp]

theorem probOutput_seq_map_prod_mk_map_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : 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]

@[simp]

theorem probOutput_bind_map_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : 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]

@[simp]

theorem probOutput_bind_map_prod_mk_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : 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]

@[simp]

theorem support_seq_map_prod_mk_eq_sprod {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) : support ((fun (x1 : α) (x2 : β) => (f x1, g x2)) <$> mx <*> my) = (f '' support mx) ×ˢ (g '' support my)

theorem finSupport_seq_map_prod_mk_eq_product {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : Type u} (mx : m α) (my : m β) (f : α → γ) (g : β → δ) [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))

theorem probOutput_bind_bind_prod_mk_eq_mul {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : 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]

theorem probOutput_bind_bind_prod_mk_eq_mul' {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β γ δ : 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]

@[simp]

theorem probOutput_prod_mk_fst_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : 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

@[simp]

theorem probOutput_prod_mk_snd_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : 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