Section 12 — Statements

The Section 12 pasting conclusions as reusable proposition-valued structures: the statement structures for the switcheroo, completed-family, half-sandwich, recurrence, Chernoff, and final pasting steps, and the scalar masses they compare. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Statements.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

A strategy is a SymStrat params.next 𝔓 K and a slice family an IdxPolyFamily params 𝔓, with local operators in 𝔓 (the vendored Op ι). The vendored second bipartite state ψbi : QuantumState (ι × ι) (passed as strategy.state by every vendored caller) both places the families and evaluates them here, so it is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; the placed families of Co/Pasting/Defs/Families.lean, Co/Pasting/Sandwich/Switcheroo.lean and Co/Pasting/Sandwich/GHatSandwich.lean take it as their first explicit argument. The one-space state of ChernoffBernoulliMatrixStatement, which evaluates an operator X on its own space, is a vector state V : VecState K with X : K →L[ℂ] K. Errors are in ℝ (the vendored Error).

The displayed error terms are classical (they mention no state, operator or measurement), so they are not ported: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT.Pasting (…) list.

Not ported

• ldPastingCompletenessLowerBound: classical, imported.
• commutativitySwitcherooError: classical, imported.
• commutingWithGCompleteError: classical, imported.
• commutingWithGIncompleteError: classical, imported.
• pairwiseCompletePartCommutationError: classical, imported.
• gHatSelfConsistencyError: classical, imported.
• gHatCommutationError: classical, imported.
• commuteGHalfSandwichError: classical, imported.
• ldSandwichLineOnePointError: classical, imported.
• hBConsistencyError: classical, imported.
• overAllOutcomesError: classical, imported.
• fromHToGError: classical, imported.
• fromHToGRecurrenceError: classical, imported.
• fromHToGPaperTotalError: classical, imported.

References

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

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

structure MIPRE.LIDT.Co.Pasting.LdPastingConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (H : Measurement (MIPStarRE.LDT.Polynomial params.next) 𝔓) (eps delta gamma kappa zeta : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:12-50 (\label{thm:ld-pasting}), conclusion in \label{item:ld-pasting-N-consistency} (lines 45-49).

Analytic conclusion for thm:ld-pasting once a witness H has been fixed.

The theorem ldPastingNontrivial separately records that the chosen witness is the canonical construction constructedPastedMeasurement params family k, so this structure stores only the quantitative conclusion from the paper.

• pointConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H.toSubMeas) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionError params k eps delta gamma kappa zeta)

  The pasted measurement is point-consistent with the strategy.

structure MIPRE.LIDT.Co.Pasting.LdPastingSubMeasConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (H : SubMeas (MIPStarRE.LDT.Polynomial params.next) 𝔓) (eps delta gamma kappa zeta : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:118-131 (\label{lem:ld-pasting-sub-measurement}).

Analytic conclusion for lem:ld-pasting-sub-measurement once a witness H has been fixed.

The theorem ldPastingSubMeas separately records that the chosen witness is the canonical construction constructedPastedSubMeas params family k, so this structure stores only the quantitative properties proved about that witness.

• pointConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params.next H) (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta)

  The pasted submeasurement is point-consistent with the strategy.

• completeness : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H) (MIPStarRE.LDT.Pasting.ldPastingCompletenessLowerBound params kappa (MIPStarRE.LDT.MainInductionStep.ldPastingInInductionNu params k eps delta gamma zeta) k)

  The pasted submeasurement is almost complete.

structure MIPRE.LIDT.Co.Pasting.GCompleteSelfConsistencyStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:514-536 (\label{lem:g-complete-self-consistency}); the \widehat G rewrite at eq:gselfconall (references/ldt-paper/ld-pasting.tex:821) is the family of self-consistency bounds compared against here.

Lean statement for lem:g-complete-self-consistency. S is the vendored bipartite state ψbi (passed as strategy.state by callers).

