Line interpolation: bad-mass comparison

Main bad-mass comparison lemmas: sandwich mismatch sums, qBipartiteConsDefect equality via single-outcome measurements, hBConsistencyBadMass, line-point defect bounds, and pastedInterpolation_verticalLine_defect_le_badMass.

References

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

theorem MIPStarRE.LDT.Pasting.interpolationEligibleSandwich_mismatch_sum_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) (hxs : Function.Injective xs) (f : AxisLinePolynomial params.next) : (∑ gs : GHatTupleOutcome params k, if IsGloballyConsistent params xs gs ∧ tupleInterpolatedVerticalLine params u xs gs ≠ f then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ≤ ∑ gs : GHatTupleOutcome params k, if ∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0

theorem MIPStarRE.LDT.Pasting.interpolationEligibleSandwich_exists_mismatch_sum_le_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) (f : AxisLinePolynomial params.next) : (∑ gs : GHatTupleOutcome params k, if ∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ≤ ∑ i : Fin k, ∑ gs : GHatTupleOutcome params k, if ∃ (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0

theorem MIPStarRE.LDT.Pasting.pastedInterpolation_verticalLine_singleOutcome_postprocess {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (k : ℕ) (u : Point params) (xs : PointTuple params k) (f : AxisLinePolynomial params.next) : (postprocess (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) fun (h : AxisLinePolynomial params.next) => decide (h = f)) = postprocess (restrictSubMeas (interpolationEligibleSandwichFamily params family k xs) (IsGloballyConsistent params xs)) fun (gs : GHatTupleOutcome params k) => decide (tupleInterpolatedVerticalLine params u xs gs = f)

noncomputable def MIPStarRE.LDT.Pasting.singleOutcomeRightSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (B : SubMeas Outcome ι) (a0 : Outcome) : SubMeas Bool ι

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.qBipartiteConsDefect_eq_false_mass_of_bool_right_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (A B : SubMeas Bool ι) (hfalse : B.outcome false = 0) (htrue : B.outcome true = B.total) : qBipartiteConsDefect ψ A B = ev ψ (opTensor (A.outcome false) B.total)

If the right-hand Boolean submeasurement has only the true outcome, the consistency defect is exactly the left false mass against its total operator.

theorem MIPStarRE.LDT.Pasting.qBipartiteConsDefect_postprocess_eq_singleOutcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ι × ι)) (A B : SubMeas Outcome ι) (a0 : Outcome) : qBipartiteConsDefect ψ (postprocess A fun (a : Outcome) => decide (a = a0)) (singleOutcomeRightSubMeas B a0) = ev ψ (opTensor ((postprocess A fun (a : Outcome) => decide (a = a0)).outcome false) (B.outcome a0))

theorem MIPStarRE.LDT.Pasting.postprocess_decide_eq_true_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (A : SubMeas Outcome ι) (a0 : Outcome) : (postprocess A fun (a : Outcome) => decide (a = a0)).outcome true = A.outcome a0

theorem MIPStarRE.LDT.Pasting.postprocess_decide_false_add_true_eq_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (A : SubMeas Outcome ι) (a0 : Outcome) : (postprocess A fun (a : Outcome) => decide (a = a0)).outcome false + A.outcome a0 = A.total

theorem MIPStarRE.LDT.Pasting.qBipartiteConsDefect_eq_sum_singleOutcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] [DecidableEq Outcome] (ψ : QuantumState (ι × ι)) (A : SubMeas Outcome ι) (B : Measurement Outcome ι) : qBipartiteConsDefect ψ A B.toSubMeas = ∑ a0 : Outcome, qBipartiteConsDefect ψ (postprocess A fun (a : Outcome) => decide (a = a0)) (singleOutcomeRightSubMeas B.toSubMeas a0)

noncomputable def MIPStarRE.LDT.Pasting.hBConsistencyBadMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) : Error

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Pasting.ldSandwichLineOnePointRightMeasurement {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (i : Fin k) (q : SandwichedLineQuestion params k) : Measurement (Option (Fq params)) ι

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePointRightMeasurement_outcome_some_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (i : Fin k) (q : SandwichedLineQuestion params k) (a : Fq params) : (ldSandwichLineOnePointRightMeasurement params strategy family i q).outcome (some a) = ∑ f : AxisLinePolynomial params.next, if f.toFun (q.2 i) = a then (verticalLineMeasurementFamily params strategy q.1).outcome f else 0

theorem MIPStarRE.LDT.Pasting.grouped_coordinate_mismatch_le_left_falseOutcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) (i : Fin k) (a : Fq params) : (∑ gs : GHatTupleOutcome params k, if ∃ (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ a then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ≤ (postprocess (ldSandwichLineOnePointLeftFamily params strategy family k ↑i (u, xs)) fun (o : Option (Fq params)) => decide (o = some a)).outcome false

theorem MIPStarRE.LDT.Pasting.hBConsistencyCoordMass_le_linePointDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) (i : Fin k) : ∑ f : AxisLinePolynomial params.next, ev strategy.state (opTensor (∑ gs : GHatTupleOutcome params k, if ∃ (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i) then (interpolationEligibleSandwichFamily params family k xs).outcome gs else 0) ((verticalLineMeasurementFamily params strategy u).outcome f)) ≤ qBipartiteConsDefect strategy.state (ldSandwichLineOnePointLeftFamily params strategy family k ↑i (u, xs)) (ldSandwichLineOnePointRightFamily params strategy family k ↑i (u, xs))

theorem MIPStarRE.LDT.Pasting.hBConsistencyBadMass_le_linePointDefectSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) : hBConsistencyBadMass params strategy family u xs ≤ ∑ i : Fin k, qBipartiteConsDefect strategy.state (ldSandwichLineOnePointLeftFamily params strategy family k ↑i (u, xs)) (ldSandwichLineOnePointRightFamily params strategy family k ↑i (u, xs))

theorem MIPStarRE.LDT.Pasting.hBConsistencyBadMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) : 0 ≤ hBConsistencyBadMass params strategy family u xs

theorem MIPStarRE.LDT.Pasting.hBConsistencyBadMass_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) : hBConsistencyBadMass params strategy family u xs ≤ 1

theorem MIPStarRE.LDT.Pasting.postprocess_restrictSubMeas_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] (A : SubMeas α ι) (p : α → Prop) [DecidablePred p] (f : α → β) (b : β) : (postprocess (restrictSubMeas A p) f).outcome b = ∑ a : α, if p a ∧ f a = b then A.outcome a else 0

theorem MIPStarRE.LDT.Pasting.pastedInterpolation_verticalLine_defect_le_badMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) {k : ℕ} (u : Point params) (xs : PointTuple params k) (hxs : Function.Injective xs) : qBipartiteConsDefect strategy.state (hRestrictionToVerticalLine params (pastedInterpolationFamily params family k xs) u) (verticalLineMeasurementFamily params strategy u) ≤ hBConsistencyBadMass params strategy family u xs