PMF expectations of operator-valued averages

This is the counterpart, in the port of the low-individual-degree test to the symmetric model (planning/c6b-plan.md, milestone M0, and its section "Port conventions"), of the operator part of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/DistributionPMF.lean: the operator average averageOperatorOverDistribution against a probabilistic project distribution is the finite expectation PMF.realWeightedSum against the associated Mathlib probability mass function.

The operators live in any real module R ([AddCommMonoid R] [Module ℝ R]), as in MIPRE/Background/LIDT/Co/Basic/Distribution.lean.

Main declarations

• averageOperatorOverDistribution_eq_toPMF_realWeightedSum
• averageOperatorOverDistribution_uniform_eq_pmf_realWeightedSum

Not ported

The classical declarations of the vendored file, which this file imports:

• Distribution.weightedSumLinearMap_eq_toPMF_realWeightedSum: classical, imported.
• Distribution.weightedSumLinearMap_eq_toPMF_realWeightedSumLinearMap: classical, imported.
• avgOver_eq_toPMF_realWeightedSum: classical, imported.
• uniformDistribution_sum_smul_eq_pmf_realWeightedSum: classical, imported.
• avgOver_uniform_eq_pmf_realWeightedSum: classical, imported.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_eq_toPMF_realWeightedSum {α : Type u_1} [Fintype α] (𝒟 : MIPStarRE.LDT.Distribution α) (h𝒟 : 𝒟.IsProbability) {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (f : α → R) : 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 MIPRE.LIDT.Co.averageOperatorOverDistribution_uniform_eq_pmf_realWeightedSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (f : α → R) : averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) f = (PMF.uniformOfFintype α).realWeightedSum f

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