PMF-weighted finite expectation identities

This module contains finite expectation identities stated directly for Mathlib probability mass functions. They connect PMF.map and PMF.bind to the real-weighted finite sums used by the low individual degree test averaging layer.

Main declarations

• PMF.map_apply_toReal
• PMF.realWeightedSum
• PMF.realWeightedSumLinearMap
• PMF.realWeightedSum_map
• PMF.realWeightedSum_bind
• PMF.map_sum_smul
• PMF.bind_apply_toReal
• PMF.bind_sum_smul
• PMF.sum_toReal_eq_one
• PMF.sum_const_smul
• PMF.totalVariationDistance
• PMF.totalVariationDistance_eq_sum_max_sub
• PMF.totalVariationDistance_uniformOfFintype_uniformOfFinset_eq
• PMF.sum_le_sum_add_totalVariationDistance
• PMF.sum_rpow_one_div_le_rpow_sum
• PMF.realWeightedSum_rpow_one_div_le_rpow
• PMF.uniformOfFintype_map_equiv
• PMF.uniformOfFintype_prod_apply_toReal
• PMF.uniformOfFintype_prod_eq_bind
• PMF.uniformOfFintype_sum_equiv_smul
• PMF.uniformOfFintype_prod_sum_smul
• PMF.uniformOfFintype_sum_equiv_fst_smul
• PMF.uniformOfFintype_sum_equiv_snd_smul
• PMF.uniformOfFintype_sum_factor_equiv_smul
• PMF.uniformOfFintype_sum_factor_equiv_fst_smul
• PMF.uniformOfFintype_sum_factor_equiv_snd_smul

References

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

