Section 12 pasting: comparison common helpers

Shared postprocessing, symmetry, distribution, boundedness, and arithmetic helpers for the Section 12 comparison lemmas.

References

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

theorem MIPStarRE.LDT.Pasting.postprocess_postprocess {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] (A : SubMeas α ι) (f : α → β) (g : β → γ) : postprocess (postprocess A f) g = postprocess A (g ∘ f)

theorem MIPStarRE.LDT.Pasting.postprocess_hRestrictionToVerticalLine_eq_evaluateAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (H : SubMeas (Polynomial params.next) ι) (u : Point params.next) : (postprocess (hRestrictionToVerticalLine params H (truncatePoint params u)) fun (f : AxisLinePolynomial params.next) => f.toFun (pointHeight params u)) = evaluateAt params.next u H

theorem MIPStarRE.LDT.Pasting.consRel_uniform_fst {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} {Outcome : Type u_4} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A B : IdxSubMeas α Outcome ι) (δ : Error) : ConsRel ψ (uniformDistribution α) A B δ → ConsRel ψ (uniformDistribution (α × β)) (fun (ab : α × β) => A ab.1) (fun (ab : α × β) => B ab.1) δ

theorem MIPStarRE.LDT.Pasting.qBipartiteMatchMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A B : SubMeas Outcome ι) : 0 ≤ qBipartiteMatchMass ψ A B

theorem MIPStarRE.LDT.Pasting.qBipartiteConsDefect_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hnorm : ψ.IsNormalized) (A B : SubMeas Outcome ι) : qBipartiteConsDefect ψ A B ≤ 1

theorem MIPStarRE.LDT.Pasting.bipartiteConsError_uniform_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hnorm : ψ.IsNormalized) (A B : IdxSubMeas Question Outcome ι) : bipartiteConsError ψ (uniformDistribution Question) A B ≤ 1

theorem MIPStarRE.LDT.Pasting.qBipartiteSSCDefect_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hnorm : ψ.IsNormalized) (A : SubMeas Outcome ι) : qBipartiteSSCDefect ψ A ≤ 1

theorem MIPStarRE.LDT.Pasting.bipartiteSSCError_uniform_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {Outcome : Type u_3} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hnorm : ψ.IsNormalized) (A : IdxSubMeas Question Outcome ι) : bipartiteSSCError ψ (uniformDistribution Question) A ≤ 1

theorem MIPStarRE.LDT.Pasting.sqrt_min_le_rpow32 (x : Error) (hx : 0 ≤ x) : √(min x 1) ≤ Real.rpow x (1 / 32)

theorem MIPStarRE.LDT.Pasting.hAConsistency_sqrt_bound_of_pos (params : Parameters) (eps delta : Error) (k : ℕ) (hk_pos : 1 ≤ k) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) : √(8 * ↑params.m * min eps 1 + 4 * min delta 1) ≤ 3 * ↑k ^ 2 * ↑params.m * (Real.rpow eps (1 / 32) + Real.rpow delta (1 / 32))

theorem MIPStarRE.LDT.Pasting.hAConsistency_error_le_nu_of_pos (params : Parameters) (eps delta gamma zeta : Error) (k : ℕ) (hk_pos : 1 ≤ k) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) : hBConsistencyError params eps delta gamma zeta k + √(8 * ↑params.m * min eps 1 + 4 * min delta 1) ≤ MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta