Evaluation Distributions of Computations with map

File for lemmas about evalDist and support involving the monadic map.

Note: we focus on lemmas that don't hold naively when reducing <$> to >>= using monad laws, since map_eq_bind_pure_comp can be applied to use bind lemmas fairly easily. Instead we focus on the cases like f <$> mx for injective f, which allow stronger statements. More generally we can consier f with InjOn f (support mx) and get good lemmas.

TODO: many lemmas should probably have mirrored bind_pure versions.

@[simp]

theorem support_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSet m] [LawfulMonad m] (f : α → β) (mx : m α) : support (f <$> mx) = f '' support mx

@[simp]

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

@[simp]

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

@[simp]

theorem evalDist_comp_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) : (evalDist ∘ fun (f : α → β) => f <$> mx) = fun (f : α → β) => f <$> evalDist mx

@[simp]

theorem probEvent_bind_pure_comp {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) (q : β → Prop) : Pr[q | mx >>= pure ∘ f] = Pr[q ∘ f | mx]

theorem probOutput_map_eq_tsum_subtype {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) [LawfulMonad m] (y : β) : Pr[=y | f <$> mx] = ∑' (x : ↑{x : α | x ∈ support mx ∧ y = f x}), Pr[=↑x | mx]

Write the probability of an output after mapping the result of a computation as a sum over all outputs such that they map to the correct final output, using subtypes. This lemma notably doesn't require decidable equality on the final type, unlike most lemmas about probability when mapping a computation.

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

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

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

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

theorem probOutput_map_eq_sum_finSupport_ite {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) [LawfulMonad m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (y : β) : Pr[=y | f <$> mx] = ∑ x ∈ finSupport mx, if y = f x then Pr[=x | mx] else 0

theorem probOutput_map_eq_sum_filter_finSupport {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) [LawfulMonad m] [HasEvalFinset m] [DecidableEq α] [DecidableEq β] (y : β) : Pr[=y | f <$> mx] = ∑ x ∈ finSupport mx with y = f x, Pr[=x | mx]

@[simp]

theorem probFailure_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) [LawfulMonad m] : Pr[⊥ | f <$> mx] = Pr[⊥ | mx]

@[simp]

theorem probEvent_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) [LawfulMonad m] (q : β → Prop) : Pr[q | f <$> mx] = Pr[q ∘ f | mx]

theorem probEvent_comp {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) (f : α → β) [LawfulMonad m] (q : β → Prop) : Pr[q ∘ f | mx] = Pr[q | f <$> mx]

theorem probFailure_eq_sub_sum_probOutput_map {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] [Fintype β] (mx : m α) (f : α → β) : Pr[⊥ | mx] = 1 - ∑ y : β, Pr[=y | f <$> mx]

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

theorem support_map_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (y : β) (hx : (support mx).Nonempty) : support ((fun (x : α) => y) <$> mx) = {y}

@[simp]

theorem finSupport_map_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (y : β) [DecidableEq α] [DecidableEq β] [HasEvalFinset m] (hx : (finSupport mx).Nonempty) : finSupport ((fun (x : α) => y) <$> mx) = if (finSupport mx).Nonempty then {y} else ∅

@[simp]

theorem probOutput_map_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (y y' : β) : Pr[=y' | (fun (x : α) => y) <$> mx] = (1 - Pr[⊥ | mx]) * Pr[=y' | pure y]

@[simp]

theorem probEvent_map_const {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (y : β) (p : β → Prop) : Pr[p | (fun (x : α) => y) <$> mx] = (1 - Pr[⊥ | mx]) * Pr[p | pure y]

@[simp]

theorem probEvent_map_const' {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) (y : β) (p : β → Prop) [DecidablePred p] : Pr[p | (fun (x : α) => y) <$> mx] = if p y then 1 - Pr[⊥ | mx] else 0

theorem probOutput_map_eq_probOutput_of_leftInvOn {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) [LawfulMonad m] {f : α → β} {g : β → α} {y : β} (hr : Set.LeftInvOn g f (support mx)) (hy : f (g y) = y) : Pr[=y | f <$> mx] = Pr[=g y | mx]

theorem probOutput_map_eq_probOutput_inverse {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) [LawfulMonad m] {f : α → β} {g : β → α} {y : β} (hl : Function.LeftInverse g f) (hy : f (g y) = y) : Pr[=y | f <$> mx] = Pr[=g y | mx]

theorem probOutput_map_eq_probOutput_apply {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] (mx : m α) [LawfulMonad m] {f : α → β} {g : β → α} {y : β} (hl : f (g y) = y) (hr : ∀ (y : α), g (f y) = y) : Pr[=y | f <$> mx] = Pr[=g y | mx]

theorem probOutput_map_eq_probOutput_invFunOn {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] [Nonempty α] (mx : m α) {f : α → β} (hf : Set.InjOn f (support mx)) (y : β) (hy : ∃ x ∈ support mx, f x = y) : Pr[=y | f <$> mx] = Pr[=Function.invFunOn f (support mx) y | mx]

theorem probOutput_map_injective {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) {f : α → β} (hf : Function.Injective f) (x : α) : Pr[=f x | f <$> mx] = Pr[=x | mx]

theorem probOutput_map_eq_probOutput {α β : Type u} {m : Type u → Type v} [Monad m] [HasEvalSPMF m] [LawfulMonad m] (mx : m α) {f : α → β} (hf : ∀ (x x' : α), f x = f x' → x = x') (x : α) : Pr[=f x | f <$> mx] = Pr[=x | mx]