Section 12 β Sandwich constructions: pasted families #
Pasted interpolation families, recurrence weights, and final operator families: the counterpart
of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/Sandwich/PastedFamilies.lean in the port of
planning/c6b-plan.md (milestone M11, section "Port conventions").
The slice family is an IdxPolyFamily params π and a strategy a SymStrat params.next π K, so
the pasted, sandwiched, vertical-line and Bernoulli-tail families are local families in π
(the vendored Op ΞΉ). Definitions that read no state and no slice family
(hRestrictionToVerticalLine, pastedMeasurementTotal) are generic over an ordered β-ring,
and the Bernoulli-tail submeasurement over any C*-algebra with its order, as the positivity
lemmas of Co/Pasting/Sandwich/GHatSandwich.lean are, so that it serves π and K βL[β] K
alike. The one placed family, fromHToGTailStageFamily, takes the symmetric model
S : SymModel π K as its first explicit argument, in place of the vendored named carriers
(ΞΉβ := ΞΉ), (ΞΉβ := ΞΉ), and its operator S.L (β¦) * S.R (β¦) is the vendored
leftTensor (β¦) * rightTensor (β¦).
Not ported #
pastedFallbackOutcome: classical, imported.verticalLine_pointAt_appendPoint: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/ld-pasting.tex
Source-style recurrence weight S_{Οtail} from lem:from-H-to-G.
The parameter prefixLen is the number of type bits already converted into the
Bernoulli polynomial. This is exactly truncatedTypeSums specialized to the
averaged complete operator G = E_x β_g G^x_g.
Equations
- MIPRE.LIDT.Co.Pasting.fromHToGRecurrenceWeight params family prefixLen Οtail = MIPRE.LIDT.Co.Pasting.truncatedTypeSums family.averagedSubMeas.total params.d prefixLen Οtail
Instances For
The interpolated operator H^{x_1,\dots,x_k}_h restricted to tuples that are
globally consistent with a single polynomial.
The paper's definition (references/ldt-paper/ld-pasting.tex lines 474β495) sums
only tuples (g_1,β¦,g_k) in Global_Ο(x) β those consistent with a single
polynomial h β and then interpolates. The |Ο| β₯ d+1 eligibility filter is
applied by interpolationEligibleSandwichFamily; this definition additionally
restricts to globally consistent tuples via IsGloballyConsistent.
Consequently, pastedInterpolationFamily is supported only on tuples satisfying
both restrictions, and any fallback or default value in
interpolateCompletedSlices is irrelevant off that restricted support.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The averaged sandwiched family restricted to outcome tuples of type Ο
with |Ο| β₯ d+1, as in lem:over-all-outcomes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The specific pasted submeasurement constructed from the sandwich/interpolation scheme.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The specific pasted measurement obtained by completing the constructed pasted submeasurement.
The paper adds all missing mass I - H_total to a single distinguished polynomial
outcome hβ (the fallback interpolant). So the outcome operator for hβ becomes
H_{hβ} + (I - H_total) while all other outcomes keep their original operators, and
the total is genuinely the identity I.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Degree-zero candidate pasted submeasurement obtained by averaging the slice family and viewing each slice polynomial as a polynomial in one more variable.
Paper origin: references/ldt-paper/ld-pasting.tex:12-55. This is a
Lean-only construction for the d = 0 branch of thm:ld-pasting, where the
ordinary interpolation construction is not available because d + 1 = 1
collapses the distinct-height argument. It introduces no additional
hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluating the averaged appended-slice submeasurement at a next-level point is the same as evaluating the averaged slice family at the truncated point.
This is the first formal step in the degree-zero branch of thm:ld-pasting;
the later consistency rectangle compares this averaged slice construction with
the point measurement.
Placeholder family for the vertical axis-parallel line measurement B^u_f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pull back the vertical-line answer family along truncatePoint, then read
its line polynomial at the lifted point's final coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In degree zero, the lifted vertical-line answer family is independent of the height coordinate once the old point coordinates are fixed.
Lean-only helper for the degree-zero branch of thm:ld-pasting; it formalizes
the fact that a vertical line answer of degree zero is constant in the line
parameter. The source context is references/ldt-paper/ld-pasting.tex:12-55.
Explicit value extracted from the i-th genuine slice outcome at the test point.
The paper's one-point sandwich comparison only sums over tuples with
g_i β β₯; the none mass is therefore removed before postprocessing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Explicit value extracted from the vertical line measurement B^u at the slice height x_i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restrict a global polynomial-valued submeasurement to the vertical line through u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Collapse a submeasurement to its Unit-valued total operator.
Equations
- MIPRE.LIDT.Co.Pasting.pastedMeasurementTotal H = MIPRE.LIDT.Co.constSubMeasFamily (MIPRE.LIDT.Co.postprocess H fun (x : Ξ±) => ())
Instances For
The expansion over all outcome types Ο, written as the
total mass of the averaged sandwich family restricted to |Ο| β₯ d+1.
Equations
- MIPRE.LIDT.Co.Pasting.allOutcomesExpansionFamily params _strategy family k = MIPRE.LIDT.Co.Pasting.pastedMeasurementTotal (MIPRE.LIDT.Co.Pasting.averagedEligibleSandwichSubMeas params family k)
Instances For
The one-outcome submeasurement whose unique effect is the Bernoulli-tail
operator of X.
Equations
- MIPRE.LIDT.Co.Pasting.bernoulliTailSubMeas k degree X hXpsd hXleOne = MIPRE.LIDT.Co.SubMeas.singleOutcome (MIPRE.LIDT.Co.Pasting.bernoulliTailOperator k degree X) β― β―
Instances For
The unique outcome of the Bernoulli-tail submeasurement is the Bernoulli-tail operator.
The total of the Bernoulli-tail submeasurement is the Bernoulli-tail operator.
The Bernoulli-tail polynomial in the averaged complete operator G = E_x \sum_g G^x_g.
Equations
- MIPRE.LIDT.Co.Pasting.bernoulliTailFromFamily params family k = MIPRE.LIDT.Co.constSubMeasFamily (MIPRE.LIDT.Co.Pasting.bernoulliTailSubMeas k params.d family.averagedSubMeas.total β― β―)
Instances For
Average the sandwiched completed-slice family over tuples whose completed/
incomplete pattern is exactly Οtail.
This is the paper's operator
$$ \mathbb E_{x_{\ge \ell}} \sum_{g_{\ge \ell} \in \mathsf{Outcomes}_{\tau_{\ge \ell}}} \widehat H^{x_{\ge \ell}}_{g_{\ge \ell}}, $$
written in the existing SubMeas Unit API so that its total operator is the
relevant suffix-stage operator. Unlike the old fromHToG recurrence families,
this keeps the \widehat H^{x_{\ge \ell}}_{g_{\ge \ell}} suffix visible instead
of collapsing immediately to the full k-step total mass.
When this is used in fromHToG, the suffix length is tailLen = k - β, and
the expectation is the paper's independent uniform average over the remaining
slice points x_{β₯β}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stage-β suffix family from the proof of lem:from-H-to-G, for a fixed
remaining tail type Ο_{β₯β}.
This is the operator-valued quantity displayed termwise in
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 where this family is used, the remaining tail length is
tailLen = k - prefixLen, so Lean stage prefixLen corresponds to the paper's
stage prefixLen + 1.
Concretely, this records
$$ \mathbb E_{x_{\ge \ell}} \sum_{g_{\ge \ell} \in \mathsf{Outcomes}_{\tau_{\ge \ell}}} \widehat H^{x_{\ge \ell}}_{g_{\ge \ell}} \otimes S_{\tau_{\ge \ell}}, $$
the tensor product being S.L (β¦) * S.R (β¦) in the symmetric model S.
Equations
- One or more equations did not get rendered due to their size.