Independent finite PMF products

A product of finite distributions assigns each tuple the product of its coordinate masses. Its induced measure is Mathlib's product measure, so its coordinates satisfy the independence and concentration theorems. Mapping coordinates commutes with this product. Replacing one coordinate of a uniform tuple by a fresh uniform sample preserves its law.

Main definitions

• Cslib.Probability.PMF.pi: independent finite products with dependent coordinate types.

Main results

• Cslib.Probability.PMF.toMeasure_pi, .toMeasure_bind_pair, .iIndepFun_pi: product-measure and independence laws.
• Cslib.Probability.PMF.pi_bind_update_pair: reveal a coordinate and retain the entire tuple.
• Cslib.Probability.PMF.pi_map, .pi_bind: coordinatewise mapping and sampling laws.
• Cslib.Probability.PMF.conditionalSnd_pi_joint: coordinatewise conditioning.

References

Adapted from Probability/Product.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The measure and independence results reuse Mathlib.

theorem Cslib.Probability.PMF.toMeasure_bind_pair {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Countable α] [Countable β] (p : PMF α) (q : PMF β) : (p.bind fun (a : α) => PMF.map (fun (b : β) => (a, b)) q).toMeasure = p.toMeasure.prod q.toMeasure

Independent PMF samples induce the product of their measures.

noncomputable def Cslib.Probability.PMF.pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) : PMF ((i : ι) → α i)

Draw each coordinate independently from its specified finite distribution.

@[simp]

theorem Cslib.Probability.PMF.pi_apply {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) (outcome : (i : ι) → α i) : (pi p) outcome = ∏ i : ι, (p i) (outcome i)

Independent tuple masses are products of their coordinate masses.

theorem Cslib.Probability.PMF.mem_support_pi_iff {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) (outcome : (i : ι) → α i) : outcome ∈ (pi p).support ↔ ∀ (i : ι), outcome i ∈ (p i).support

A tuple can occur precisely when every coordinate can occur.

theorem Cslib.Probability.PMF.toMeasure_pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSingletonClass (α i)] (p : (i : ι) → PMF (α i)) : (pi p).toMeasure = MeasureTheory.Measure.pi fun (i : ι) => (p i).toMeasure

The PMF product agrees with the measure-theoretic product.

theorem Cslib.Probability.PMF.iIndepFun_pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [(i : ι) → MeasurableSpace (α i)] [∀ (i : ι), MeasurableSingletonClass (α i)] (p : (i : ι) → PMF (α i)) : ProbabilityTheory.iIndepFun (fun (i : ι) (outcome : (i : ι) → α i) => outcome i) (pi p).toMeasure

Coordinate projections of the product are mutually independent.

@[simp]

theorem Cslib.Probability.PMF.pi_map_eval {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) (i : ι) : PMF.map (fun (outcome : (i : ι) → α i) => outcome i) (pi p) = p i

Each coordinate of the independent product has its specified distribution.

theorem Cslib.Probability.PMF.pi_uniformOfFintype {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [DecidableEq ι] [(i : ι) → Fintype (α i)] [∀ (i : ι), Nonempty (α i)] : (pi fun (i : ι) => uniformOfFintype (α i)) = uniformOfFintype ((i : ι) → α i)

Independent uniform coordinates give the uniform distribution on tuples.

theorem Cslib.Probability.PMF.uniformOfFintype_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ : Type u_4} [Fintype γ] [Nonempty γ] (i : ι) : ((uniformOfFintype γ).bind fun (value : γ) => PMF.map (fun (values : ι → γ) => Function.update values i value) (uniformOfFintype (ι → γ))) = uniformOfFintype (ι → γ)

Replacing one coordinate of a uniform tuple by a fresh uniform draw preserves its law. The other coordinates stay independent of the replacement.

