Distribution infrastructure for the low individual degree test

Shared distribution definitions: finite-support weighted distributions, a probability predicate, push-forward distributions, weighted-sum linear maps, averaging, uniform distribution, and outcome summation.

Note: this module contributes declarations to the comparator statement closure of mainFormal, which must elaborate in the same environment as the Mathlib-only Challenge.lean. Keep the full import Mathlib; do not narrow it. See docs/comparator.md, "Environment alignment".

structure MIPStarRE.LDT.Distribution (α : Type u_1) : Type u_1

A finite-support weighted distribution with nonnegative real-valued weights.

• support : Finset α
• weight : α → Error
• nonnegative (a : α) : 0 ≤ self.weight a
• outsideSupport (a : α) : a ∉ self.support → self.weight a = 0

def MIPStarRE.LDT.Distribution.totalWeight {α : Type u_1} (𝒟 : Distribution α) : Error

The total mass carried by the explicit support of a distribution.

Equations

• 𝒟.totalWeight = ∑ a ∈ 𝒟.support, 𝒟.weight a

def MIPStarRE.LDT.Distribution.IsProbability {α : Type u_1} (𝒟 : Distribution α) : Prop

A Distribution is probabilistic when its total mass is exactly 1.

Equations

• 𝒟.IsProbability = (𝒟.totalWeight = 1)

