The operator-valued average over a finite-support distribution

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/Distribution.lean.

The vendored file defines averageOperatorOverDistribution 𝒟 f = ∑ a ∈ 𝒟.support, 𝒟.weight a • f a for a family f of matrices MIPStarRE.Quantum.Op ι. The port needs it for two kinds of operators, the local ones (a C*-algebra 𝔓) and the joint ones (K →L[ℂ] K), so it is defined here for any real module R, and each lemma asks for exactly the structure its proof uses:

• the definition and the linear lemmas (_map, _congr, _sum, _finset_sum, _const): [AddCommMonoid R] [Module ℝ R];
• the order lemmas (_nonneg, _mono): in addition [PartialOrder R] [IsOrderedAddMonoid R] [PosSMulMono ℝ R];
• the bounds by the identity (_le_one_*): in addition [One R] [ZeroLEOneClass R] [SMulPosMono ℝ R].

Every C*-algebra with its order ([CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓]), in particular K →L[ℂ] K, has all of these instances, with Module ℝ the restriction of scalars of its complex structure. For K →L[ℂ] K this file also declares shortcut instances for the real scalars (see "Shortcut instances for the joint operators" below), because synthesizing those classes there is slow; they are scoped to MIPRE.LIDT.Co, so in force in every port file and nowhere else.

The classical part of the vendored file (Distribution, avgOver, the uniform distributions, the push-forward, toPMF, the total variation distance) is not ported: it is imported, and named through an explicit open MIPStarRE.LDT (…) list. The names below resolve, inside MIPRE.LIDT.Co, to the ported declarations, never to the vendored matrix ones.

Not ported

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

• Distribution: classical, imported.
• Distribution.totalWeight: classical, imported.
• Distribution.IsProbability: classical, imported.
• Distribution.map: classical, imported.
• Distribution.map_support: classical, imported.
• Distribution.map_weight: classical, imported.
• Distribution.map_totalWeight: classical, imported.
• Distribution.map_sum_smul: classical, imported.
• Distribution.sum_univ_eq_sum_support: classical, imported.
• Distribution.IsProbability.weight_sum_eq_one: classical, imported.
• Distribution.IsProbability.weight_sum_univ_eq_one: classical, imported.
• Distribution.IsProbability.weight_sum_le_one: classical, imported.
• Distribution.IsProbability.map: classical, imported.
• Distribution.toPMF: classical, imported.
• Distribution.toPMF_apply: classical, imported.
• Distribution.toPMF_apply_toReal: classical, imported.
• Distribution.toPMF_apply_of_notMem: classical, imported.
• Distribution.toPMF_map: classical, imported.
• avgOver: classical, imported.
• Distribution.weightedSumLinearMap: classical (generic in the module), imported.
• Distribution.weightedSumLinearMap_apply: classical, imported.
• Distribution.avgOver_eq_weightedSumLinearMap: classical, imported.
• Distribution.avgOver_map: classical, imported.
• Distribution.uniformOnFinset: classical, imported.
• Distribution.uniformOnFinset_support: classical, imported.
• Distribution.uniformOnFinset_weight: classical, imported.
• Distribution.uniformOnFinset_isProbability: classical, imported.
• Distribution.uniformOnFinset_weight_sum_le_one: classical, imported.
• Distribution.uniformOnFinset_toPMF: classical, imported.
• uniformDistribution: classical, imported.
• uniformDistribution_support: classical, imported.
• uniformDistribution_weight_sum_eq_one: classical, imported.
• uniformDistribution_isProbability: classical, imported.
• uniformDistribution_weight_sum_le_one: classical, imported.
• uniformDistribution_toPMF: classical, imported.
• totalVariationDistance: classical, imported.
• totalVariationDistance_eq_univ_sum: classical, imported.
• totalVariationDistance_eq_toPMF_sum: classical, imported.

Shortcut instances for the joint operators