noncomputable def PMF.realWeightedSum {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (f : α → M) : M

The finite real-weighted expectation of a module-valued function against a probability mass function. This is the finite-sum form of expectation used in the low individual degree test, stated directly in Mathlib's PMF language.

Equations

• p.realWeightedSum f = ∑ a : α, (p a).toReal • f a

noncomputable def PMF.realWeightedSumLinearMap {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) : (α → M) →ₗ[MIPStarRE.LDT.Error] M

The finite PMF-weighted expectation as a linear map in the averaged family.

This is the linear form of PMF.realWeightedSum; it records that the probability weights are fixed and the averaged object varies linearly.

Equations

• p.realWeightedSumLinearMap = { toFun := fun (f : α → M) => p.realWeightedSum f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PMF.realWeightedSumLinearMap_apply {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (f : α → M) : p.realWeightedSumLinearMap f = p.realWeightedSum f

noncomputable def PMF.totalVariationDistance {α : Type u_1} [Fintype α] (p q : PMF α) : MIPStarRE.LDT.Error

The finite total-variation distance between two probability mass functions, written as half the L^1 distance between their real weights.

This is the PMF form of the finite total-variation comparison used in Proposition prop:ld-dnoteq of references/ldt-paper/ld-pasting.tex.

Equations

• p.totalVariationDistance q = 1 / 2 * ∑ a : α, |(p a).toReal - (q a).toReal|

theorem PMF.map_apply_toReal {α : Type u_1} {β : Type u_2} [Fintype α] (p : PMF α) (e : α → β) (b : β) : ((map e p) b).toReal = ∑ a : α, if b = e a then (p a).toReal else 0

Pointwise real-weight formula for a finite push-forward probability mass function. This is the finite real-valued form of PMF.map_apply.

theorem PMF.map_sum_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (e : α → β) (f : β → M) : ∑ b : β, ((map e p) b).toReal • f b = ∑ a : α, (p a).toReal • f (e a)

A finite PMF-weighted sum against a push-forward is the corresponding PMF-weighted sum of the pulled-back family.

theorem PMF.bind_apply_toReal {α : Type u_1} {β : Type u_2} [Fintype α] (p : PMF α) (q : α → PMF β) (b : β) : ((p.bind q) b).toReal = ∑ a : α, (p a).toReal * ((q a) b).toReal

Pointwise real-weight formula for a finite monadic composition of probability mass functions. This is the finite real-valued form of PMF.bind_apply.

theorem PMF.bind_sum_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (q : α → PMF β) (f : β → M) : ∑ b : β, ((p.bind q) b).toReal • f b = ∑ a : α, (p a).toReal • ∑ b : β, ((q a) b).toReal • f b

A finite PMF-weighted sum against a monadic composition is the iterated PMF-weighted sum.

theorem PMF.uniformOfFintype_prod_apply_toReal {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (a : α) (b : β) : ((uniformOfFintype (α × β)) (a, b)).toReal = ((uniformOfFintype α) a).toReal * ((uniformOfFintype β) b).toReal

The uniform probability mass on a product is the product of the two coordinate uniform masses, after coercion to real weights.

theorem PMF.uniformOfFintype_prod_eq_bind {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] : uniformOfFintype (α × β) = (uniformOfFintype α).bind fun (a : α) => map (fun (b : β) => (a, b)) (uniformOfFintype β)

The uniform probability mass function on a product is the monadic composition of the two coordinate-uniform probability mass functions.

theorem PMF.sum_toReal_eq_one {α : Type u_1} [Fintype α] (p : PMF α) : ∑ a : α, (p a).toReal = 1

The real weights of a finite probability mass function sum to one.

This is a Lean-only normalization lemma for transporting finite probability calculations to Mathlib's PMF language.

theorem PMF.sum_const_smul {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (x : M) : ∑ a : α, (p a).toReal • x = x

The PMF-weighted sum of a constant family is the constant value.

theorem PMF.sum_rpow_one_div_le_rpow_sum {α : Type u_1} [Fintype α] (p : PMF α) (f : α → MIPStarRE.LDT.Error) (n : ℕ) (hn : 1 ≤ n) (hf : ∀ (a : α), 0 ≤ f a) : ∑ a : α, (p a).toReal * Real.rpow (f a) (1 / ↑n) ≤ (∑ a : α, (p a).toReal * f a).rpow (1 / ↑n)

Jensen's inequality for the concave power x ↦ x ^ (1 / n), stated for a finite probability mass function.

theorem PMF.uniformOfFintype_map_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (e : α ≃ β) : map (⇑e) (uniformOfFintype α) = uniformOfFintype β

The uniform probability mass function is invariant under transport by an equivalence.

theorem PMF.uniformOfFintype_sum_equiv_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (e : α ≃ β) (f : α → M) : ∑ a : α, ((uniformOfFintype α) a).toReal • f a = ∑ b : β, ((uniformOfFintype β) b).toReal • f (e.symm b)

Reindex a finite sum weighted by Mathlib's uniform PMF along an equivalence.

theorem PMF.uniformOfFintype_prod_sum_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (f : α → β → M) : ∑ ab : α × β, ((uniformOfFintype (α × β)) ab).toReal • f ab.1 ab.2 = ∑ a : α, ((uniformOfFintype α) a).toReal • ∑ b : β, ((uniformOfFintype β) b).toReal • f a b

Split a finite sum weighted by the uniform PMF on a product into iterated uniform PMF-weighted sums.

theorem PMF.uniformOfFintype_sum_equiv_fst_smul {γ : 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) : ∑ x : γ, ((uniformOfFintype γ) x).toReal • f (e x).1 = ∑ a : α, ((uniformOfFintype α) a).toReal • f a

Marginalize a uniform PMF-weighted sum along the first coordinate of a product equivalence.

theorem PMF.uniformOfFintype_sum_equiv_snd_smul {γ : 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) : ∑ x : γ, ((uniformOfFintype γ) x).toReal • f (e x).2 = ∑ b : β, ((uniformOfFintype β) b).toReal • f b

Marginalize a uniform PMF-weighted sum along the second coordinate of a product equivalence.

theorem PMF.uniformOfFintype_sum_factor_equiv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_4} [Fintype α] [Nonempty α] [Fintype γ] [Nonempty γ] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (m : α → β) (g : β → γ) (e : α ≃ γ) (h : ∀ (a : α), g (m a) = e a) (f : γ → M) : ∑ a : α, ((uniformOfFintype α) a).toReal • f (g (m a)) = ∑ c : γ, ((uniformOfFintype γ) c).toReal • f c

A uniform PMF-weighted sum pushed forward through a map has the uniform average of an equivalent observed coordinate.

theorem PMF.uniformOfFintype_sum_factor_equiv_fst_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [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) : ∑ a : α, ((uniformOfFintype α) a).toReal • f (g (m a)) = ∑ c : γ, ((uniformOfFintype γ) c).toReal • f c

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

theorem PMF.uniformOfFintype_sum_factor_equiv_snd_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [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) : ∑ a : α, ((uniformOfFintype α) a).toReal • f (g (m a)) = ∑ d : δ, ((uniformOfFintype δ) d).toReal • f d

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

theorem PMF.realWeightedSum_map {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (e : α → β) (f : β → M) : (map e p).realWeightedSum f = p.realWeightedSum fun (a : α) => f (e a)

A finite PMF-weighted sum against a push-forward is the corresponding PMF-weighted sum of the pulled-back family.

theorem PMF.realWeightedSum_bind {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (q : α → PMF β) (f : β → M) : (p.bind q).realWeightedSum f = p.realWeightedSum fun (a : α) => (q a).realWeightedSum f

A finite PMF-weighted sum against a monadic composition is the corresponding iterated PMF-weighted sum.

theorem PMF.realWeightedSum_const {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module MIPStarRE.LDT.Error M] (p : PMF α) (x : M) : (p.realWeightedSum fun (x_1 : α) => x) = x

The finite PMF-weighted sum of a constant family is the constant value.

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

Reindex a finite expectation against Mathlib's uniform PMF along an equivalence.

theorem PMF.realWeightedSum_uniformOfFintype_prod {α : 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 (a : α) => (uniformOfFintype β).realWeightedSum fun (b : β) => f a b

Split a finite expectation against the uniform PMF on a product into iterated finite expectations against the coordinate-uniform PMFs.

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

A uniform finite expectation pushed forward through a map has the uniform expectation of an equivalent observed coordinate.

theorem PMF.realWeightedSum_uniformOfFintype_factor_equiv_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [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) : ((uniformOfFintype α).realWeightedSum fun (a : α) => f (g (m a))) = (uniformOfFintype γ).realWeightedSum f

A uniform finite expectation pushed forward through a map has the first coordinate uniform marginal when the seed is equivalent to a product.

theorem PMF.realWeightedSum_uniformOfFintype_factor_equiv_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [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) : ((uniformOfFintype α).realWeightedSum fun (a : α) => f (g (m a))) = (uniformOfFintype δ).realWeightedSum f

A uniform finite expectation pushed forward through a map has the second coordinate uniform marginal when the seed is equivalent to a product.

theorem PMF.totalVariationDistance_eq_sum_max_sub {α : Type u_1} [Fintype α] (p q : PMF α) : p.totalVariationDistance q = ∑ a : α, max 0 ((q a).toReal - (p a).toReal)

For finite probability mass functions, total variation is the total positive part of the signed weight difference q - p.

This is the finite PMF form of the elementary total-variation calculation used in Proposition prop:ld-dnoteq of references/ldt-paper/ld-pasting.tex.

theorem PMF.totalVariationDistance_uniformOfFintype_uniformOfFinset_eq {α : Type u_1} [Fintype α] [Nonempty α] (s : Finset α) (hs : s.Nonempty) : (uniformOfFintype α).totalVariationDistance (uniformOfFinset s hs) = 1 - ↑s.card / ↑(Fintype.card α)

Total variation between the uniform probability mass function on a finite ambient type and the uniform probability mass function on a nonempty finite subset.

This is the PMF form of the uniform-versus-conditioned-uniform calculation in Proposition prop:ld-dnoteq of references/ldt-paper/ld-pasting.tex.

theorem PMF.sum_le_sum_add_totalVariationDistance {α : Type u_1} [Fintype α] (p q : PMF α) (f : α → MIPStarRE.LDT.Error) (hf_nonneg : ∀ (a : α), 0 ≤ f a) (hf_le_one : ∀ (a : α), f a ≤ 1) : ∑ a : α, (q a).toReal * f a ≤ ∑ a : α, (p a).toReal * f a + p.totalVariationDistance q

A [0,1]-valued function has expectations over two finite probability mass functions differing by at most their total-variation distance.

This is the finite PMF comparison estimate used after Proposition prop:ld-dnoteq in references/ldt-paper/ld-pasting.tex.

theorem PMF.realWeightedSum_rpow_one_div_le_rpow {α : Type u_1} [Fintype α] (p : PMF α) (f : α → MIPStarRE.LDT.Error) (n : ℕ) (hn : 1 ≤ n) (hf : ∀ (a : α), 0 ≤ f a) : (p.realWeightedSum fun (a : α) => Real.rpow (f a) (1 / ↑n)) ≤ (p.realWeightedSum f).rpow (1 / ↑n)

Jensen's inequality for the concave power x ↦ x ^ (1 / n), stated for the finite expectation associated to a probability mass function.