Marginals, conditionals, and products of joint PMFs

Structural operations on PMF (α × β): the projections fst/snd (row/column marginals), the conditional cond, and the independent product (a mathlib gap, [UPSTREAM] candidate). These are measure-free bookkeeping on finite joints; information-theoretic consumers live in Entropy.lean, Bayesian ones in JointPosterior.lean.

Main definitions

• PMF.fst, PMF.snd — marginals of a joint PMF via PMF.map.
• PMF.cond — conditional distribution given a second-coordinate value.
• PMF.product — independent product distribution.

Main results

• fst_apply / snd_apply — marginals as row/column sums.
• snd_mul_cond, toMeasure_cond — chain rule and the bridge to ProbabilityTheory.cond.
• product_apply, toMeasure_product — pointwise and measure-level characterization of the product.

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

Marginal along the first projection.

Equations

• joint.fst = PMF.map Prod.fst joint

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

Marginal along the second projection.

Equations

• joint.snd = PMF.map Prod.snd joint

theorem PMF.fst_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] (joint : PMF (α × β)) (a : α) : joint.fst a = ∑ b : β, joint (a, b)

joint.fst a = ∑ b, joint (a, b) for finite-Fintype joint PMFs. The first marginal is the row-sum of the joint.

theorem PMF.snd_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (joint : PMF (α × β)) (b : β) : joint.snd b = ∑ a : α, joint (a, b)

joint.snd b = ∑ a, joint (a, b) for finite-Fintype joint PMFs. The second marginal is the column-sum of the joint.

theorem PMF.fst_toRealFn_eq_sum {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] (joint : PMF (α × β)) (a : α) : joint.fst.toRealFn a = ∑ b : β, joint.toRealFn (a, b)

toRealFn of the first marginal equals the row-sum of toRealFn of the joint.

theorem PMF.snd_toRealFn_eq_sum {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (joint : PMF (α × β)) (b : β) : joint.snd.toRealFn b = ∑ a : α, joint.toRealFn (a, b)

toRealFn of the second marginal equals the column-sum of toRealFn of the joint.

theorem PMF.apply_le_fst {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] (joint : PMF (α × β)) (x : α × β) : joint x ≤ joint.fst x.1

The joint is atomwise dominated by its first marginal.

theorem PMF.apply_le_snd {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (joint : PMF (α × β)) (x : α × β) : joint x ≤ joint.snd x.2

The joint is atomwise dominated by its second marginal.

theorem PMF.fst_apply_ne_zero {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] {joint : PMF (α × β)} {x : α × β} (h : joint x ≠ 0) : joint.fst x.1 ≠ 0

A point of positive joint mass has positive first-marginal mass.

theorem PMF.snd_apply_ne_zero {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] {joint : PMF (α × β)} {x : α × β} (h : joint x ≠ 0) : joint.snd x.2 ≠ 0

A point of positive joint mass has positive second-marginal mass.

theorem PMF.tsum_indicator_fiber_snd {α : Type u_1} {β : Type u_2} [DecidableEq β] (G : PMF (α × β)) (b : β) : ∑' (x : α × β), {x : α × β | x.2 = b}.indicator (⇑G) x = G.snd b

The fiber mass over a second-coordinate value is the second marginal.

theorem PMF.snd_apply_ne_zero_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] (G : PMF (α × β)) (b : β) : G.snd b ≠ 0 ↔ ∃ x ∈ {x : α × β | x.2 = b}, x ∈ G.support

A positive second marginal is witnessed on its fiber.

noncomputable def PMF.cond {α : Type u_1} {β : Type u_2} [DecidableEq β] (G : PMF (α × β)) (b : β) : PMF α

The conditional distribution of the first coordinate of a joint given the second: the discrete disintegration of a joint PMF (the PMF mirror of MeasureTheory.Measure.condKernel), via PMF.filter on the fiber. Junk (an arbitrary point mass) at b of marginal mass zero; lemmas hypothesize G.snd b ≠ 0.

Equations

• G.cond b = if h : G.snd b ≠ 0 then PMF.map Prod.fst (G.filter {x : α × β | x.2 = b} ⋯) else PMF.pure ⋯.some.1

theorem PMF.cond_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (G : PMF (α × β)) {b : β} (h : G.snd b ≠ 0) (a : α) : (G.cond b) a = G (a, b) / G.snd b

The conditional is the joint renormalized by the marginal.

theorem PMF.snd_mul_cond {α : Type u_1} {β : Type u_2} [DecidableEq β] (G : PMF (α × β)) {b : β} (h : G.snd b ≠ 0) (a : α) : G.snd b * (G.cond b) a = G (a, b)

Disintegration identity: marginal times conditional is the joint.

theorem PMF.toMeasure_cond {α : Type u_1} {β : Type u_2} [DecidableEq β] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (G : PMF (α × β)) {b : β} (h : G.snd b ≠ 0) : (G.cond b).toMeasure = MeasureTheory.Measure.map Prod.fst G.toMeasure[|Prod.snd ⁻¹' {b}]

The measure of the conditional is the conditioned measure's first marginal, connecting PMF.cond to ProbabilityTheory.cond.

theorem PMF.toMeasure_fst {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (joint : PMF (α × β)) : joint.toMeasure.fst = joint.fst.toMeasure

The measure of the first marginal is the first marginal of the measure.

theorem PMF.toMeasure_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (joint : PMF (α × β)) : joint.toMeasure.snd = joint.snd.toMeasure

The measure of the second marginal is the second marginal of the measure.

theorem PMF.sum_toReal_mul_fst {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] (joint : PMF (α × β)) (f : α → ℝ) : ∑ x : α × β, (joint x).toReal * f x.1 = ∑ a : α, (joint.fst a).toReal * f a

Law of the unconscious statistician for the first marginal: the joint expectation of a function of the first coordinate is its expectation under the marginal.

theorem PMF.sum_toReal_mul_snd {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (joint : PMF (α × β)) (f : β → ℝ) : ∑ x : α × β, (joint x).toReal * f x.2 = ∑ b : β, (joint.snd b).toReal * f b

Law of the unconscious statistician for the second marginal.

Product PMF

PMF.product P Q is the independent joint distribution: (P.product Q) (a, b) = P a · Q b. Foundation for defining mutualInformation as KL(joint ‖ product).

Mathlib gap. PMF.product is missing from mathlib. Defined here via the standard monadic bind/map construction.

noncomputable def PMF.product {α : Type u_1} {β : Type u_2} (P : PMF α) (Q : PMF β) : PMF (α × β)

The independent product distribution of two PMFs.

Equations

• P.product Q = P.bind fun (a : α) => PMF.map (Prod.mk a) Q

@[simp]

theorem PMF.product_apply {α : Type u_1} {β : Type u_2} (P : PMF α) (Q : PMF β) (a : α) (b : β) : (P.product Q) (a, b) = P a * Q b

@[simp]

theorem PMF.product_toRealFn {α : Type u_1} {β : Type u_2} (P : PMF α) (Q : PMF β) (a : α) (b : β) : (P.product Q).toRealFn (a, b) = P.toRealFn a * Q.toRealFn b

theorem PMF.toMeasure_product {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (P : PMF α) (Q : PMF β) : (P.product Q).toMeasure = P.toMeasure.prod Q.toMeasure

The measure of the product PMF is the product of the measures.