Average lemmas for finite-support distributions

This module contains the finite-sum and uniform-average lemmas for the project Distribution type. The primitive distribution definitions, uniform distributions, and total variation distance live in MIPStarRE.LDT.Basic.Distribution.

Main declarations

The main results are the algebraic rules for avgOver, scalar and operator-valued forms of the module-valued finite-sum rules for uniform distributions, and the comparison between finite uniform averages and Mathlib uniform probability mass functions.

References

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

Averaging infrastructure

Linearity proofs use Distribution.weightedSumLinearMap; order and support estimates use Mathlib's Finset.sum API.

theorem MIPStarRE.LDT.avgOver_zero {α : Type u_1} (𝒟 : Distribution α) : (avgOver 𝒟 fun (x : α) => 0) = 0

Averaging the zero function gives zero.

theorem MIPStarRE.LDT.avgOver_mono {α : Type u_1} (𝒟 : Distribution α) (f g : α → Error) (hfg : ∀ (a : α), f a ≤ g a) : avgOver 𝒟 f ≤ avgOver 𝒟 g

Averaging preserves order when weights are nonneg.

theorem MIPStarRE.LDT.avgOver_nonneg {α : Type u_1} (𝒟 : Distribution α) (f : α → Error) (hf : ∀ (a : α), 0 ≤ f a) : 0 ≤ avgOver 𝒟 f

Averaging a nonneg function with nonneg weights gives a nonneg result.

theorem MIPStarRE.LDT.avgOver_add {α : Type u_1} (𝒟 : Distribution α) (f g : α → Error) : (avgOver 𝒟 fun (a : α) => f a + g a) = avgOver 𝒟 f + avgOver 𝒟 g

Averaging distributes over addition.

theorem MIPStarRE.LDT.avgOver_sub {α : Type u_1} (𝒟 : Distribution α) (f g : α → Error) : (avgOver 𝒟 fun (a : α) => f a - g a) = avgOver 𝒟 f - avgOver 𝒟 g

Averaging distributes over subtraction.

theorem MIPStarRE.LDT.avgOver_const_mul {α : Type u_1} (𝒟 : Distribution α) (c : Error) (f : α → Error) : (avgOver 𝒟 fun (a : α) => c * f a) = c * avgOver 𝒟 f

Averaging commutes with scalar multiplication.

theorem MIPStarRE.LDT.avgOver_mul_const {α : Type u_1} (𝒟 : Distribution α) (f : α → Error) (c : Error) : (avgOver 𝒟 fun (a : α) => f a * c) = avgOver 𝒟 f * c

Averaging commutes with scalar multiplication on the right.

theorem MIPStarRE.LDT.avgOver_sum {α : Type u_1} {β : Type u_2} [Fintype β] (𝒟 : Distribution α) (f : α → β → Error) : (avgOver 𝒟 fun (a : α) => ∑ b : β, f a b) = ∑ b : β, avgOver 𝒟 fun (a : α) => f a b

Pull a finite outcome sum through an average.

theorem MIPStarRE.LDT.avgOver_finset_sum {α : Type u_1} {β : Type u_2} (𝒟 : Distribution α) (s : Finset β) (f : α → β → Error) : (avgOver 𝒟 fun (a : α) => ∑ b ∈ s, f a b) = ∑ b ∈ s, avgOver 𝒟 fun (a : α) => f a b

Pull a finite-set sum through an average.

theorem MIPStarRE.LDT.avgOver_comm {α : Type u_1} {β : Type u_2} (𝒟α : Distribution α) (𝒟β : Distribution β) (f : α → β → Error) : (avgOver 𝒟α fun (a : α) => avgOver 𝒟β (f a)) = avgOver 𝒟β fun (b : β) => avgOver 𝒟α fun (a : α) => f a b

Fubini swap for two nested finite-support distribution averages.

theorem MIPStarRE.LDT.avgOver_congr {α : Type u_1} (𝒟 : Distribution α) (f g : α → Error) (h : ∀ (a : α), f a = g a) : avgOver 𝒟 f = avgOver 𝒟 g