Under the import of all of Mathlib that the vendored classical layer brings, synthesizing the real ordered-module structure of K →L[ℂ] K takes 0.6–1.9 s per class (PosSMulMono ℝ through Mathlib/Algebra/Order/Star/Basic.lean's IsOrderedModule instance for star-ordered rings, and IsScalarTower ℝ/SMulCommClass ℝ through Algebra.complexToReal), paid again at every use of an order lemma below on joint operators. These shortcuts, found first, cut such a use from about 2 s to 0.3 s. The real scalar structure itself is slow too: SMulZeroClass ℝ (reached through smul_nonneg) and Algebra ℝ (reached by simp [smul_mul_assoc]) take about 0.5 s each, and SMul ℝ 0.1 s at every elaboration of c • X with c : ℝ; their shortcuts carry data, but each is inferInstance, the instance the search finds anyway, so it is the same term and creates no diamond. The local C*-algebra 𝔓 does not need any of them (0.1–0.2 s per use).

They are scoped instances of MIPRE.LIDT.Co: in force in every file of the port (each works inside that namespace) and in no importer outside it. A new shortcut for the joint operators goes here.

@[instance_reducible]

noncomputable def MIPRE.LIDT.Co.instSMulRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] : SMul ℝ (K →L[ℂ] K)

Shortcut: the real scalar action on K →L[ℂ] K.

Equations

• MIPRE.LIDT.Co.instSMulRealCLM = inferInstance

@[instance_reducible]

noncomputable def MIPRE.LIDT.Co.instSMulZeroClassRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] : SMulZeroClass ℝ (K →L[ℂ] K)

Shortcut: the real scalar action on K →L[ℂ] K fixes zero.

Equations

• MIPRE.LIDT.Co.instSMulZeroClassRealCLM = inferInstance

@[instance_reducible]

noncomputable def MIPRE.LIDT.Co.instModuleRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] : Module ℝ (K →L[ℂ] K)

Shortcut: K →L[ℂ] K is a real vector space.

Equations

• MIPRE.LIDT.Co.instModuleRealCLM = inferInstance

@[instance_reducible]

noncomputable def MIPRE.LIDT.Co.instAlgebraRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] : Algebra ℝ (K →L[ℂ] K)

Shortcut: K →L[ℂ] K is a real algebra.

Equations

• MIPRE.LIDT.Co.instAlgebraRealCLM = inferInstance

theorem MIPRE.LIDT.Co.instIsScalarTowerRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] : IsScalarTower ℝ (K →L[ℂ] K) (K →L[ℂ] K)

Shortcut: real scalars associate with the product of K →L[ℂ] K.

theorem MIPRE.LIDT.Co.instSMulCommClassRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] : SMulCommClass ℝ (K →L[ℂ] K) (K →L[ℂ] K)

Shortcut: real scalars commute with the product of K →L[ℂ] K.

theorem MIPRE.LIDT.Co.instPosSMulMonoRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : PosSMulMono ℝ (K →L[ℂ] K)

Shortcut: real scalars act monotonically on the Loewner order of K →L[ℂ] K.