• completePartSelfConsistency : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (IdxSubMeas.liftLeft S family.meas.toIdxSubMeas) (IdxSubMeas.liftRight S family.meas.toIdxSubMeas) zeta

  Stores self-consistency of the full slice family family.meas because the cor:G-hat-facts decomposition expands \widehat G self-consistency into the original slice-family term plus the incomplete part, not the postprocessed complete-part family.

structure MIPRE.LIDT.Co.Pasting.GBotSelfConsistencyStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (zeta : ℝ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:537-558 (\label{cor:g-bot-self-consistency}); incomplete-part complement of \label{lem:g-complete-self-consistency} and the eq:gselfconall self-consistency family at line 821.

Lean statement for cor:g-bot-self-consistency.

• incompletePartSelfConsistency : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (incompletePartLeftFamily S params family) (incompletePartRightFamily S params family) zeta

  The incomplete parts G^x_⊥ are self-consistent.

structure MIPRE.LIDT.Co.Pasting.CommutativitySwitcherooStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (M : IdxProjSubMeas (MIPStarRE.LDT.Fq params) Outcome 𝔓) (zeta omega chi : ℝ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:560-720 (\label{lem:commutativity-switcheroo}).

Lean statement for lem:commutativity-switcheroo.

• aggregateCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (switcherooAggregateLeft S params family M) (switcherooAggregateRight S params family M) (MIPStarRE.LDT.Pasting.commutativitySwitcherooError zeta omega chi)

  The aggregate G^x M^y and M^y G^x families are close.

structure MIPRE.LIDT.Co.Pasting.CommutingWithGCompleteStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:721-774 (\label{cor:commuting-with-G-complete}).

Lean statement for cor:commuting-with-G-complete.

• pairwiseCompletePartCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => OpFamily.leftPlacedOpFamily S (CommutativityPoints.orderedProductOpFamily (family.meas q.1).toSubMeas (family.meas q.2).toSubMeas)) (fun (q : MIPStarRE.LDT.Pasting.SlicePairQuestion params) => OpFamily.leftPlacedOpFamily S (CommutativityPoints.reversedProductOpFamily (family.meas q.1).toSubMeas (family.meas q.2).toSubMeas)) (MIPStarRE.LDT.Pasting.pairwiseCompletePartCommutationError params gamma zeta)

  The slice measurements G^x, G^y approximately commute.

• pointWithCompletePartCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (completePartPointProductLeft S params family) (completePartPointProductRight S params family) (MIPStarRE.LDT.Pasting.commutingWithGCompleteError params gamma zeta)

  The slice outcomes G^x_g approximately commute with the complete parts G^y.

• completePartCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (completePartTotalProductLeft S params family) (completePartTotalProductRight S params family) (MIPStarRE.LDT.Pasting.commutingWithGCompleteError params gamma zeta)

  The complete parts G^x, G^y approximately commute.

structure MIPRE.LIDT.Co.Pasting.CommutingWithGIncompleteStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:775-816 (\label{cor:commuting-with-G-incomplete}).

Lean statement for cor:commuting-with-G-incomplete.

• pointWithIncompletePartCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (incompletePartPointProductLeft S params family) (incompletePartPointProductRight S params family) (MIPStarRE.LDT.Pasting.commutingWithGIncompleteError params gamma zeta)

  The slice outcomes G^x_g approximately commute with the incomplete parts G^y_⊥.

• incompletePartCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (incompletePartTotalProductLeft S params family) (incompletePartTotalProductRight S params family) (MIPStarRE.LDT.Pasting.commutingWithGIncompleteError params gamma zeta)

  The incomplete parts G^x_⊥, G^y_⊥ approximately commute.

structure MIPRE.LIDT.Co.Pasting.GHatFactsStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:817-862 (\label{cor:G-hat-facts}); the displayed \widehat G self-consistency and commutation lines eq:gselfconall and eq:gcomall are at lines 821 and 823.

Lean statement for cor:G-hat-facts.

• completedSelfConsistency : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (gHatSelfConsistencyLeftFamily S params family) (gHatSelfConsistencyRightFamily S params family) (MIPStarRE.LDT.Pasting.gHatSelfConsistencyError zeta)

  The completed slice measurements \widehat G^x are self-consistent.

• completedCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SlicePairQuestion params)) (gHatPairProductLeft S params family) (gHatPairProductRight S params family) (MIPStarRE.LDT.Pasting.gHatCommutationError params gamma zeta)

  The completed slice measurements \widehat G^x, \widehat G^y approximately commute.