theorem Cslib.Probability.PMF.pi_map {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (p : (i : ι) → PMF (α i)) (f : (i : ι) → α i → β i) : (pi fun (i : ι) => PMF.map (f i) (p i)) = PMF.map (fun (outcome : (i : ι) → α i) (i : ι) => f i (outcome i)) (pi p)

Applying a separate function to each coordinate preserves the product structure.

theorem Cslib.Probability.PMF.pi_bind {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (p : (i : ι) → PMF (α i)) (kernel : (i : ι) → α i → PMF (β i)) : (pi fun (i : ι) => (p i).bind (kernel i)) = (pi p).bind fun (outcome : (i : ι) → α i) => pi fun (i : ι) => kernel i (outcome i)

Independent conditional samples can be drawn after the complete tuple of their inputs.

theorem Cslib.Probability.PMF.pi_bind_update {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [DecidableEq ι] (p : (i : ι) → PMF (α i)) (i : ι) : ((p i).bind fun (value : α i) => pi (Function.update p i (PMF.pure value))) = pi p

One coordinate of an independent product may be sampled first and then held fixed.

theorem Cslib.Probability.PMF.pi_bind_update_pair {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [DecidableEq ι] (p : (i : ι) → PMF (α i)) (i : ι) : ((p i).bind fun (value : α i) => PMF.map (fun (x : (i : ι) → α i) => (value, x)) (pi (Function.update p i (PMF.pure value)))) = PMF.map (fun (outcome : (i : ι) → α i) => (outcome i, outcome)) (pi p)

Revealing one coordinate and retaining the tuple is equivalent to sampling that coordinate first, then independently completing the remaining coordinates.

theorem Cslib.Probability.PMF.pi_fin_succ {γ : Type u_4} [Finite γ] (count : ℕ) (p : PMF γ) : (pi fun (x : Fin (count + 1)) => p) = p.bind fun (first : γ) => PMF.map (Fin.cons first) (pi fun (x : Fin count) => p)

Split an independent finite sequence into its first draw and its remaining draws.

theorem Cslib.Probability.PMF.pi_bind_pair {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (p : (i : ι) → PMF (α i)) (kernel : (i : ι) → α i → PMF (β i)) : PMF.map (fun (outcome : (i : ι) → α i × β i) => (fun (i : ι) => (outcome i).1, fun (i : ι) => (outcome i).2)) (pi fun (i : ι) => (p i).bind fun (a : α i) => PMF.map (fun (x : β i) => (a, x)) (kernel i a)) = (pi p).bind fun (outcome : (i : ι) → α i) => PMF.map (fun (x : (i : ι) → β i) => (outcome, x)) (pi fun (i : ι) => kernel i (outcome i))

Independent pairs can be sampled by drawing their first components, then drawing each second component conditionally and independently.

theorem Cslib.Probability.PMF.pi_joint_eq_bind_conditionalSnd {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (joint : (i : ι) → PMF (α i × β i)) : PMF.map (fun (outcome : (i : ι) → α i × β i) => (fun (i : ι) => (outcome i).1, fun (i : ι) => (outcome i).2)) (pi joint) = (pi fun (i : ι) => PMF.map Prod.fst (joint i)).bind fun (observed : (i : ι) → α i) => PMF.map (fun (x : (i : ι) → β i) => (observed, x)) (pi fun (i : ι) => conditionalSnd (joint i) (observed i))

Independent joint samples can be drawn by first drawing all observations and then drawing the hidden coordinates independently from their conditional distributions.

theorem Cslib.Probability.PMF.conditionalSnd_pi_joint {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} {β : ι → Type u_3} [∀ (i : ι), Finite (α i)] [∀ (i : ι), Finite (β i)] (joint : (i : ι) → PMF (α i × β i)) (observed : (i : ι) → α i) (hobserved : observed ∈ (pi fun (i : ι) => PMF.map Prod.fst (joint i)).support) : conditionalSnd (PMF.map (fun (outcome : (i : ι) → α i × β i) => (fun (i : ι) => (outcome i).1, fun (i : ι) => (outcome i).2)) (pi joint)) observed = pi fun (i : ι) => conditionalSnd (joint i) (observed i)

Conditioning independent joint samples on a possible observation tuple preserves independence of their hidden coordinates.