Lemmas About the Distribution Semantics of Seq

This file collects various lemmas about the monadic sequence operation og <*> oa.

One especially important case is f <$> oa <*> ob where f : α → β → γ, that runs the two computations oa and ob to get some x and y respectively, returning only the value f x y.

@[simp]

theorem OracleComp.support_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) : (og <*> oa).support = ⋃ g ∈ og.support, g '' oa.support

@[simp]

theorem OracleComp.finSupport_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α] [DecidableEq β] [DecidableEq (α → β)] : (og <*> oa).finSupport = og.finSupport.biUnion fun (g : α → β) => Finset.image g oa.finSupport

theorem OracleComp.probOutput_seq_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.FiniteRange] (y : β) : [=y|og <*> oa] = ∑' (g : α → β) (x : α), [=g|og] * [=x|oa] * [=y|pure (g x)]

theorem OracleComp.probOutput_seq_eq_tsum_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.FiniteRange] [DecidableEq β] (y : β) : [=y|og <*> oa] = ∑' (g : α → β) (x : α), if y = g x then [=g|og] * [=x|oa] else 0

theorem OracleComp.probOutput_seq_eq_sum_finSupport_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] [DecidableEq (α → β)] [DecidableEq β] (y : β) : [=y|og <*> oa] = ∑ g ∈ og.finSupport, ∑ x ∈ oa.finSupport, if y = g x then [=g|og] * [=x|oa] else 0

theorem OracleComp.probFailure_seq {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.FiniteRange] : [⊥|og <*> oa] = [⊥|og] + [⊥|oa] - [⊥|og] * [⊥|oa]

theorem OracleComp.probEvent_seq_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.FiniteRange] (p : β → Prop) : [p|og <*> oa] = ∑' (g : α → β), [=g|og] * [p ∘ g|oa]

theorem OracleComp.probEvent_seq_eq_tsum_ite {ι : Type u} {spec : OracleSpec ι} {α β : Type v} (oa : OracleComp spec α) (og : OracleComp spec (α → β)) [spec.FiniteRange] (p : β → Prop) [DecidablePred p] : [p|og <*> oa] = ∑' (g : α → β) (x : α), if p (g x) then [=g|og] * [=x|oa] else 0

@[simp]

theorem OracleComp.support_seq_map_eq_image2 {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) : (f <$> oa <*> ob).support = Set.image2 f oa.support ob.support

@[simp]

theorem OracleComp.finSupport_seq_map_eq_image2 {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] [DecidableEq β] [DecidableEq γ] : (f <$> oa <*> ob).finSupport = Finset.image₂ f oa.finSupport ob.finSupport

theorem OracleComp.evalDist_seq_map {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] : (f <$> oa <*> ob).evalDist = f <$> oa.evalDist <*> ob.evalDist

theorem OracleComp.probOutput_seq_map_eq_tsum {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (z : γ) : [=z|f <$> oa <*> ob] = ∑' (x : α) (y : β), [=x|oa] * [=y|ob] * [=z|pure (f x y)]

theorem OracleComp.probOutput_seq_map_eq_tsum_ite {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] [DecidableEq γ] (z : γ) : [=z|f <$> oa <*> ob] = ∑' (x : α) (y : β), if z = f x y then [=x|oa] * [=y|ob] else 0

theorem OracleComp.probEvent_seq_map_eq_probEvent_comp_uncurry {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (p : γ → Prop) : [p|f <$> oa <*> ob] = [p ∘ Function.uncurry f|Prod.mk <$> oa <*> ob]

theorem OracleComp.probEvent_seq_map_eq_probEvent {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (p : γ → Prop) : [p|f <$> oa <*> ob] = [fun (z : α × β) => p (f z.1 z.2)|Prod.mk <$> oa <*> ob]

@[simp]

theorem OracleComp.probOutput_seq_map_swap {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (z : γ) : [=z|Function.swap f <$> ob <*> oa] = [=z|f <$> oa <*> ob]

@[simp]

theorem OracleComp.evalDist_seq_map_swap {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] : (Function.swap f <$> ob <*> oa).evalDist = (f <$> oa <*> ob).evalDist

@[simp]

theorem OracleComp.probEvent_seq_map_swap {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (p : γ → Prop) : [p|Function.swap f <$> ob <*> oa] = [p|f <$> oa <*> ob]

@[simp]

theorem OracleComp.support_seq_map_swap {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] : (Function.swap f <$> ob <*> oa).support = (f <$> oa <*> ob).support

@[simp]

theorem OracleComp.finSupport_seq_map_swap {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq γ] : (Function.swap f <$> ob <*> oa).finSupport = (f <$> oa <*> ob).finSupport

theorem OracleComp.mem_support_seq_map_iff_of_injective2 {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) (hf : Function.Injective2 f) (x : α) (y : β) : f x y ∈ (f <$> oa <*> ob).support ↔ x ∈ oa.support ∧ y ∈ ob.support

theorem OracleComp.mem_finSupport_seq_map_iff_of_injective2 {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (hf : Function.Injective2 f) (x : α) (y : β) : f x y ∈ (f <$> oa <*> ob).finSupport ↔ x ∈ oa.finSupport ∧ y ∈ ob.finSupport

theorem OracleComp.probOutput_seq_map_eq_mul_of_injective2 {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (hf : Function.Injective2 f) (x : α) (y : β) : [=f x y|f <$> oa <*> ob] = [=x|oa] * [=y|ob]

theorem OracleComp.probOutput_seq_map_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ) [spec.FiniteRange] (x : α) (y : β) (z : γ) (h : ∀ x' ∈ oa.support, ∀ y' ∈ ob.support, z = f x' y' ↔ x' = x ∧ y' = y) : [=z|f <$> oa <*> ob] = [=x|oa] * [=y|ob]

If the results of the computations oa and ob are combined with some function f, and there exists unique x and y such that f x y = z (given as explicit arguments), then the probability of getting z as an output of f <$> oa <*> ob is the product of probabilities of getting x and y from oa and ob respectively.

theorem OracleComp.probEvent_seq_map_eq_mul {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v} (f : α → β → γ) [spec.FiniteRange] (oa : OracleComp spec α) (ob : OracleComp spec β) (p : γ → Prop) (q1 : α → Prop) (q2 : β → Prop) (h : ∀ x ∈ oa.support, ∀ y ∈ ob.support, p (f x y) ↔ q1 x ∧ q2 y) : [p|f <$> oa <*> ob] = [q1|oa] * [q2|ob]

If the results of the computations oa and ob are combined with some function f, and p is an event such that outputs of f are in p iff the individual components lie in some other events q1 and q2, then the probability of the event p is the product of the probabilites holding individually. NOTE: universe levels of α, β, γ

theorem OracleComp.probOutput_map_eq_single {ι : Type u} {spec : OracleSpec ι} {α β : Type v} [spec.FiniteRange] {oa : OracleComp spec α} {f : α → β} {y : β} (x : α) (h : ∀ x' ∈ oa.support, y = f x' → x = x') (h' : f x = y) : [=y|f <$> oa] = [=x|oa]