structure MIPRE.LIDT.Co.Pasting.CommuteGHalfSandwichStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:872-917 (\label{lem:commute-g-half-sandwich}).

Lean statement for lem:commute-g-half-sandwich.

• repeatedCommutation : S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params k)) (gHatHalfSandwichLeft S params family k) (gHatHalfSandwichRight S params family k) (MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta k)

  The half-sandwich product and its cyclic rotation are close.

structure MIPRE.LIDT.Co.Pasting.LdSandwichLineOnePointStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (k i : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:918-1040 (\label{lem:ld-sandwich-line-one-point}).

Lean statement for lem:ld-sandwich-line-one-point.

• linePointComparison : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointLeftFamily params strategy family k i) (ldSandwichLineOnePointRightFamily params strategy family k i) (MIPStarRE.LDT.Pasting.ldSandwichLineOnePointError params eps delta gamma zeta k)

  The i-th sandwiched slice value agrees with the vertical line measurement.

structure MIPRE.LIDT.Co.Pasting.HBConsistencyStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1041-1140 (\label{lem:h-b-consistency}).

Lean statement for lem:h-b-consistency.

• lineConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.VerticalLineQuestion params)) (hRestrictionToVerticalLine params (constructedPastedSubMeas params family k)) (verticalLineMeasurementFamily params strategy) (MIPStarRE.LDT.Pasting.hBConsistencyError params eps delta gamma zeta k)

  The pasted submeasurement restricted to vertical lines agrees with the line measurement.

noncomputable def MIPRE.LIDT.Co.Pasting.overAllOutcomesPastedMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (k : ℕ) : ℝ

Scalar expectation of the pasted submeasurement mass appearing on the left-hand side of lem:over-all-outcomes.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.overAllOutcomesExpansionMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (k : ℕ) : ℝ

Scalar expectation of the all-outcomes expansion on the right-hand side of lem:over-all-outcomes.

Equations

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

