Documentation

MIPRE.Background.LIDT.Co.Pasting.SwitcherooSetup.Centers

Section 12 pasting: switcheroo centers #

Switcheroo center terms and their sandwich rewrites: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/SwitcherooSetup/Centers.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored second bipartite state ψbi : QuantumState (ι × ι) is the symmetric model S : SymModel 𝔓 K, in the vendored argument position; the slice family is an IdxPolyFamily params 𝔓 and the auxiliary family M an IdxProjSubMeas (Fq params) Outcome 𝔓. The vendored hypothesis hnorm : ψbi.IsNormalized of switcheroo_first_term_close is dropped, normalization being a theorem of the model (section "Swap symmetry is a theorem"); callers pass params S family M omega hselfM.

The two sandwich rewrites split the slice-pair average by avgOver_uniform_prod and identify the summands by S.leftTensor_mul_leftTensor (the middle one by definitional equality), in place of the vendored simp on avgOver.

Not ported #

Nothing: every declaration of the vendored file is ported here.

References #

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

source
noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateTarget {𝔓 : 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 𝔓) :
ℝ

The common comparison scalar ⟨ψ, G ⊗ M ψ⟩ from the switcheroo proof.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.Pasting.switcherooAggregateFirstTerm {𝔓 : 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 𝔓) :
    ℝ

    The first positive term in the switcheroo expansion.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateFirstTerm_eq_leftSandwich {𝔓 : 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 𝔓) :
      switcherooAggregateFirstTerm params S family M = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) fun (x : MIPStarRE.LDT.Pasting.SliceQuestion params) => Preliminaries.leftSandwichExpectation S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) M (completePartSubMeas params family x).total

      Rewrite the first positive switcheroo term as a left-sandwich average.

      source
      theorem MIPRE.LIDT.Co.Pasting.switcherooAggregateTarget_eq_middleSandwich {𝔓 : 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 𝔓) :
      switcherooAggregateTarget params S family M = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) fun (x : MIPStarRE.LDT.Pasting.SliceQuestion params) => Preliminaries.middleSandwichExpectation S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) M (completePartSubMeas params family x).total

      Rewrite the G ⊗ M switcheroo center as a middle-sandwich average.

      source
      theorem MIPRE.LIDT.Co.Pasting.switcheroo_first_term_close {𝔓 : 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 𝔓) (omega : ℝ) (hselfM : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) (switcherooSelfConsistencyLeft S params M) (switcherooSelfConsistencyRight S params M) omega) :
      have firstTerm := MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) fun (x : MIPStarRE.LDT.Pasting.SliceQuestion params) => Preliminaries.leftSandwichExpectation S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) M (completePartSubMeas params family x).total; have commonTerm := MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) fun (x : MIPStarRE.LDT.Pasting.SliceQuestion params) => Preliminaries.middleSandwichExpectation S (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Pasting.SliceQuestion params)) M (completePartSubMeas params family x).total; |firstTerm - commonTerm| ≤ 2 * √omega

      The first positive switcheroo term is close to the G ⊗ M center via the self-consistency of M.