noncomputable def MIPStarRE.LDT.Distribution.map {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (e : α → β) : Distribution β

Push a finite-support distribution forward along a map.

This is the project Distribution analogue of PMF.map. The support is the image of the original finite support, and each new weight is the sum of the weights in the corresponding fiber.

Equations

• 𝒟.map e = { support := Finset.image e 𝒟.support, weight := fun (b : β) => ∑ a ∈ 𝒟.support with e a = b, 𝒟.weight a, nonnegative := ⋯, outsideSupport := ⋯ }

@[simp]

theorem MIPStarRE.LDT.Distribution.map_support {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (e : α → β) : (𝒟.map e).support = Finset.image e 𝒟.support

@[simp]

theorem MIPStarRE.LDT.Distribution.map_weight {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (e : α → β) (b : β) : (𝒟.map e).weight b = ∑ a ∈ 𝒟.support with e a = b, 𝒟.weight a

theorem MIPStarRE.LDT.Distribution.map_totalWeight {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (e : α → β) : (𝒟.map e).totalWeight = 𝒟.totalWeight

Push-forward preserves total mass.

theorem MIPStarRE.LDT.Distribution.map_sum_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} [DecidableEq β] [AddCommMonoid M] [Module Error M] (𝒟 : Distribution α) (e : α → β) (f : β → M) : ∑ b ∈ (𝒟.map e).support, (𝒟.map e).weight b • f b = ∑ a ∈ 𝒟.support, 𝒟.weight a • f (e a)

A finite weighted sum over a push-forward distribution is the corresponding weighted sum of the pulled-back family. This is the Distribution analogue of the finite-sum form of PMF.map.

theorem MIPStarRE.LDT.Distribution.sum_univ_eq_sum_support {α : Type u_1} {β : Type u_2} [Fintype α] [AddCommMonoid β] (𝒟 : Distribution α) (f : α → β) (hf : ∀ a ∉ 𝒟.support, f a = 0) : ∑ a : α, f a = ∑ a ∈ 𝒟.support, f a

On a finite ambient type, a summand that vanishes outside a distribution's explicit support has the same total sum over all ambient values as over that support.

This is a project-local explicit-support adapter around Mathlib's Finset.sum_subset: Mathlib supplies the finite-sum theorem, while this lemma packages the common shape used when paper expressions sum over a whole question set but the repository stores a smaller Distribution.support. It is not intended to replace Mathlib probability theory.

theorem MIPStarRE.LDT.Distribution.IsProbability.weight_sum_eq_one {α : Type u_1} {𝒟 : Distribution α} (h𝒟 : 𝒟.IsProbability) : ∑ a ∈ 𝒟.support, 𝒟.weight a = 1

Unpack the equality form of the probability invariant.

theorem MIPStarRE.LDT.Distribution.IsProbability.weight_sum_univ_eq_one {α : Type u_1} [Fintype α] {𝒟 : Distribution α} (h𝒟 : 𝒟.IsProbability) : ∑ a : α, 𝒟.weight a = 1

On a finite ambient type, a probabilistic Distribution has total weight 1 even when its weights are summed over the whole ambient type.

This packages the explicit-support bookkeeping in Distribution for downstream Lean statements that follow the paper's notation 𝔼_{x ∼ 𝒟} over the question set rather than over a stored support finset.

theorem MIPStarRE.LDT.Distribution.IsProbability.weight_sum_le_one {α : Type u_1} {𝒟 : Distribution α} (h𝒟 : 𝒟.IsProbability) : ∑ a ∈ 𝒟.support, 𝒟.weight a ≤ 1

A probability distribution has total weight at most 1.

theorem MIPStarRE.LDT.Distribution.IsProbability.map {α : Type u_1} {β : Type u_2} [DecidableEq β] {𝒟 : Distribution α} (h𝒟 : 𝒟.IsProbability) (e : α → β) : (𝒟.map e).IsProbability

Push-forward preserves the probability invariant.

noncomputable def MIPStarRE.LDT.Distribution.toPMF {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) : PMF α

The Mathlib probability mass function associated to a project Distribution whose total mass is one.

The construction sends each nonnegative real weight to ℝ≥0∞ by ENNReal.ofReal; the hypotheses of PMF.ofFinset are exactly the project probability invariant and the stored zero-off-support condition.

Equations

• 𝒟.toPMF h𝒟 = PMF.ofFinset (fun (a : α) => ENNReal.ofReal (𝒟.weight a)) 𝒟.support ⋯ ⋯

@[simp]

theorem MIPStarRE.LDT.Distribution.toPMF_apply {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (a : α) : (𝒟.toPMF h𝒟) a = ENNReal.ofReal (𝒟.weight a)

@[simp]

theorem MIPStarRE.LDT.Distribution.toPMF_apply_toReal {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (a : α) : ((𝒟.toPMF h𝒟) a).toReal = 𝒟.weight a

theorem MIPStarRE.LDT.Distribution.toPMF_apply_of_notMem {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) {a : α} (ha : a ∉ 𝒟.support) : (𝒟.toPMF h𝒟) a = 0

The associated PMF has zero mass outside the stored support of the project distribution.

theorem MIPStarRE.LDT.Distribution.toPMF_map {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (e : α → β) : (𝒟.map e).toPMF ⋯ = PMF.map e (𝒟.toPMF h𝒟)

The project push-forward agrees with Mathlib's push-forward of the associated probability mass function.

def MIPStarRE.LDT.avgOver {α : Type u_1} (𝒟 : Distribution α) (f : α → Error) : Error

Average a scalar function against the stored finite support of a distribution.

Equations

• MIPStarRE.LDT.avgOver 𝒟 f = ∑ a ∈ 𝒟.support, 𝒟.weight a * f a

noncomputable def MIPStarRE.LDT.Distribution.weightedSumLinearMap (M : Type u_1) [AddCommMonoid M] [Module Error M] {α : Type u_2} (𝒟 : Distribution α) : (α → M) →ₗ[Error] M

The module-valued weighted finite sum associated to a finite-support Distribution, as a linear map in the averaged family.

This packages the finite-support expression underlying both scalar averages and operator averages. It keeps the explicit support carried by Distribution, while exposing the Error-module structure of the weighted sum.

Equations

• MIPStarRE.LDT.Distribution.weightedSumLinearMap M 𝒟 = { toFun := fun (f : α → M) => ∑ a ∈ 𝒟.support, 𝒟.weight a • f a, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

theorem MIPStarRE.LDT.Distribution.avgOver_eq_weightedSumLinearMap {α : Type u_1} (𝒟 : Distribution α) (f : α → Error) : avgOver 𝒟 f = (weightedSumLinearMap Error 𝒟) f

The scalar average is the weighted finite-sum linear map applied to a scalar family.

theorem MIPStarRE.LDT.Distribution.avgOver_map {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (e : α → β) (f : β → Error) : avgOver (𝒟.map e) f = avgOver 𝒟 fun (a : α) => f (e a)

Averaging against a pushed-forward distribution is averaging the pulled-back function against the original distribution.

noncomputable def MIPStarRE.LDT.averageOperatorOverDistribution {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (f : α → Quantum.Op ι) : Quantum.Op ι

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 Quantum.Op scalar action, not a replacement for Mathlib's probability theory APIs.

Equations

• MIPStarRE.LDT.averageOperatorOverDistribution 𝒟 f = ∑ a ∈ 𝒟.support, 𝒟.weight a • f a

theorem MIPStarRE.LDT.Distribution.averageOperatorOverDistribution_eq_weightedSumLinearMap {α : Type u_1} (𝒟 : Distribution α) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution 𝒟 f = (weightedSumLinearMap (Quantum.Op ι) 𝒟) f

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

theorem MIPStarRE.LDT.Distribution.averageOperatorOverDistribution_map {α : Type u_1} {β : Type u_2} [DecidableEq β] (𝒟 : Distribution α) (e : α → β) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (f : β → Quantum.Op ι) : 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 MIPStarRE.LDT.averageOperatorOverDistribution_congr {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (A B : α → Quantum.Op ι) (h : ∀ (a : α), A a = B a) : averageOperatorOverDistribution 𝒟 A = averageOperatorOverDistribution 𝒟 B

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

theorem MIPStarRE.LDT.averageOperatorOverDistribution_sum {α : Type u_1} {β : Type u_2} [Fintype β] (𝒟 : Distribution α) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (f : α → β → Quantum.Op ι) : (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 MIPStarRE.LDT.averageOperatorOverDistribution_finset_sum {α : Type u_1} {β : Type u_2} (𝒟 : Distribution α) (s : Finset β) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (f : α → β → Quantum.Op ι) : (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 MIPStarRE.LDT.averageOperatorOverDistribution_nonneg {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (f : α → Quantum.Op ι) (hf : ∀ (a : α), 0 ≤ f a) : 0 ≤ averageOperatorOverDistribution 𝒟 f

Operator averages preserve positivity.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_mono {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (f g : α → Quantum.Op ι) (hfg : ∀ (a : α), f a ≤ g a) : averageOperatorOverDistribution 𝒟 f ≤ averageOperatorOverDistribution 𝒟 g

Operator averages preserve pointwise order.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_const {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (A : Quantum.Op ι) : (averageOperatorOverDistribution 𝒟 fun (x : α) => A) = (∑ a ∈ 𝒟.support, 𝒟.weight a) • A

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

theorem MIPStarRE.LDT.averageOperatorOverDistribution_const_of_isProbability {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (A : Quantum.Op ι) : (averageOperatorOverDistribution 𝒟 fun (x : α) => A) = A

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

theorem MIPStarRE.LDT.averageOperatorOverDistribution_le_one_of_weight_sum_le_one {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (f : α → Quantum.Op ι) (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 MIPStarRE.LDT.averageOperatorOverDistribution_le_one_of_isProbability {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → Quantum.Op ι) (hf : ∀ (a : α), f a ≤ 1) : averageOperatorOverDistribution 𝒟 f ≤ 1

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

noncomputable def MIPStarRE.LDT.Distribution.uniformOnFinset {α : Type u_1} (s : Finset α) : Distribution α

The uniform distribution on a specified finite support.

The stored support is s, and the weight of a point is the elementary finite uniform weight 1 / s.card on s and 0 off s. When the support is empty this gives the zero sub-probability distribution, matching the convention used for degenerate filtered supports in the LDT development.

Equations

• MIPStarRE.LDT.Distribution.uniformOnFinset s = { support := s, weight := fun (a : α) => if a ∈ s then 1 / ↑s.card else 0, nonnegative := ⋯, outsideSupport := ⋯ }

@[simp]

theorem MIPStarRE.LDT.Distribution.uniformOnFinset_support {α : Type u_1} (s : Finset α) : (uniformOnFinset s).support = s

@[simp]

theorem MIPStarRE.LDT.Distribution.uniformOnFinset_weight {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) : (uniformOnFinset s).weight a = if a ∈ s then 1 / ↑s.card else 0

theorem MIPStarRE.LDT.Distribution.uniformOnFinset_isProbability {α : Type u_1} (s : Finset α) (hs : s.Nonempty) : (uniformOnFinset s).IsProbability

A nonempty finite support gives a probability distribution.

theorem MIPStarRE.LDT.Distribution.uniformOnFinset_weight_sum_le_one {α : Type u_1} (s : Finset α) : ∑ a ∈ (uniformOnFinset s).support, (uniformOnFinset s).weight a ≤ 1

The uniform distribution on any finite support is a sub-probability distribution. It has mass 1 on nonempty support and mass 0 on empty support.

theorem MIPStarRE.LDT.Distribution.uniformOnFinset_toPMF {α : Type u_1} (s : Finset α) (hs : s.Nonempty) : (uniformOnFinset s).toPMF ⋯ = PMF.uniformOfFinset s hs

The project uniform distribution on a nonempty finite support is Mathlib's uniform probability mass function on that support.

noncomputable def MIPStarRE.LDT.uniformDistribution (α : Type u_1) [Fintype α] [DecidableEq α] [Nonempty α] : Distribution α

The uniform distribution on a nonempty finite type.

Equations

• MIPStarRE.LDT.uniformDistribution α = MIPStarRE.LDT.Distribution.uniformOnFinset Finset.univ

@[simp]

theorem MIPStarRE.LDT.uniformDistribution_support (α : Type u_1) [Fintype α] [DecidableEq α] [Nonempty α] : (uniformDistribution α).support = Finset.univ

The uniform distribution on a finite type has full support.

theorem MIPStarRE.LDT.uniformDistribution_weight_sum_eq_one (α : Type u_1) [Fintype α] [DecidableEq α] [Nonempty α] : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a = 1

The weights of a uniform distribution sum to exactly 1.

theorem MIPStarRE.LDT.uniformDistribution_isProbability (α : Type u_1) [Fintype α] [DecidableEq α] [Nonempty α] : (uniformDistribution α).IsProbability

The uniform distribution is a genuine probability distribution.

theorem MIPStarRE.LDT.uniformDistribution_weight_sum_le_one (α : Type u_1) [Fintype α] [DecidableEq α] [Nonempty α] : ∑ a ∈ (uniformDistribution α).support, (uniformDistribution α).weight a ≤ 1

The weights of a uniform distribution sum to at most 1.

theorem MIPStarRE.LDT.uniformDistribution_toPMF (α : Type u_1) [Fintype α] [DecidableEq α] [Nonempty α] : (uniformDistribution α).toPMF ⋯ = PMF.uniformOfFintype α

The project uniform distribution on a nonempty finite type is Mathlib's uniform probability mass function on that type.

noncomputable def MIPStarRE.LDT.totalVariationDistance {α : Type u_1} [DecidableEq α] (μ ν : Distribution α) : Error

Total variation distance between two distributions: TV(μ, ν) = ½ ∑_a |μ(a) - ν(a)| over the union of supports.

Equations

• MIPStarRE.LDT.totalVariationDistance μ ν = 1 / 2 * ∑ a ∈ μ.support ∪ ν.support, |μ.weight a - ν.weight a|

theorem MIPStarRE.LDT.totalVariationDistance_eq_univ_sum {α : Type u_1} [Fintype α] [DecidableEq α] (μ ν : Distribution α) : totalVariationDistance μ ν = 1 / 2 * ∑ a : α, |μ.weight a - ν.weight a|

On a finite ambient type, the local total-variation distance may be summed over all points rather than over the union of the stored supports.

theorem MIPStarRE.LDT.totalVariationDistance_eq_toPMF_sum {α : Type u_1} [Fintype α] [DecidableEq α] (μ ν : Distribution α) (hμ : μ.IsProbability) (hν : ν.IsProbability) : totalVariationDistance μ ν = 1 / 2 * ∑ a : α, |((μ.toPMF hμ) a).toReal - ((ν.toPMF hν) a).toReal|

For probability distributions on a finite ambient type, the local total-variation distance is the half L^1 distance between the associated Mathlib probability mass functions.