If f = g pointwise, their averages agree.

theorem MIPStarRE.LDT.avgOver_congr_on_support {α : Type u_1} (𝒟 : Distribution α) (f g : α → Error) (h : ∀ a ∈ 𝒟.support, f a = g a) : avgOver 𝒟 f = avgOver 𝒟 g

If two scalar functions agree on a distribution's explicit support, their averages agree. This support-restricted form is useful for distributions whose support carries an invariant not available for all ambient values.

theorem MIPStarRE.LDT.avgOver_mono_on_support {α : Type u_1} (𝒟 : Distribution α) (f g : α → Error) (h : ∀ a ∈ 𝒟.support, f a ≤ g a) : avgOver 𝒟 f ≤ avgOver 𝒟 g

Averaging preserves supportwise order when weights are nonnegative. This is the support-restricted analogue of avgOver_mono.

theorem MIPStarRE.LDT.avgOver_const {α : Type u_1} (𝒟 : Distribution α) (c : Error) : (avgOver 𝒟 fun (x : α) => c) = (∑ a ∈ 𝒟.support, 𝒟.weight a) * c

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

theorem MIPStarRE.LDT.avgOver_const_of_isProbability {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (c : Error) : (avgOver 𝒟 fun (x : α) => c) = c

Averaging a constant against a probability distribution returns that constant.

theorem MIPStarRE.LDT.avgOver_le_of_weight_sum_le_one {α : Type u_1} (𝒟 : Distribution α) (f : α → Error) (δ : Error) (h𝒟 : ∑ a ∈ 𝒟.support, 𝒟.weight a ≤ 1) (hδ_nonneg : 0 ≤ δ) (hf : ∀ (a : α), f a ≤ δ) : avgOver 𝒟 f ≤ δ

A scalar average against a sub-probability distribution is bounded by any nonnegative pointwise upper bound.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_mul_left_right {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (𝒟 : Distribution α) (L R : Quantum.Op ι) (A : α → Quantum.Op ι) : (averageOperatorOverDistribution 𝒟 fun (a : α) => L * A a * R) = L * averageOperatorOverDistribution 𝒟 A * R

Fixed left and right multiplications factor through an operator average.

theorem MIPStarRE.LDT.avgOver_eq_toPMF_support_sum {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → Error) : avgOver 𝒟 f = ∑ a ∈ 𝒟.support, ((𝒟.toPMF h𝒟) a).toReal * f a

Averaging against a probabilistic project distribution is the finite sum over its stored support against the associated Mathlib probability mass function.

theorem MIPStarRE.LDT.avgOver_eq_toPMF_sum {α : Type u_1} [Fintype α] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → Error) : avgOver 𝒟 f = ∑ a : α, ((𝒟.toPMF h𝒟) a).toReal * f a

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

theorem MIPStarRE.LDT.avgOver_eq_toPMF_integral {α : Type u_1} [Finite α] [MeasurableSpace α] [MeasurableSingletonClass α] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) (f : α → Error) : avgOver 𝒟 f = ∫ (a : α), f a ∂(𝒟.toPMF h𝒟).toMeasure

