Section 12 pasting: line one-point transport — endpoint equivalences

Internal helper module; part of the file-split for #1127.

References

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

noncomputable def MIPStarRE.LDT.Pasting.postprocessMeasurement {α : Type u_2} {β : Type u_3} {ι : Type u_4} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (B : Measurement α ι) (f : α → β) : Measurement β ι

Turn a postprocessed submeasurement from a measurement into a measurement.

Equations

• MIPStarRE.LDT.Pasting.postprocessMeasurement B f = { toSubMeas := MIPStarRE.LDT.postprocess B.toSubMeas f, total_eq_one := ⋯ }

noncomputable def MIPStarRE.LDT.Pasting.sandwichedLineQuestionSplitAtEquiv (params : Parameters) [FieldModel params.q] {k : ℕ} (i : Fin k) : SandwichedLineQuestion params k ≃ (Point params × Fq params) × ({ j : Fin k // j ≠ i } → Fq params)

Split a sandwiched-line question at one selected slice coordinate.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.sandwichedLineQuestionPrefixEquiv (params : Parameters) [FieldModel params.q] {k i : ℕ} (hi : i < k) : SandwichedLineQuestion params k ≃ (Point params × PointTuple params (i + 1)) × ({ j : Fin k // i < ↑j } → Fq params)

Split a sandwiched-line question into the prefix through i and the tail.

Equations

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

def MIPStarRE.LDT.Pasting.prodPrefixReassocEquiv (α : Type u_2) (β : Type u_3) (γ : Type u_4) : (α × β) × γ ≃ β × α × γ

Reassociate a nested product so the prefix coordinate becomes first.

Equations

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

noncomputable def MIPStarRE.LDT.Pasting.sandwichedLineQuestionPrefixFstEquiv (params : Parameters) [FieldModel params.q] {k i : ℕ} (hi : i < k) : SandwichedLineQuestion params k ≃ PointTuple params (i + 1) × Point params × ({ j : Fin k // i < ↑j } → Fq params)

View the prefix of a sandwiched-line question as the first product coordinate.

Equations

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

def MIPStarRE.LDT.Pasting.pointTupleLastFrontEquiv (params : Parameters) (i : ℕ) : PointTuple params (i + 1) ≃ PointTuple params (i + 1)

Rotate the last coordinate of a prefix tuple to the front.

Equations

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

def MIPStarRE.LDT.Pasting.gHatTupleOutcomeLastFrontEquiv (params : Parameters) [FieldModel params.q] (i : ℕ) : GHatTupleOutcome params (i + 1) ≃ GHatTupleOutcome params (i + 1)

Rotate the last completed-slice outcome of a prefix tuple to the front.

Equations

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

def MIPStarRE.LDT.Pasting.pointTupleLastReverseEquiv (params : Parameters) (i : ℕ) : PointTuple params (i + 1) ≃ PointTuple params (i + 1)

Move the last coordinate to the front and reverse the preceding prefix.

Equations

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

def MIPStarRE.LDT.Pasting.gHatTupleOutcomeLastReverseEquiv (params : Parameters) [FieldModel params.q] (i : ℕ) : GHatTupleOutcome params (i + 1) ≃ GHatTupleOutcome params (i + 1)

Move the last completed-slice outcome to the front and reverse the preceding prefix.

Equations

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

def MIPStarRE.LDT.Pasting.gHatTupleOutcomePrefixLastEquiv (params : Parameters) [FieldModel params.q] (n : ℕ) : GHatTupleOutcome params (n + 1) ≃ GHatTupleOutcome params n × GHatOutcome params

Split a completed-slice outcome tuple into the first n coordinates and the last one.

Equations

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