Section 8 global variance: uniform averaging

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/GlobalVariance/Theorems/Averaging.lean in the port of planning/c6b-plan.md (milestone M6, section "Port conventions"): the squared norm of a uniform operator average is at most the average of the squared norms (ev_uniformAverage_sq_le_avg), and its consequences for one-outcome averaged families (qSDD_unit_family_of_average_le_avg, sddRel_unit_family_of_pointwise).

Each statement uses a single state and joint operators, so it takes a vector state V : VecState K (a symmetric model is accepted through its coercion) as its explicit first argument, in the GlobalVariance namespace, as M1's and M3's helpers do. ev ψ is V.ev, qSDD ψ is V.qSDD, SDDRel ψ is V.SDDRel, ᴴ is star.

The vendored proof of ev_uniformAverage_sq_le_avg expands the square into a double sum and bounds each cross term by Cauchy–Schwarz; here it is the Jensen inequality of the vector state, VecState.ev_sum_conjTranspose_mul_sum_le, applied to the family a ↦ |α|⁻¹ • D a. Two private theorems unfold the uniform operator and scalar averages to these sums.

Not ported

• avgOver_polynomialDistribution_le_of_pointwise: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/expansion.tex
• blueprint/src/chapter/ch06_variance.tex

Uniform averaging infrastructure

theorem MIPRE.LIDT.Co.GlobalVariance.ev_uniformAverage_sq_le_avg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] (V : VecState K) (D : α → K →L[ℂ] K) : V.ev (star (averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) D) * averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) D) ≤ MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution α) fun (a : α) => V.ev (star (D a) * D a)

Jensen for a uniform operator average: ev (Sᴴ S) ≤ avg_a ev (D_aᴴ D_a) for S = avg_a D_a.

theorem MIPRE.LIDT.Co.GlobalVariance.qSDD_unit_family_of_average_le_avg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] (V : VecState K) (MA MB : SubMeas Unit (K →L[ℂ] K)) (A B : α → K →L[ℂ] K) (hMA : MA.outcome () = averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) A) (hMB : MB.outcome () = averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) B) : V.qSDD MA MB ≤ MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution α) fun (a : α) => V.ev (star (A a - B a) * (A a - B a))

The squared distance of two one-outcome submeasurements whose outcomes are uniform averages is at most the average of the pointwise squared distances.

theorem MIPRE.LIDT.Co.GlobalVariance.sddRel_unit_family_of_pointwise {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {α : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (MA MB : Question → SubMeas Unit (K →L[ℂ] K)) (A B : Question → α → K →L[ℂ] K) (hMA : ∀ (q : Question), (MA q).outcome () = averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) fun (a : α) => A q a) (hMB : ∀ (q : Question), (MB q).outcome () = averageOperatorOverDistribution (MIPStarRE.LDT.uniformDistribution α) fun (a : α) => B q a) (δ : ℝ) (hpoint : ∀ (a : α), (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.ev (star (A q a - B q a) * (A q a - B q a))) ≤ δ) : V.SDDRel 𝒟 MA MB δ

Lift pointwise operator deviation bounds to an SDDRel bound for unit-valued averaged families.