Uniform push-forward averaging lemmas

This file contains shared averaging lemmas for uniformly sampled finite seeds that are pushed forward to a question distribution. The main use case is a random seed a : α, a pushed-forward value m a : β, and an observed coordinate g (m a) which is identified with a uniform coordinate by an equivalence.

Main declarations

• avgOver_uniform_map_eq_uniform_of_factor_equiv
• averageOperatorOverDistribution_uniform_map_eq_uniform_of_factor_equiv
• avgOver_uniform_map_eq_uniform_fst_of_factor_equiv
• avgOver_uniform_map_eq_uniform_snd_of_factor_equiv
• averageOperatorOverDistribution_uniform_map_eq_uniform_fst_of_factor_equiv
• averageOperatorOverDistribution_uniform_map_eq_uniform_snd_of_factor_equiv

References

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

Project-distribution map averages

theorem MIPStarRE.LDT.avgOver_uniform_map_eq_uniform_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Fintype γ] [DecidableEq γ] [Nonempty γ] (m : α → β) (g : β → γ) (e : α ≃ γ) (h : ∀ (a : α), g (m a) = e a) (f : γ → Error) : (avgOver ((uniformDistribution α).map m) fun (b : β) => f (g b)) = avgOver (uniformDistribution γ) f

A uniform push-forward has the uniform average induced by an equivalent observed coordinate.

The map m is the finite random seed map, g is the observed coordinate on the pushed-forward value, and e records that this observed coordinate is equivalent to a uniform sample of γ.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_map_eq_uniform_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Fintype γ] [DecidableEq γ] [Nonempty γ] (m : α → β) (g : β → γ) (e : α ≃ γ) (h : ∀ (a : α), g (m a) = e a) {ι : Type u_4} [Fintype ι] [DecidableEq ι] (A : γ → Quantum.Op ι) : (averageOperatorOverDistribution ((uniformDistribution α).map m) fun (b : β) => A (g b)) = averageOperatorOverDistribution (uniformDistribution γ) A

A uniform push-forward has the uniform operator average induced by an equivalent observed coordinate.

The map m is the finite random seed map, g is the observed coordinate on the pushed-forward value, and e records that this observed coordinate is equivalent to a uniform sample of γ.

theorem MIPStarRE.LDT.avgOver_uniform_map_eq_uniform_fst_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [Finite δ] [Nonempty δ] (m : α → β) (g : β → γ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).1) (f : γ → Error) : (avgOver ((uniformDistribution α).map m) fun (b : β) => f (g b)) = avgOver (uniformDistribution γ) f

A uniform push-forward has the first-coordinate uniform marginal when the observed coordinate factors through a product equivalence of the seed.

theorem MIPStarRE.LDT.avgOver_uniform_map_eq_uniform_snd_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Finite γ] [Nonempty γ] [Fintype δ] [DecidableEq δ] [Nonempty δ] (m : α → β) (g : β → δ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).2) (f : δ → Error) : (avgOver ((uniformDistribution α).map m) fun (b : β) => f (g b)) = avgOver (uniformDistribution δ) f

A uniform push-forward has the second-coordinate uniform marginal when the observed coordinate factors through a product equivalence of the seed.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_map_eq_uniform_fst_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Fintype γ] [DecidableEq γ] [Nonempty γ] [Finite δ] [Nonempty δ] (m : α → β) (g : β → γ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).1) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (A : γ → Quantum.Op ι) : (averageOperatorOverDistribution ((uniformDistribution α).map m) fun (b : β) => A (g b)) = averageOperatorOverDistribution (uniformDistribution γ) A

A uniform push-forward has the first-coordinate uniform operator marginal when the observed coordinate factors through a product equivalence of the seed.

theorem MIPStarRE.LDT.averageOperatorOverDistribution_uniform_map_eq_uniform_snd_of_factor_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [DecidableEq β] [Finite γ] [Nonempty γ] [Fintype δ] [DecidableEq δ] [Nonempty δ] (m : α → β) (g : β → δ) (e : α ≃ γ × δ) (h : ∀ (a : α), g (m a) = (e a).2) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (A : δ → Quantum.Op ι) : (averageOperatorOverDistribution ((uniformDistribution α).map m) fun (b : β) => A (g b)) = averageOperatorOverDistribution (uniformDistribution δ) A

A uniform push-forward has the second-coordinate uniform operator marginal when the observed coordinate factors through a product equivalence of the seed.