Documentation

MIPRE.Background.LIDT.Co.Pasting.ComparisonLemmas.LdSandwichLineOnePoint.PrefixMoved

Section 12 pasting: line one-point transport — prefix moved lemmas #

The prefix lemmas of the line one-point transport: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LdSandwichLineOnePoint/PrefixMoved.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The slice family is an IdxPolyFamily params 𝔓, so the prefix families and the half-products are local, in 𝔓, and the vendored conjugate transpose ᴴ is star. The endpoint consistency of the rotated prefix family is a ConsRel on strategy.state, and the raw commutation of the prefix an SDDOpRel on a symmetric model S; no swap or normalization hypothesis appears, the vendored statements having none. The half-product identities (the last factor split off, the last slice summed out, the reversed product as the adjoint) hold in 𝔓 from the projectivity of the completed slices alone.

Not ported #

Nothing: every vendored declaration has a counterpart of the same name.

References #

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

source
noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixOriginalFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) :
IdxSubMeas (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (Option (MIPStarRE.LDT.Fq params)) 𝔓

The original one-point left family restricted to the prefix through coordinate i.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixMovedFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) {k i : ℕ} (hi : i < k) :
    IdxSubMeas (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) (Option (MIPStarRE.LDT.Fq params)) 𝔓

    The prefix family after rotating the selected coordinate to the front.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixMoved_eq_endpoint {𝔓 : 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 i : ℕ} (hi : i < k) :
      ldSandwichLineOnePointPrefixMovedFamily params family hi = fun (q : MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k) => postprocess (evaluateAt params q.1 (family.meas (q.2 ⟨i, hi⟩)).toSubMeas) some

      Rotating the selected coordinate to the front reduces the prefix family to ldGbcon.

      This is the prefix-completeness collapse and endpoint identification used after references/ldt-paper/ld-pasting.tex:1011--1024: once the selected coordinate is first, summing the remaining prefix sandwich leaves the one-point endpoint measurement.

      source
      theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointLeftFamily_self_eq_prefixOriginal {𝔓 : 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 𝔓) (i : ℕ) :
      ldSandwichLineOnePointLeftFamily params strategy family (i + 1) i = ldSandwichLineOnePointPrefixOriginalFamily params family ⋯

      The global one-point left family at its last prefix index is the prefix family.

      source
      theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixMoved_consRel_endpoint_of_axis_self {𝔓 : 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) (eps delta zeta : ℝ) (haxis : strategy.axisParallelFailureProbability ≤ eps) (hself : strategy.selfConsistencyFailureProbability ≤ delta) (family : IdxPolyFamily params 𝔓) (hcons : family.ConsistentWithPoints strategy zeta) {k i : ℕ} (hi : i < k) :
      strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SandwichedLineQuestion params k)) (ldSandwichLineOnePointPrefixMovedFamily params family hi) (ldSandwichLineOnePointRightFamily params strategy family k i) (zeta + √(8 * ↑params.m * eps + 4 * delta))

      Endpoint consistency for the rotated prefix family.

      source
      theorem MIPRE.LIDT.Co.Pasting.ldSandwichLineOnePointPrefixMoved_rawCommutation {𝔓 : 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 : ℝ) (hcomm : ∀ (j : ℕ), 2 ≤ j → CommuteGHalfSandwichStatement params S family gamma zeta j) {i : ℕ} (hi0 : i ≠ 0) :
      S.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.PointTuple params (i + 1))) (gHatHalfSandwichLeft S params family (i + 1)) (gHatHalfSandwichRight S params family (i + 1)) (MIPStarRE.LDT.Pasting.commuteGHalfSandwichError params gamma zeta (i + 1))

      Raw commutation for the nonempty prefix before adding the remaining question tail.

      source
      theorem MIPRE.LIDT.Co.Pasting.gHatHalfProduct_prefix_mul_last {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (i : ℕ) (xs : MIPStarRE.LDT.PointTuple params (i + 2)) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 2)) :
      gHatHalfProductOutcomeOperator params family (i + 2) xs gs = (gHatHalfProductOutcomeOperator params family (i + 1) (fun (j : Fin (i + 1)) => xs ⟨↑j, ⋯⟩) fun (j : Fin (i + 1)) => gs ⟨↑j, ⋯⟩) * (gHatIdxMeas params family (xs ⟨i + 1, ⋯⟩)).outcome (gs ⟨i + 1, ⋯⟩)

      Expand a half-product into the prefix product times the last slice operator.

      source
      theorem MIPRE.LIDT.Co.Pasting.gHatHalfProductOutcomeOperator_prefix_last {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (n : ℕ) (xs : MIPStarRE.LDT.PointTuple params (n + 1)) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (n + 1)) :
      gHatHalfProductOutcomeOperator params family (n + 1) xs gs = (gHatHalfProductOutcomeOperator params family n (fun (j : Fin n) => xs ⟨↑j, ⋯⟩) fun (j : Fin n) => gs ⟨↑j, ⋯⟩) * (gHatIdxMeas params family (xs ⟨n, ⋯⟩)).outcome (gs ⟨n, ⋯⟩)

      Split the ordered half-product into its first n coordinates and the last slice.

      source
      theorem MIPRE.LIDT.Co.Pasting.gHatSandwich_sum_last_eq_prefix {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (n : ℕ) (xs : MIPStarRE.LDT.PointTuple params (n + 1)) (gsPrefix : MIPStarRE.LDT.Pasting.GHatTupleOutcome params n) :
      (∑ g : MIPStarRE.LDT.Pasting.GHatOutcome params, have half := gHatHalfProductOutcomeOperator params family (n + 1) xs ((MIPStarRE.LDT.Pasting.gHatTupleOutcomePrefixLastEquiv params n).symm (gsPrefix, g)); half * star half) = gHatHalfProductOutcomeOperator params family n (fun (j : Fin n) => xs ⟨↑j, ⋯⟩) gsPrefix * star (gHatHalfProductOutcomeOperator params family n (fun (j : Fin n) => xs ⟨↑j, ⋯⟩) gsPrefix)

      Summing the last completed-slice sandwich coordinate deletes that coordinate.

      This formalizes the measurement-completeness step in ld-pasting.tex lines 934--941 for a single trailing coordinate.

      source
      theorem MIPRE.LIDT.Co.Pasting.gHatHalfProduct_lastReverse_eq_conjTranspose {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (i : ℕ) (xs : MIPStarRE.LDT.PointTuple params (i + 1)) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) :
      gHatHalfProductOutcomeOperator params family (i + 1) ((MIPStarRE.LDT.Pasting.pointTupleLastReverseEquiv params i) xs) ((MIPStarRE.LDT.Pasting.gHatTupleOutcomeLastReverseEquiv params i) gs) = star (gHatHalfProductOutcomeOperator params family (i + 1) xs gs)

      Reversing the prefix after moving the last coordinate to the front gives the adjoint product.

      source
      theorem MIPRE.LIDT.Co.Pasting.gHatRotatedHalfProduct_lastReverse_eq_conjTranspose_lastFront {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (i : ℕ) (xs : MIPStarRE.LDT.PointTuple params (i + 1)) (gs : MIPStarRE.LDT.Pasting.GHatTupleOutcome params (i + 1)) :
      gHatRotatedHalfProductOutcomeOperator params family (i + 1) ((MIPStarRE.LDT.Pasting.pointTupleLastReverseEquiv params i) xs) ((MIPStarRE.LDT.Pasting.gHatTupleOutcomeLastReverseEquiv params i) gs) = star (gHatHalfProductOutcomeOperator params family (i + 1) ((MIPStarRE.LDT.Pasting.pointTupleLastFrontEquiv params i) xs) ((MIPStarRE.LDT.Pasting.gHatTupleOutcomeLastFrontEquiv params i) gs))

      The rotated product on the last-reversed tuple is the adjoint of the last-front product.