Line interpolation: averaging and tensor helpers

Tensor/average helper lemmas and total-variation comparison used across the line interpolation error bounding chain.

References

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

theorem MIPStarRE.LDT.Pasting.avgOver_distinct_bounded_le_avgOver_uniform_add_tv (params : Parameters) [FieldModel params.q] (k : ℕ) (hk : k ≤ params.q) (F : PointTuple params k → Error) (hF_nonneg : ∀ (xs : PointTuple params k), 0 ≤ F xs) (hF_le_one : ∀ (xs : PointTuple params k), F xs ≤ 1) : avgOver (distinctTupleDistribution params k) F ≤ avgOver (uniformDistribution (PointTuple params k)) F + totalVariationDistance (uniformDistribution (PointTuple params k)) (distinctTupleDistribution params k)

theorem MIPStarRE.LDT.Pasting.avgOver_distinct_bounded_le_avgOver_uniform_add_tv_of_any_k (params : Parameters) [FieldModel params.q] (k : ℕ) (F : PointTuple params k → Error) (hF_nonneg : ∀ (xs : PointTuple params k), 0 ≤ F xs) (hF_le_one : ∀ (xs : PointTuple params k), F xs ≤ 1) : avgOver (distinctTupleDistribution params k) F ≤ avgOver (uniformDistribution (PointTuple params k)) F + totalVariationDistance (uniformDistribution (PointTuple params k)) (distinctTupleDistribution params k)

theorem MIPStarRE.LDT.Pasting.max_zero_add_le (a t : Error) (ha : 0 ≤ a) : max 0 (a + t) ≤ a + max 0 t

theorem MIPStarRE.LDT.Pasting.max_zero_mul_add_le (w a t : Error) (hw : 0 ≤ w) : max 0 (w * a + t) ≤ w * max 0 a + max 0 t

theorem MIPStarRE.LDT.Pasting.max_zero_avgOver_le_avgOver_max_zero {α : Type u_2} (𝒟 : Distribution α) (f : α → Error) : max 0 (avgOver 𝒟 f) ≤ avgOver 𝒟 fun (a : α) => max 0 (f a)

theorem MIPStarRE.LDT.Pasting.qBipartiteMatchMass_averageIdxSubMeas_left {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (B : SubMeas Outcome ι) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : qBipartiteMatchMass ψ (averageIdxSubMeas 𝒟 A h𝒟) B = avgOver 𝒟 fun (q : Question) => qBipartiteMatchMass ψ (A q) B

theorem MIPStarRE.LDT.Pasting.ev_opTensor_total_averageIdxSubMeas_left {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (B : SubMeas Outcome ι) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : ev ψ (opTensor (averageIdxSubMeas 𝒟 A h𝒟).total B.total) = avgOver 𝒟 fun (q : Question) => ev ψ (opTensor (A q).total B.total)

theorem MIPStarRE.LDT.Pasting.qBipartiteConsDefect_averageIdxSubMeas_left_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (B : SubMeas Outcome ι) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : qBipartiteConsDefect ψ (averageIdxSubMeas 𝒟 A h𝒟) B ≤ avgOver 𝒟 fun (q : Question) => qBipartiteConsDefect ψ (A q) B