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

theorem mem_support_seq_iff {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [LawfulMonad m] (mf : m (α → β)) (mx : m α) (y : β) : y ∈ support (mf <*> mx) ↔ ∃ f ∈ support mf, ∃ x ∈ support mx, f x = y

@[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) : probEvent (mf <*> mx) p = ∑' (f : α → β), Pr[= f | mf] * probEvent mx (p ∘ f)

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] : probEvent (mf <*> mx) p = ∑' (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) : probEvent (mx <* my) p = (1 - Pr[⊥ | my]) * probEvent mx p

@[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) : probEvent (mx *> my) p = (1 - Pr[⊥ | mx]) * probEvent my p

@[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] (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

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

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)

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) : probEvent (Function.swap f <$> my <*> mx) p = probEvent (f <$> mx <*> my) p

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)

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 γ] : 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) : probEvent (f <$> mx <*> my) p = probEvent mx q1 * probEvent my q2

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) : probEvent (f <$> mx <*> my) p = probEvent (Prod.mk <$> mx <*> my) (p ∘ Function.uncurry f)

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) : probEvent (f <$> mx <*> my) p = probEvent (Prod.mk <$> mx <*> my) fun (z : α × β) => p (f z.1 z.2)