structure MIPRE.LIDT.Co.Pasting.OverAllOutcomesStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (eps delta gamma zeta : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1141-1294 (\label{lem:over-all-outcomes}).

Lean statement for lem:over-all-outcomes.

The paper's displayed statement is a scalar approximation of expectation values, not a stronger ≈_δ relation between already-collapsed Unit-indexed submeasurements. Accordingly, this structure stores only the absolute-value bound between the pasted mass and the all-outcomes expansion mass.

• totalOutcomeExpansion : |overAllOutcomesPastedMass params strategy family k - overAllOutcomesExpansionMass params strategy family k| ≤ MIPStarRE.LDT.Pasting.overAllOutcomesError params eps delta gamma zeta k

  The pasted mass is close to the all-outcomes expansion mass.

noncomputable def MIPRE.LIDT.Co.Pasting.fromHToGTailStageMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (prefixLen : ℕ) {tailLen : ℕ} (τtail : MIPStarRE.LDT.Pasting.GHatType tailLen) : ℝ

Scalar expectation of one per-tail contribution in lem:from-H-to-G.

This is the single-τ_{≥ℓ} term appearing inside the aggregate stage mass from references/ldt-paper/ld-pasting.tex, equation eq:i-think-this-is-what-i'm-supposed-to-prove-2 (lines 1386–1391). The parameter prefixLen is the Lean 0-based stage index. In the ambient k-step recurrence, the remaining tail length is tailLen = k - prefixLen.

Equations

• MIPRE.LIDT.Co.Pasting.fromHToGTailStageMass params S family prefixLen τtail = S.ev (MIPRE.LIDT.Co.Pasting.fromHToGTailStageFamily S params family prefixLen τtail ()).total

noncomputable def MIPRE.LIDT.Co.Pasting.fromHToGStageMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (k ℓ : ℕ) : ℝ

Scalar expectation of the full Lean stage-ℓ quantity from lem:from-H-to-G.

This is the aggregate quantity displayed in references/ldt-paper/ld-pasting.tex, equation eq:i-think-this-is-what-i'm-supposed-to-prove-2 (lines 1386–1391). Lean uses 0-based indexing: stage ℓ here corresponds to the paper's stage ℓ + 1, so the remaining tail has length k - ℓ. Accordingly, this sums over all remaining tail types τ_{≥ℓ} ∈ {0,1}^{k-ℓ}, while the next Lean stage ℓ + 1 sums over the shorter tails τ_{>ℓ}.

Equations

• MIPRE.LIDT.Co.Pasting.fromHToGStageMass params S family k ℓ = ∑ τtail : MIPStarRE.LDT.Pasting.GHatType (k - ℓ), MIPRE.LIDT.Co.Pasting.fromHToGTailStageMass params S family ℓ τtail

noncomputable def MIPRE.LIDT.Co.Pasting.fromHToGAllOutcomesMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (k : ℕ) : ℝ

Scalar expectation of the left-hand side of lem:from-H-to-G, i.e. the uniform average of the eligible pasted-sandwich total mass.

Equations

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

noncomputable def MIPRE.LIDT.Co.Pasting.fromHToGBernoulliTailMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (k : ℕ) : ℝ

Scalar expectation of the Bernoulli-tail polynomial F(G) on the bipartite state from lem:from-H-to-G.

Equations

• MIPRE.LIDT.Co.Pasting.fromHToGBernoulliTailMass params S family k = S.subMeasMass (MIPRE.LIDT.Co.IdxSubMeas.liftRight S (MIPRE.LIDT.Co.Pasting.bernoulliTailFromFamily params family k) ())

structure MIPRE.LIDT.Co.Pasting.FromHToGStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (S : SymModel 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1295-1670 (\label{lem:from-H-to-G}).

Lean statement for lem:from-H-to-G.

The paper's displayed statement is a scalar approximation of expectation values, not a new ≈_δ relation between submeasurements. Accordingly, this statement stores only the final all-outcomes vs. Bernoulli-tail comparison; the adjacent-stage estimates are recorded by the internal construction lemmas.

• bernoulliPolynomialRewrite : |fromHToGAllOutcomesMass params strategy S family k - fromHToGBernoulliTailMass params S family k| ≤ MIPStarRE.LDT.Pasting.fromHToGError params gamma zeta k

  The all-outcomes mass is close to the Bernoulli-tail mass.

structure MIPRE.LIDT.Co.Pasting.ChernoffBernoulliMatrixStatement {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (theta : ℝ) (k degree : ℕ) (X : K →L[ℂ] K) (kappa : ℝ) (hXpsd : 0 ≤ X) (hXleOne : X ≤ 1) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1671-1798 (\label{lem:chernoff-bernoulli-matrix}); the operator-Chernoff inequality is proved by applying continuous functional calculus to the scalar tail polynomial and the scalar Chernoff bound eq:by-chernoff at line 1739.

Lean statement for lem:chernoff-bernoulli-matrix. The vendored one-space state ψ : QuantumState ι and operator X : Op ι are a vector state V : VecState K and an operator X : K →L[ℂ] K.

• matrixTailBound : V.CompletenessAtLeast (bernoulliTailSubMeas k degree X hXpsd hXleOne) (1 - kappa / (1 - theta) - Real.exp (-(theta ^ 2 * ↑k) / 2))

  The Bernoulli-tail submeasurement of X is almost complete.

structure MIPRE.LIDT.Co.Pasting.LdPastingNCompletenessStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (kappa nu : ℝ) (k : ℕ) : Prop

Paper origin: references/ldt-paper/ld-pasting.tex:1799-1849 (\label{cor:ld-pasting-N-completeness}).

Lean statement for cor:ld-pasting-N-completeness.

• completenessBound : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state (constructedPastedSubMeas params family k)) (MIPStarRE.LDT.Pasting.ldPastingCompletenessLowerBound params kappa nu k)

  The constructed pasted submeasurement is almost complete.