Module-valued uniform finite sums for project distributions

This module contains the module-valued finite-sum algebra for the project Distribution type. The statements keep the paper-facing uniformDistribution notation, but their proofs reduce the probability calculation to the finite-expectation API for Mathlib probability mass functions.

Main declarations

• Distribution.sum_smul_eq_toPMF_support_sum
• Distribution.sum_smul_eq_toPMF_sum
• uniformDistribution_sum_smul_eq_pmf_sum
• uniformDistribution_sum_smul_equiv
• uniformDistribution_sum_smul_prod
• uniformDistribution_sum_smul_comm
• uniformDistribution_sum_smul_prod_swap
• uniformDistribution_sum_smul_equiv_prod
• uniformDistribution_sum_smul_equiv_fst
• uniformDistribution_sum_smul_equiv_snd
• uniformDistribution_map_sum_smul_eq_uniform_of_factor_equiv
• uniformOnFinset_sum_smul_eq_subtype
• uniformOnFinset_filter_sum_smul_equiv

References

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

theorem MIPStarRE.LDT.Distribution.sum_smul_eq_toPMF_support_sum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Module Error M] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → M) : ∑ a ∈ 𝒟.support, 𝒟.weight a • f a = ∑ a ∈ 𝒟.support, ((𝒟.toPMF h𝒟) a).toReal • f a

A module-valued finite weighted sum against a probabilistic project distribution may be written with the real weights of the associated Mathlib probability mass function, over the stored support.

theorem MIPStarRE.LDT.Distribution.sum_smul_eq_toPMF_sum {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module Error M] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → M) : ∑ a ∈ 𝒟.support, 𝒟.weight a • f a = ∑ a : α, ((𝒟.toPMF h𝒟) a).toReal • f a

