Evaluation Distributions of Computations with seq

File for lemmas about evalDist and support involving the monadic seq, seqLeft, and seqRight operations.

TODO: many lemmas should probably have mirrored versions for bind_map.

@[simp]

theorem support_seq {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) : support (mf <*> mx) = ⋃ f ∈ support mf, f '' support mx

@[simp]

theorem finSupport_seq {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [HasEvalFinset m] [LawfulMonad m] [DecidableEq (α → β)] [DecidableEq α] [DecidableEq β] (mf : m (α → β)) (mx : m α) : finSupport (mf <*> mx) = (finSupport mf).biUnion fun (f : α → β) => Finset.image f (finSupport mx)

@[simp]

theorem evalDist_seq {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) : evalDist (mf <*> mx) = evalDist mf <*> evalDist mx

theorem probOutput_seq_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) (y : β) : Pr[=y | mf <*> mx] = ∑' (f : α → β) (x : α), Pr[=f | mf] * Pr[=x | mx] * Pr[=y | pure (f x)]

theorem probOutput_seq_eq_tsum_ite {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] [DecidableEq β] (mf : m (α → β)) (mx : m α) (y : β) : Pr[=y | mf <*> mx] = ∑' (f : α → β) (x : α), if y = f x then Pr[=f | mf] * Pr[=x | mx] else 0

@[simp]

theorem probFailure_seq {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) : Pr[⊥ | mf <*> mx] = Pr[⊥ | mf] + Pr[⊥ | mx] - Pr[⊥ | mf] * Pr[⊥ | mx]

theorem probEvent_seq_eq_tsum {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) (p : β → Prop) : Pr[p | mf <*> mx] = ∑' (f : α → β), Pr[=f | mf] * Pr[p ∘ f | mx]

theorem probEvent_seq_eq_tsum_ite {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) (p : β → Prop) [DecidablePred p] : Pr[p | mf <*> mx] = ∑' (f : α → β) (x : α), if p (f x) then Pr[=f | mf] * Pr[=x | mx] else 0

@[simp]

theorem support_seqLeft {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [LawfulMonad m] (mx : m α) (my : m β) [Decidable (support my).Nonempty] : support (mx <* my) = if (support my).Nonempty then support mx else ∅

@[simp]

theorem evalDist_seqLeft {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) : evalDist (mx <* my) = evalDist mx <* evalDist my

@[simp]

theorem probOutput_seqLeft {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) (x : α) : Pr[=x | mx <* my] = (1 - Pr[⊥ | my]) * Pr[=x | mx]

@[simp]

theorem probFailure_seqLeft {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) : Pr[⊥ | mx <* my] = Pr[⊥ | mx] + Pr[⊥ | my] - Pr[⊥ | mx] * Pr[⊥ | my]

@[simp]

theorem probEvent_seqLeft {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) (p : α → Prop) : Pr[p | mx <* my] = (1 - Pr[⊥ | my]) * Pr[p | mx]

@[simp]

theorem support_seqRight {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [LawfulMonad m] (mx : m α) (my : m β) [Decidable (support mx).Nonempty] : support (mx *> my) = if (support mx).Nonempty then support my else ∅

@[simp]

theorem evalDist_seqRight {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) : evalDist (mx *> my) = evalDist mx *> evalDist my

@[simp]

theorem probOutput_seqRight {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) (y : β) : Pr[=y | mx *> my] = (1 - Pr[⊥ | mx]) * Pr[=y | my]

@[simp]

theorem probFailure_seqRight {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) : Pr[⊥ | mx *> my] = Pr[⊥ | mx] + Pr[⊥ | my] - Pr[⊥ | mx] * Pr[⊥ | my]

@[simp]

theorem probEvent_seqRight {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (my : m β) (p : β → Prop) : Pr[p | mx *> my] = (1 - Pr[⊥ | mx]) * Pr[p | my]

@[simp]

theorem support_seq_map_eq_image2 {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSet m] : support (f <$> mx <*> my) = Set.image2 f (support mx) (support my)

@[simp]

theorem finSupport_seq_map_eq_image2 {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] [DecidableEq γ] : finSupport (f <$> mx <*> my) = Finset.image₂ f (finSupport mx) (finSupport my)

theorem evalDist_seq_map {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] : evalDist (f <$> mx <*> my) = f <$> evalDist mx <*> evalDist my

theorem probOutput_seq_map_eq_tsum {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] (z : γ) : Pr[=z | f <$> mx <*> my] = ∑' (x : α) (y : β), Pr[=x | mx] * Pr[=y | my] * Pr[=z | pure (f x y)]

theorem probOutput_seq_map_eq_tsum_ite {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] [DecidableEq γ] (z : γ) : Pr[=z | f <$> mx <*> my] = ∑' (x : α) (y : β), if z = f x y then Pr[=x | mx] * Pr[=y | my] else 0

theorem probOutput_seq_map_eq_mul_of_injective2 {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] [DecidableEq γ] (hf : Function.Injective2 f) (x : α) (y : β) : Pr[=f x y | f <$> mx <*> my] = Pr[=x | mx] * Pr[=y | my]

theorem mem_support_seq_map_iff_of_injective2 {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSet m] (hf : Function.Injective2 f) (x : α) (y : β) : f x y ∈ support (f <$> mx <*> my) ↔ x ∈ support mx ∧ y ∈ support my

theorem mem_finSupport_seq_map_iff_of_injective2 {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (hf : Function.Injective2 f) (x : α) (y : β) : f x y ∈ finSupport (f <$> mx <*> my) ↔ x ∈ finSupport mx ∧ y ∈ finSupport my

@[simp]

theorem probOutput_seq_map_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] [DecidableEq γ] (z : γ) : Pr[=z | Function.swap f <$> my <*> mx] = Pr[=z | f <$> mx <*> my]

@[simp]

theorem evalDist_seq_map_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] : evalDist (Function.swap f <$> my <*> mx) = evalDist (f <$> mx <*> my)

@[simp]

theorem probEvent_seq_map_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] (p : γ → Prop) : Pr[p | Function.swap f <$> my <*> mx] = Pr[p | f <$> mx <*> my]

@[simp]

theorem support_seq_map_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSet m] : support (Function.swap f <$> my <*> mx) = support (f <$> mx <*> my)

@[simp]

theorem finSupport_seq_map_swap {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSet m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] [DecidableEq γ] : finSupport (Function.swap f <$> my <*> mx) = finSupport (f <$> mx <*> my)

theorem probEvent_seq_map_eq_mul {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] (p : γ → Prop) (q1 : α → Prop) (q2 : β → Prop) (h : ∀ x ∈ support mx, ∀ y ∈ support my, p (f x y) ↔ q1 x ∧ q2 y) : Pr[p | f <$> mx <*> my] = Pr[q1 | mx] * Pr[q2 | my]

theorem probOutput_seq_map_eq_mul {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] (x : α) (y : β) (z : γ) (h : ∀ x' ∈ support mx, ∀ y' ∈ support my, z = f x' y' ↔ x' = x ∧ y' = y) : Pr[=z | f <$> mx <*> my] = Pr[=x | mx] * Pr[=y | my]

theorem probEvent_seq_map_eq_probEvent_comp_uncurry {α β γ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (mx : m α) (my : m β) (f : α → β → γ) [HasEvalSPMF m] (p : γ → Prop) : Pr[p | f <$> mx <*> my] = Pr[p ∘ Function.uncurry f | Prod.mk <$> mx <*> my]

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