Uniform PMF finite-expectation identities

This module contains high-level uniform-expectation identities for Mathlib probability mass functions. The statements are phrased in terms of PMF.realWeightedSum, rather than finite sums, so that product, marginalization, equivalence-transport, and finite push-forward arguments can be carried out directly in the probability-mass-function language.

Main declarations

• PMF.realWeightedSum_uniformOfFintype_comm
• PMF.realWeightedSum_uniformOfFintype_prod_swap
• PMF.realWeightedSum_uniformOfFintype_equiv_prod
• PMF.realWeightedSum_uniformOfFintype_equiv_prod_swap
• PMF.realWeightedSum_uniformOfFintype_equiv_fst
• PMF.realWeightedSum_uniformOfFintype_equiv_snd
• PMF.realWeightedSum_uniformOfFintype_fst
• PMF.realWeightedSum_uniformOfFintype_snd
• PMF.realWeightedSum_map_uniformOfFintype_factor_equiv
• PMF.realWeightedSum_map_uniformOfFintype_factor_equiv_fst
• PMF.realWeightedSum_map_uniformOfFintype_factor_equiv_snd

References

These are formalization-internal finite probability lemmas for the low individual degree test development.

theorem PMF.realWeightedSum_uniformOfFintype_comm {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (f : α → β → M) : ((uniformOfFintype α).realWeightedSum fun (a : α) => (uniformOfFintype β).realWeightedSum fun (b : β) => f a b) = (uniformOfFintype β).realWeightedSum fun (b : β) => (uniformOfFintype α).realWeightedSum fun (a : α) => f a b

Swap two nested finite expectations against uniform probability mass functions.

theorem PMF.realWeightedSum_uniformOfFintype_prod_swap {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (f : α → β → M) : ((uniformOfFintype (α × β)).realWeightedSum fun (ab : α × β) => f ab.1 ab.2) = (uniformOfFintype β).realWeightedSum fun (b : β) => (uniformOfFintype α).realWeightedSum fun (a : α) => f a b

Split a finite expectation against the uniform PMF on a product into iterated finite expectations, with the second coordinate averaged first.

theorem PMF.realWeightedSum_uniformOfFintype_equiv_prod {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [Nonempty γ] [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (e : γ ≃ α × β) (f : γ → M) : (uniformOfFintype γ).realWeightedSum f = (uniformOfFintype α).realWeightedSum fun (a : α) => (uniformOfFintype β).realWeightedSum fun (b : β) => f (e.symm (a, b))

Transport a finite expectation against a uniform PMF through an equivalence whose target is a product, then split the product expectation.

theorem PMF.realWeightedSum_uniformOfFintype_equiv_prod_swap {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [Nonempty γ] [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (e : γ ≃ α × β) (f : γ → M) : (uniformOfFintype γ).realWeightedSum f = (uniformOfFintype β).realWeightedSum fun (b : β) => (uniformOfFintype α).realWeightedSum fun (a : α) => f (e.symm (a, b))

Transport a finite expectation against a uniform PMF through an equivalence whose target is a product, then split the product expectation with the second coordinate averaged first.

theorem PMF.realWeightedSum_uniformOfFintype_equiv_fst {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [Nonempty γ] [Fintype α] [Nonempty α] [Finite β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (e : γ ≃ α × β) (f : α → M) : ((uniformOfFintype γ).realWeightedSum fun (x : γ) => f (e x).1) = (uniformOfFintype α).realWeightedSum f

A finite expectation against a uniform PMF marginalizes a function depending only on the first coordinate of a product equivalence.

theorem PMF.realWeightedSum_uniformOfFintype_equiv_snd {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [Nonempty γ] [Finite α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (e : γ ≃ α × β) (f : β → M) : ((uniformOfFintype γ).realWeightedSum fun (x : γ) => f (e x).2) = (uniformOfFintype β).realWeightedSum f

A finite expectation against a uniform PMF marginalizes a function depending only on the second coordinate of a product equivalence.

theorem PMF.realWeightedSum_uniformOfFintype_fst {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (f : α → M) : ((uniformOfFintype (α × β)).realWeightedSum fun (ab : α × β) => f ab.1) = (uniformOfFintype α).realWeightedSum f

A finite expectation against the uniform PMF on a product marginalizes a function depending only on the first coordinate.

theorem PMF.realWeightedSum_uniformOfFintype_snd {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (f : β → M) : ((uniformOfFintype (α × β)).realWeightedSum fun (ab : α × β) => f ab.2) = (uniformOfFintype β).realWeightedSum f

A finite expectation against the uniform PMF on a product marginalizes a function depending only on the second coordinate.

theorem PMF.realWeightedSum_map_uniformOfFintype_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_4} [Fintype α] [Fintype β] [Nonempty α] [Fintype γ] [Nonempty γ] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (m : α → β) (g : β → γ) (e : α ≃ γ) (h : ∀ (a : α), g (m a) = e a) (f : γ → M) : ((map m (uniformOfFintype α)).realWeightedSum fun (b : β) => f (g b)) = (uniformOfFintype γ).realWeightedSum f

A pushed-forward uniform PMF has the uniform expectation induced by an equivalent observed coordinate.

theorem PMF.realWeightedSum_map_uniformOfFintype_factor_equiv_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [Fintype α] [Fintype β] [Nonempty α] [Fintype γ] [Nonempty γ] [Finite δ] [Nonempty δ] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (m : α → β) (g : β → γ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).1) (f : γ → M) : ((map m (uniformOfFintype α)).realWeightedSum fun (b : β) => f (g b)) = (uniformOfFintype γ).realWeightedSum f

A pushed-forward uniform PMF has the first-coordinate uniform marginal when the seed is equivalent to a product.

theorem PMF.realWeightedSum_map_uniformOfFintype_factor_equiv_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [Fintype α] [Fintype β] [Nonempty α] [Finite γ] [Nonempty γ] [Fintype δ] [Nonempty δ] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (m : α → β) (g : β → δ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).2) (f : δ → M) : ((map m (uniformOfFintype α)).realWeightedSum fun (b : β) => f (g b)) = (uniformOfFintype δ).realWeightedSum f

A pushed-forward uniform PMF has the second-coordinate uniform marginal when the seed is equivalent to a product.