A module-valued finite weighted sum against a probabilistic project distribution may be written as a full finite sum with the real weights of the associated Mathlib probability mass function.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_eq_pmf_sum {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [AddCommMonoid M] [Module Error M] (f : α → M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f a = ∑ a : α, ((PMF.uniformOfFintype α) a).toReal • f a

Module-valued finite-sum expression for the uniform distribution, stated without measurable-space assumptions.

theorem MIPStarRE.LDT.uniformOnFinset_sum_smul_eq_pmf_sum {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [Module Error M] (s : Finset α) (hs : s.Nonempty) (f : α → M) : ∑ a ∈ (Distribution.uniformOnFinset s).support, (Distribution.uniformOnFinset s).weight a • f a = ∑ a ∈ s, ((PMF.uniformOfFinset s hs) a).toReal • f a

A finite-support uniform weighted sum is the corresponding Mathlib uniform PMF-weighted sum.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_const {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [AddCommMonoid M] [Module Error M] (x : M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • x = x

A constant family has uniform module-valued average equal to that constant. This is the project-distribution form of PMF.sum_const_smul.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_equiv {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (e : α ≃ β) (f : α → M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f a = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f (e.symm b)

Reindex a uniform module-valued average along an equivalence.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_prod {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (f : α → β → M) : ∑ ab ∈ (uniformDistribution (α × β)).support, (uniformDistribution (α × β)).weight ab • f ab.1 ab.2 = ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f a b

Split a uniform module-valued average over a product into iterated uniform module-valued averages.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_comm {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (f : α → β → M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f a b = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f a b

Swap two nested uniform module-valued averages over finite nonempty types.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_prod_swap {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (f : α → β → M) : ∑ ab ∈ (uniformDistribution (α × β)).support, (uniformDistribution (α × β)).weight ab • f ab.1 ab.2 = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f a b

Split a uniform module-valued average over a product into iterated uniform module-valued averages, with the second coordinate averaged first.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_equiv_prod {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (e : γ ≃ α × β) (f : γ → M) : ∑ x ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight x • f x = ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f (e.symm (a, b))

Transport a uniform module-valued average through an equivalence whose target is a product, then split the product average.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_equiv_prod_swap {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (e : γ ≃ α × β) (f : γ → M) : ∑ x ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight x • f x = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f (e.symm (a, b))

Transport a uniform module-valued average through an equivalence whose target is a product, then split the product average in the other order.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_equiv_fst {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Fintype α] [DecidableEq α] [Nonempty α] [Finite β] [Nonempty β] [AddCommMonoid M] [Module Error M] (e : γ ≃ α × β) (f : α → M) : ∑ x ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight x • f (e x).1 = ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f a

A function depending only on the first coordinate of a product equivalence has the first-coordinate uniform module-valued marginal.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_equiv_snd {γ : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Finite α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (e : γ ≃ α × β) (f : β → M) : ∑ x ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight x • f (e x).2 = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f b

A function depending only on the second coordinate of a product equivalence has the second-coordinate uniform module-valued marginal.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype γ] [DecidableEq γ] [Nonempty γ] [AddCommMonoid M] [Module Error M] (m : α → β) (g : β → γ) (e : α ≃ γ) (h : ∀ (a : α), g (m a) = e a) (f : γ → M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f (g (m a)) = ∑ c ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight c • f c

A uniformly sampled seed has the uniform module-valued average of an equivalent observed coordinate.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_factor_equiv_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype γ] [DecidableEq γ] [Nonempty γ] [Finite δ] [Nonempty δ] [AddCommMonoid M] [Module Error M] (m : α → β) (g : β → γ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).1) (f : γ → M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f (g (m a)) = ∑ c ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight c • f c

A uniformly sampled seed has the first-coordinate uniform module-valued marginal when the observed coordinate factors through a product equivalence.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_factor_equiv_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Finite γ] [Nonempty γ] [Fintype δ] [DecidableEq δ] [Nonempty δ] [AddCommMonoid M] [Module Error M] (m : α → β) (g : β → δ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).2) (f : δ → M) : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a • f (g (m a)) = ∑ d ∈ (uniformDistribution δ).support, (uniformDistribution δ).weight d • f d

A uniformly sampled seed has the second-coordinate uniform module-valued marginal when the observed coordinate factors through a product equivalence.

theorem MIPStarRE.LDT.uniformDistribution_map_sum_smul_eq_uniform_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [AddCommMonoid M] [Module Error M] (m : α → β) (g : β → γ) (e : α ≃ γ) (h : ∀ (a : α), g (m a) = e a) (f : γ → M) : ∑ b ∈ ((uniformDistribution α).map m).support, ((uniformDistribution α).map m).weight b • f (g b) = ∑ c ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight c • f c

A uniform push-forward has the uniform module-valued average induced by an equivalent observed coordinate.

theorem MIPStarRE.LDT.uniformDistribution_map_sum_smul_eq_uniform_fst_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [Finite δ] [Nonempty δ] [AddCommMonoid M] [Module Error M] (m : α → β) (g : β → γ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).1) (f : γ → M) : ∑ b ∈ ((uniformDistribution α).map m).support, ((uniformDistribution α).map m).weight b • f (g b) = ∑ c ∈ (uniformDistribution γ).support, (uniformDistribution γ).weight c • f c

A uniform push-forward has the first-coordinate uniform module-valued marginal when the observed coordinate factors through a product equivalence.

theorem MIPStarRE.LDT.uniformDistribution_map_sum_smul_eq_uniform_snd_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {M : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Finite γ] [Nonempty γ] [Fintype δ] [DecidableEq δ] [Nonempty δ] [AddCommMonoid M] [Module Error M] (m : α → β) (g : β → δ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).2) (f : δ → M) : ∑ b ∈ ((uniformDistribution α).map m).support, ((uniformDistribution α).map m).weight b • f (g b) = ∑ d ∈ (uniformDistribution δ).support, (uniformDistribution δ).weight d • f d

A uniform push-forward has the second-coordinate uniform module-valued marginal when the observed coordinate factors through a product equivalence.

theorem MIPStarRE.LDT.uniformOnFinset_sum_smul_eq_subtype {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] [Module Error M] (s : Finset α) [Nonempty ↥s] (f : α → M) : ∑ a ∈ (Distribution.uniformOnFinset s).support, (Distribution.uniformOnFinset s).weight a • f a = ∑ a ∈ (uniformDistribution ↥s).support, (uniformDistribution ↥s).weight a • f ↑a

A finite-support uniform module-valued average is the corresponding uniform average over the support subtype.

theorem MIPStarRE.LDT.uniformOnFinset_sum_smul_equiv {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (s : Finset α) (e : β ≃ ↥s) (f : α → M) : ∑ a ∈ (Distribution.uniformOnFinset s).support, (Distribution.uniformOnFinset s).weight a • f a = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f ↑(e b)

A finite-support uniform module-valued average may be reindexed by any finite type equivalent to the support subtype.

theorem MIPStarRE.LDT.uniformOnFinset_filter_sum_smul_eq_subtype {α : Type u_1} {M : Type u_2} [Fintype α] [DecidableEq α] (p : α → Prop) [DecidablePred p] [Nonempty { a : α // p a }] [AddCommMonoid M] [Module Error M] (f : α → M) : ∑ a ∈ (Distribution.uniformOnFinset (Finset.filter p Finset.univ)).support, (Distribution.uniformOnFinset (Finset.filter p Finset.univ)).weight a • f a = ∑ a ∈ (uniformDistribution { a : α // p a }).support, (uniformDistribution { a : α // p a }).weight a • f ↑a

A uniform module-valued average over a filtered finite support is the uniform average over the finite subtype satisfying the predicate.

theorem MIPStarRE.LDT.uniformOnFinset_filter_sum_smul_equiv {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype β] [DecidableEq β] [Nonempty β] [AddCommMonoid M] [Module Error M] (e : β ≃ { a : α // p a }) (f : α → M) : ∑ a ∈ (Distribution.uniformOnFinset (Finset.filter p Finset.univ)).support, (Distribution.uniformOnFinset (Finset.filter p Finset.univ)).weight a • f a = ∑ b ∈ (uniformDistribution β).support, (uniformDistribution β).weight b • f ↑(e b)

A uniform module-valued average over a filtered finite type may be reindexed by any finite seed type equivalent to the predicate subtype.