Part A: Probability of Sets and Conditional Probability

noncomputable def PMF.prob {α : Type u_1} (p : PMF α) (A : Set α) : ENNReal

Probability of a set under a PMF: Pr_p[A] = ∑_a 𝟙_A(a) · p(a).

Equations

• p.prob A = ∑' (a : α), A.indicator (⇑p) a

noncomputable def PMF.condProb {α : Type u_1} (p : PMF α) (A B : Set α) : ENNReal

Conditional probability: Pr_p[A | B] = Pr_p[A ∩ B] / Pr_p[B].

Equations

• p.condProb A B = p.prob (A ∩ B) / p.prob B

@[simp]

theorem PMF.prob_empty {α : Type u_1} (p : PMF α) : p.prob ∅ = 0

@[simp]

theorem PMF.prob_univ {α : Type u_1} (p : PMF α) : p.prob Set.univ = 1

theorem PMF.prob_le_one {α : Type u_1} (p : PMF α) (A : Set α) : p.prob A ≤ 1

theorem PMF.prob_ne_top {α : Type u_1} (p : PMF α) (A : Set α) : p.prob A ≠ ⊤

theorem PMF.prob_mono {α : Type u_1} (p : PMF α) {A B : Set α} (h : A ⊆ B) : p.prob A ≤ p.prob B

theorem PMF.prob_singleton {α : Type u_1} (p : PMF α) (a : α) : p.prob {a} = p a

theorem PMF.prob_inter_le_right {α : Type u_1} (p : PMF α) (A B : Set α) : p.prob (A ∩ B) ≤ p.prob B

theorem PMF.condProb_le_one {α : Type u_1} (p : PMF α) (A B : Set α) : p.condProb A B ≤ 1

Pr[A | B] ≤ 1.

theorem PMF.condProb_mul {α : Type u_1} (p : PMF α) (A B : Set α) : p.condProb A B * p.prob B = p.prob (A ∩ B)

Pr[A | B] · Pr[B] = Pr[A ∩ B] (definition of conditional probability).

theorem PMF.condProb_self {α : Type u_1} (p : PMF α) (B : Set α) (hB : p.prob B ≠ 0) : p.condProb B B = 1

Pr[B | B] = 1 when Pr[B] ≠ 0.

theorem PMF.bayes_theorem {α : Type u_1} (p : PMF α) (A B : Set α) : p.condProb A B * p.prob B = p.condProb B A * p.prob A

Bayes' theorem: Pr[A|B] · Pr[B] = Pr[B|A] · Pr[A].

theorem PMF.total_probability {α : Type u_1} (p : PMF α) (A B : Set α) : p.condProb A B * p.prob B + p.condProb A Bᶜ * p.prob Bᶜ = p.prob A

Law of total probability: Pr[A] = Pr[A|B] · Pr[B] + Pr[A|Bᶜ] · Pr[Bᶜ].

Part B: Bayesian Inversion

noncomputable def PMF.joint {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) : PMF (α × β)

Joint distribution from prior π and likelihood f: joint(a, b) = π(a) · f(a)(b).

Equations

• π.joint f = ⟨fun (x : α × β) => match x with | (a, b) => π a * (f a) b, ⋯⟩

noncomputable def PMF.marginalβ {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (b : β) : ENNReal

Marginal on β: marginal(b) = ∑_a π(a) · f(a)(b).

Equations

• π.marginalβ f b = ∑' (a : α), π a * (f a) b

@[simp]

theorem PMF.joint_apply {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (a : α) (b : β) : (π.joint f) (a, b) = π a * (f a) b

theorem PMF.marginalβ_eq_bind {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (b : β) : π.marginalβ f b = (π.bind f) b

noncomputable def CatCrypt.Prob.bayesInv {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (b : β) (hmarg : π.marginalβ f b ≠ 0) : PMF α

Bayesian inversion: posterior distribution P(a | b). Uses PMF.normalize on the un-normalized posterior a ↦ π(a) · f(a)(b).

Equations

• CatCrypt.Prob.bayesInv π f b hmarg = PMF.normalize (fun (a : α) => π a * (f a) b) ⋯ ⋯

theorem CatCrypt.Prob.bayesInv_apply {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (b : β) (hmarg : π.marginalβ f b ≠ 0) (a : α) : (bayesInv π f b hmarg) a = π a * (f a) b * (π.marginalβ f b)⁻¹

theorem CatCrypt.Prob.bayesInv_recovery {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (b : β) (hmarg : π.marginalβ f b ≠ 0) (a : α) : (bayesInv π f b hmarg) a * π.marginalβ f b = π a * (f a) b

Recovery equation (discrete Bayes' theorem): posterior(a) · marginal(b) = π(a) · f(a)(b).

theorem CatCrypt.Prob.marginalβ_eq_tsum_joint {α : Type u_1} {β : Type u_2} (π : PMF α) (f : α → PMF β) (b : β) : π.marginalβ f b = ∑' (a : α), (π.joint f) (a, b)

The marginal is the sum of joint over the first component.

Part C: Uniform Conditioning

theorem CatCrypt.Prob.prob_uniform_eq {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] (A : Finset α) : (PMF.uniformOfFintype α).prob ↑A = ↑A.card / ↑(Fintype.card α)

For uniform distribution, Pr[A] = |A| / |α|.

theorem CatCrypt.Prob.condProb_uniform_eq {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] (A B : Finset α) : (PMF.uniformOfFintype α).condProb ↑A ↑B = ↑(A ∩ B).card / ↑B.card

For uniform distribution on a finite type, conditional probability is Pr[A | B] = |A ∩ B| / |B|.

theorem CatCrypt.Prob.condProb_uniform_singleton {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] (a : α) (B : Finset α) (ha : a ∈ B) : (PMF.uniformOfFintype α).condProb {a} ↑B = (↑B.card)⁻¹

For uniform distribution, probability of a single element given membership in B is 1 / |B|.