Averaging against a probabilistic project distribution is integration against its associated Mathlib probability mass function.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_eq_toPMF_support_sum {α : Type u_1} (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution 𝒟 f = ∑ a ∈ 𝒟.support, ((𝒟.toPMF h𝒟) a).toReal • f a

Operator-valued averaging against a probabilistic project distribution is the finite operator sum over the stored support against the associated Mathlib probability mass function.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_eq_toPMF_sum {α : Type u_1} [Fintype α] (𝒟 : Distribution α) (h𝒟 : 𝒟.IsProbability) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution 𝒟 f = ∑ a : α, ((𝒟.toPMF h𝒟) a).toReal • f a

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

theorem MIPStarRE.LDT.Distribution.IsProbability.avgOver_le_of_forall_le_on_support {α : Type u_1} {𝒟 : Distribution α} (h𝒟 : 𝒟.IsProbability) (f : α → Error) (δ : Error) (hf : ∀ a ∈ 𝒟.support, f a ≤ δ) : avgOver 𝒟 f ≤ δ

A supportwise upper bound also bounds the average of a probability distribution. This packages the paper convention that expectations are taken against genuine probability distributions, while still allowing Distribution itself to carry a larger ambient type than its explicit support.

theorem MIPStarRE.LDT.totalVariationDistance_eq_sum_max_sub {α : Type u_1} [DecidableEq α] (μ ν : Distribution α) (hμ : μ.IsProbability) (hν : ν.IsProbability) : totalVariationDistance μ ν = ∑ a ∈ μ.support ∪ ν.support, max 0 (ν.weight a - μ.weight a)

For two probability distributions, total variation is the total positive part of the signed weight difference ν - μ.

This is the finite-distribution identity (1 / 2) * ∑ |μ(a)-ν(a)| = ∑ max 0 (ν(a)-μ(a)), written for the project Distribution representation.

theorem MIPStarRE.LDT.avgOver_le_avgOver_add_totalVariationDistance {α : Type u_1} [DecidableEq α] (μ ν : Distribution α) (hμ : μ.IsProbability) (hν : ν.IsProbability) (f : α → Error) (hf_nonneg : ∀ (a : α), 0 ≤ f a) (hf_le_one : ∀ (a : α), f a ≤ 1) : avgOver ν f ≤ avgOver μ f + totalVariationDistance μ ν

A [0,1]-valued function has expectations over two probability distributions differing by at most their total variation distance.

The statement is oriented for replacement estimates: averaging against ν is bounded by averaging against μ, plus the finite total-variation distance between the two distributions.

theorem MIPStarRE.LDT.avgOver_uniform_const {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (c : Error) : (avgOver (uniformDistribution α) fun (x : α) => c) = c

Averaging a constant against the uniform distribution on a nonempty finite type returns that constant.

theorem MIPStarRE.LDT.avgOver_uniform_eq_pmf_sum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (f : α → Error) : avgOver (uniformDistribution α) f = ∑ a : α, ((PMF.uniformOfFintype α) a).toReal * f a

Finite-sum expression for the uniform average, stated without measurable-space assumptions.

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_eq_pmf_sum {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (f : α → Error) : avgOver (Distribution.uniformOnFinset s) f = ∑ a ∈ s, ((PMF.uniformOfFinset s hs) a).toReal * f a

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

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_eq_pmf_integral {α : Type u_1} [Finite α] [MeasurableSpace α] [MeasurableSingletonClass α] (s : Finset α) (hs : s.Nonempty) (f : α → Error) : avgOver (Distribution.uniformOnFinset s) f = ∫ (a : α), f a ∂(PMF.uniformOfFinset s hs).toMeasure

A finite-support uniform average is the finite integral with respect to the corresponding Mathlib uniform probability mass function.

theorem MIPStarRE.LDT.avgOver_uniform_eq_pmf_integral {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (f : α → Error) : avgOver (uniformDistribution α) f = ∫ (a : α), f a ∂(PMF.uniformOfFintype α).toMeasure

The uniform average with respect to uniformDistribution is the finite integral with respect to the uniform probability mass function.

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_eq_subtype {α : Type u_1} [DecidableEq α] (s : Finset α) [Nonempty ↥s] (f : α → Error) : avgOver (Distribution.uniformOnFinset s) f = avgOver (uniformDistribution ↥s) fun (a : ↥s) => f ↑a

A uniform average over a finite support is the same as the uniform average over the corresponding finite subtype.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_eq_pmf_sum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (uniformDistribution α) f = ∑ a : α, ((PMF.uniformOfFintype α) a).toReal • f a

The uniform operator average is the finite operator sum weighted by PMF.uniformOfFintype.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniformOnFinset_eq_pmf_sum {α : Type u_1} (s : Finset α) (hs : s.Nonempty) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (Distribution.uniformOnFinset s) f = ∑ a ∈ s, ((PMF.uniformOfFinset s hs) a).toReal • f a

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

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (e : α ≃ β) (f : α → Quantum.Op ι) : averageOperatorOverDistribution (uniformDistribution α) f = averageOperatorOverDistribution (uniformDistribution β) fun (b : β) => f (e.symm b)

Reindexing a uniform operator average along an equivalence preserves its value.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniformOnFinset_eq_subtype {α : Type u_1} [DecidableEq α] (s : Finset α) [Nonempty ↥s] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (Distribution.uniformOnFinset s) f = averageOperatorOverDistribution (uniformDistribution ↥s) fun (a : ↥s) => f ↑a

A uniform operator average over a finite support is the same as the uniform operator average over the corresponding finite subtype.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniformOnFinset_equiv {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq β] [Nonempty β] (s : Finset α) (e : β ≃ ↥s) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (Distribution.uniformOnFinset s) f = averageOperatorOverDistribution (uniformDistribution β) fun (b : β) => f ↑(e b)

A uniform operator average over a finite support may be reindexed by any finite type equivalent to that support subtype.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniformOnFinset_filter_eq_subtype {α : Type u_1} [Fintype α] [DecidableEq α] (p : α → Prop) [DecidablePred p] [Nonempty { a : α // p a }] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (Distribution.uniformOnFinset (Finset.filter p Finset.univ)) f = averageOperatorOverDistribution (uniformDistribution { a : α // p a }) fun (a : { a : α // p a }) => f ↑a

A uniform operator average over a filtered finite support is the uniform operator average over the finite subtype satisfying the predicate.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniformOnFinset_filter_equiv {α : Type u_1} {β : Type u_2} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype β] [DecidableEq β] [Nonempty β] (e : β ≃ { a : α // p a }) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) : averageOperatorOverDistribution (Distribution.uniformOnFinset (Finset.filter p Finset.univ)) f = averageOperatorOverDistribution (uniformDistribution β) fun (b : β) => f ↑(e b)

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

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_le_one {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (f : α → Quantum.Op ι) (hf : ∀ (a : α), f a ≤ 1) : averageOperatorOverDistribution (uniformDistribution α) f ≤ 1

A uniform average of effects is again bounded above by the identity operator.

theorem MIPStarRE.LDT.avgOver_uniform_le_of_forall_le_on_support {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (f : α → Error) (δ : Error) (hf : ∀ a ∈ (uniformDistribution α).support, f a ≤ δ) : avgOver (uniformDistribution α) f ≤ δ

A uniform average is bounded by any supportwise upper bound.

theorem MIPStarRE.LDT.avgOver_uniform_le_const {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (f : α → Error) (δ : Error) (hf : ∀ (a : α), f a ≤ δ) : avgOver (uniformDistribution α) f ≤ δ

A uniform average is bounded by any pointwise upper bound.

theorem MIPStarRE.LDT.avgOver_uniform_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (e : α ≃ β) (f : α → Error) : avgOver (uniformDistribution α) f = avgOver (uniformDistribution β) fun (b : β) => f (e.symm b)

Reindexing a uniform average along an equivalence preserves its value.

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_equiv {α : Type u_1} {β : Type u_2} [Fintype β] [DecidableEq β] [Nonempty β] (s : Finset α) (e : β ≃ ↥s) (f : α → Error) : avgOver (Distribution.uniformOnFinset s) f = avgOver (uniformDistribution β) fun (b : β) => f ↑(e b)

A uniform average over a finite support may be reindexed by any finite type equivalent to that support subtype.

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_filter_eq_subtype {α : Type u_1} [Fintype α] [DecidableEq α] (p : α → Prop) [DecidablePred p] [Nonempty { a : α // p a }] (f : α → Error) : avgOver (Distribution.uniformOnFinset (Finset.filter p Finset.univ)) f = avgOver (uniformDistribution { a : α // p a }) fun (a : { a : α // p a }) => f ↑a

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

theorem MIPStarRE.LDT.avgOver_uniformOnFinset_filter_equiv {α : Type u_1} {β : Type u_2} [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype β] [DecidableEq β] [Nonempty β] (e : β ≃ { a : α // p a }) (f : α → Error) : avgOver (Distribution.uniformOnFinset (Finset.filter p Finset.univ)) f = avgOver (uniformDistribution β) fun (b : β) => f ↑(e b)

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

theorem MIPStarRE.LDT.avgOver_uniform_prod {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (f : α → β → Error) : (avgOver (uniformDistribution (α × β)) fun (ab : α × β) => f ab.1 ab.2) = avgOver (uniformDistribution α) fun (a : α) => avgOver (uniformDistribution β) fun (b : β) => f a b

Split a uniform average over a product into iterated uniform averages.

theorem MIPStarRE.LDT.avgOver_uniform_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (f : α → β → Error) : (avgOver (uniformDistribution α) fun (a : α) => avgOver (uniformDistribution β) (f a)) = avgOver (uniformDistribution β) fun (b : β) => avgOver (uniformDistribution α) fun (a : α) => f a b

Swap two nested uniform averages over finite nonempty types.

theorem MIPStarRE.LDT.avgOver_uniform_prod_swap {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (f : α → β → Error) : (avgOver (uniformDistribution (α × β)) fun (ab : α × β) => f ab.1 ab.2) = avgOver (uniformDistribution β) fun (b : β) => avgOver (uniformDistribution α) fun (a : α) => f a b

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

theorem MIPStarRE.LDT.avgOver_uniform_sum_eq_card_mul_prod {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (f : α → β → Error) : (avgOver (uniformDistribution α) fun (a : α) => ∑ b : β, f a b) = ↑(Fintype.card β) * avgOver (uniformDistribution (α × β)) fun (ab : α × β) => f ab.1 ab.2

Pull a finite sum through a uniform average and express it as a uniform average over the product, with the cardinality of the summed type as the normalizing factor.

theorem MIPStarRE.LDT.avgOver_uniform_equiv_prod {γ : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (e : γ ≃ α × β) (f : γ → Error) : avgOver (uniformDistribution γ) f = avgOver (uniformDistribution α) fun (a : α) => avgOver (uniformDistribution β) fun (b : β) => f (e.symm (a, b))

Transport a uniform average through an equivalence whose target is a product, then split the product average into iterated uniform averages.

theorem MIPStarRE.LDT.avgOver_uniform_equiv_prod_swap {γ : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (e : γ ≃ α × β) (f : γ → Error) : avgOver (uniformDistribution γ) f = avgOver (uniformDistribution β) fun (b : β) => avgOver (uniformDistribution α) fun (a : α) => f (e.symm (a, b))

Transport a uniform average through an equivalence whose target is a product, then split the product average with the second coordinate averaged first.

theorem MIPStarRE.LDT.avgOver_uniform_equiv_fst {γ : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Fintype α] [DecidableEq α] [Nonempty α] [Finite β] [Nonempty β] (e : γ ≃ α × β) (f : α → Error) : (avgOver (uniformDistribution γ) fun (x : γ) => f (e x).1) = avgOver (uniformDistribution α) f

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

theorem MIPStarRE.LDT.avgOver_uniform_equiv_snd {γ : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype γ] [DecidableEq γ] [Nonempty γ] [Finite α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (e : γ ≃ α × β) (f : β → Error) : (avgOver (uniformDistribution γ) fun (x : γ) => f (e x).2) = avgOver (uniformDistribution β) f

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

theorem MIPStarRE.LDT.avgOver_uniform_fst {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (f : α → Error) : (avgOver (uniformDistribution (α × β)) fun (ab : α × β) => f ab.1) = avgOver (uniformDistribution α) f

Averaging a function depending only on the first coordinate marginalizes a uniform product.

theorem MIPStarRE.LDT.avgOver_uniform_snd {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] (f : β → Error) : (avgOver (uniformDistribution (α × β)) fun (ab : α × β) => f ab.2) = avgOver (uniformDistribution β) f

Averaging a function depending only on the second coordinate marginalizes a uniform product.