theorem MIPRE.LIDT.Co.instSMulPosMonoRealCLM {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : SMulPosMono ℝ (K →L[ℂ] K)

Shortcut: a nonnegative operator of K →L[ℂ] K scales monotonically in a real scalar.

noncomputable def MIPRE.LIDT.Co.averageOperatorOverDistribution {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (𝒟 : MIPStarRE.LDT.Distribution α) (f : α → R) : R

Weighted sum of operators over a distribution's finite support, using the same support/weight data as the scalar avgOver.

This is a project-local adapter around Mathlib finite sums for the LDT Distribution representation and the real scalar action on an operator space R (the local C*-algebra or K →L[ℂ] K), not a replacement for Mathlib's probability theory APIs.

Equations

• MIPRE.LIDT.Co.averageOperatorOverDistribution 𝒟 f = ∑ a ∈ 𝒟.support, 𝒟.weight a • f a

theorem MIPRE.LIDT.Co.Distribution.averageOperatorOverDistribution_eq_weightedSumLinearMap {α : Type u_1} (𝒟 : MIPStarRE.LDT.Distribution α) {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (f : α → R) : averageOperatorOverDistribution 𝒟 f = (MIPStarRE.LDT.Distribution.weightedSumLinearMap R 𝒟) f

Operator averaging is the weighted finite-sum linear map applied to an operator-valued family.

theorem MIPRE.LIDT.Co.Distribution.averageOperatorOverDistribution_map {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : MIPStarRE.LDT.Distribution α) (e : α → β) {R : Type u_3} [AddCommMonoid R] [Module ℝ R] (f : β → R) : averageOperatorOverDistribution (𝒟.map e) f = averageOperatorOverDistribution 𝒟 fun (a : α) => f (e a)

Operator-valued averaging against a pushed-forward distribution is operator-valued averaging of the pulled-back family against the original distribution.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_congr {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (𝒟 : MIPStarRE.LDT.Distribution α) (A B : α → R) (h : ∀ (a : α), A a = B a) : averageOperatorOverDistribution 𝒟 A = averageOperatorOverDistribution 𝒟 B

If two operator-valued families agree pointwise, their averages agree.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_sum {α : Type u_1} {β : Type u_2} [Fintype β] (𝒟 : MIPStarRE.LDT.Distribution α) {R : Type u_3} [AddCommMonoid R] [Module ℝ R] (f : α → β → R) : (averageOperatorOverDistribution 𝒟 fun (a : α) => ∑ b : β, f a b) = ∑ b : β, averageOperatorOverDistribution 𝒟 fun (a : α) => f a b

Pull a finite outcome sum through an operator-valued average.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_finset_sum {α : Type u_1} {β : Type u_2} (𝒟 : MIPStarRE.LDT.Distribution α) (s : Finset β) {R : Type u_3} [AddCommMonoid R] [Module ℝ R] (f : α → β → R) : (averageOperatorOverDistribution 𝒟 fun (a : α) => ∑ b ∈ s, f a b) = ∑ b ∈ s, averageOperatorOverDistribution 𝒟 fun (a : α) => f a b

Pull a finite-set outcome sum through an operator-valued average.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_nonneg {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] [PartialOrder R] [IsOrderedAddMonoid R] [PosSMulMono ℝ R] (𝒟 : MIPStarRE.LDT.Distribution α) (f : α → R) (hf : ∀ (a : α), 0 ≤ f a) : 0 ≤ averageOperatorOverDistribution 𝒟 f

Operator averages preserve positivity.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_mono {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] [PartialOrder R] [IsOrderedAddMonoid R] [PosSMulMono ℝ R] (𝒟 : MIPStarRE.LDT.Distribution α) (f g : α → R) (hfg : ∀ (a : α), f a ≤ g a) : averageOperatorOverDistribution 𝒟 f ≤ averageOperatorOverDistribution 𝒟 g

Operator averages preserve pointwise order.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_const {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (𝒟 : MIPStarRE.LDT.Distribution α) (A : R) : (averageOperatorOverDistribution 𝒟 fun (x : α) => A) = (∑ a ∈ 𝒟.support, 𝒟.weight a) • A

The average of a constant operator is the total mass times that operator.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_const_of_isProbability {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] (𝒟 : MIPStarRE.LDT.Distribution α) (h𝒟 : 𝒟.IsProbability) (A : R) : (averageOperatorOverDistribution 𝒟 fun (x : α) => A) = A

The average of a constant operator over a probability distribution is that operator.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_le_one_of_weight_sum_le_one {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] [PartialOrder R] [IsOrderedAddMonoid R] [PosSMulMono ℝ R] [SMulPosMono ℝ R] [One R] [ZeroLEOneClass R] (𝒟 : MIPStarRE.LDT.Distribution α) (f : α → R) (h𝒟 : ∑ a ∈ 𝒟.support, 𝒟.weight a ≤ 1) (hf : ∀ (a : α), f a ≤ 1) : averageOperatorOverDistribution 𝒟 f ≤ 1

An average of effects against a sub-probability distribution is again bounded above by the identity operator.

theorem MIPRE.LIDT.Co.averageOperatorOverDistribution_le_one_of_isProbability {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [Module ℝ R] [PartialOrder R] [IsOrderedAddMonoid R] [PosSMulMono ℝ R] [SMulPosMono ℝ R] [One R] [ZeroLEOneClass R] (𝒟 : MIPStarRE.LDT.Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → R) (hf : ∀ (a : α), f a ≤ 1) : averageOperatorOverDistribution 𝒟 f ≤ 1

An average of effects against a probability distribution is again bounded above by the identity operator.