Uniform averaging infrastructure #
theorem
MIPStarRE.LDT.GlobalVariance.sddRel_unit_family_of_pointwise
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{Question : Type u_2}
{α : Type u_3}
[Fintype α]
[DecidableEq α]
[Nonempty α]
(ψ : QuantumState ι)
(𝒟 : Distribution Question)
(MA MB : Question → SubMeas Unit ι)
(A B : Question → α → Quantum.Op ι)
(hMA :
∀ (q : Question), (MA q).outcome () = averageOperatorOverDistribution (uniformDistribution α) fun (a : α) => A q a)
(hMB :
∀ (q : Question), (MB q).outcome () = averageOperatorOverDistribution (uniformDistribution α) fun (a : α) => B q a)
(δ : Error)
(hpoint :
∀ (a : α), (avgOver 𝒟 fun (q : Question) => ev ψ (Matrix.conjTranspose (A q a - B q a) * (A q a - B q a))) ≤ δ)
:
SDDRel ψ 𝒟 MA MB δ
Lift pointwise operator deviation bounds to an SDDRel bound for
unit-valued averaged families.
Averaging and local-to-global helpers #
theorem
MIPStarRE.LDT.GlobalVariance.avgOver_polynomialDistribution_le_of_pointwise
(params : Parameters)
[FieldModel params.q]
(f : Polynomial params → Error)
(δ : Error)
(hpoint : ∀ (g : Polynomial params), f g ≤ δ)
:
Average a pointwise polynomial bound over the uniform polynomial distribution.