PMF expectations associated to project distributions

This module relates the project Distribution averaging notation to the finite expectation PMF.realWeightedSum on Mathlib probability mass functions. The statements keep the project-facing averages available while allowing later probability arguments to cite the associated Mathlib PMF object directly. The module-valued finite-sum algebra for uniform project distributions lives in MIPStarRE.LDT.Basic.DistributionUniformSums; this file records the additional comparison with PMF.realWeightedSum.

Main declarations

• avgOver_eq_toPMF_realWeightedSum
• averageOperatorOverDistribution_eq_toPMF_realWeightedSum
• Distribution.weightedSumLinearMap_eq_toPMF_realWeightedSum
• Distribution.weightedSumLinearMap_eq_toPMF_realWeightedSumLinearMap
• uniformDistribution_sum_smul_eq_pmf_realWeightedSum
• avgOver_uniform_eq_pmf_realWeightedSum
• averageOperatorOverDistribution_uniform_eq_pmf_realWeightedSum

References

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

theorem MIPStarRE.LDT.Distribution.weightedSumLinearMap_eq_toPMF_realWeightedSum {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module Error M] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → M) : (weightedSumLinearMap M 𝒟) f = (𝒟.toPMF h𝒟).realWeightedSum f

The module-valued weighted sum against a probabilistic Distribution agrees with finite expectation against its associated Mathlib probability mass function.

theorem MIPStarRE.LDT.Distribution.weightedSumLinearMap_eq_toPMF_realWeightedSumLinearMap {α : Type u_1} {M : Type u_2} [Fintype α] [AddCommMonoid M] [Module Error M] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) : weightedSumLinearMap M 𝒟 = (𝒟.toPMF h𝒟).realWeightedSumLinearMap

The weighted-sum linear map of a probabilistic Distribution is the finite-expectation linear map of its associated Mathlib probability mass function.

theorem MIPStarRE.LDT.avgOver_eq_toPMF_realWeightedSum {α : Type u_1} [Fintype α] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → Error) : avgOver 𝒟 f = (𝒟.toPMF h𝒟).realWeightedSum f

Averaging against a probabilistic project distribution is the finite expectation against its associated Mathlib probability mass function.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_eq_toPMF_realWeightedSum {α : Type u_1} [Fintype α] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution 𝒟 f = (𝒟.toPMF h𝒟).realWeightedSum f

Operator-valued averaging against a probabilistic project distribution is the finite expectation against its associated Mathlib probability mass function.

theorem MIPStarRE.LDT.uniformDistribution_sum_smul_eq_pmf_realWeightedSum {α : 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 = (PMF.uniformOfFintype α).realWeightedSum f

Module-valued finite expectation for the uniform distribution, stated directly in terms of Mathlib's uniform probability mass function.

theorem MIPStarRE.LDT.avgOver_uniform_eq_pmf_realWeightedSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (f : α → Error) : avgOver (uniformDistribution α) f = (PMF.uniformOfFintype α).realWeightedSum f

The uniform average is the finite expectation against Mathlib's uniform probability mass function.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_eq_pmf_realWeightedSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (uniformDistribution α) f = (PMF.uniformOfFintype α).realWeightedSum f

The uniform operator average is the finite expectation against Mathlib's uniform probability mass function.