Documentation

MIPRE.Background.LIDT.Co.Doubling.Halving

The doubled model's quantities are role averages of the model's #

Theorem C of reports/c6b-paper-proofs.md, §4 (Lemma 5), in the vocabulary of the port and of M: every quantity of the doubled model Doubling.model hM hψ (Co/Doubling/Model.lean) built from Born probabilities is the average of the same quantity of M over the two ways of assigning the doubled players' blocks to the two players of M.

An element x of the doubled local algebra Loc M = LocA M × LocB M has the components compA hM x : 𝒜 and compB hM x : ℬ, its blocks pulled back along the ⋆-isomorphisms of IsFinitePair.equivA and IsFinitePair.equivB; on the report's local algebra 𝒜 × ℬ, translated by Doubling.equiv, they are the two coordinates (compA_equiv, compB_equiv).

The players' algebras of M are star-ordered here, as in MIPRE.LIDT.Simul.SoundIn, so that the components of a positive element are positive and POVMs transport.

The components of the doubled local algebra #

source
noncomputable def MIPRE.LIDT.Co.Doubling.compA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) :
Loc M →⋆ₐ[ℂ] 𝒜

The first component of an element of the doubled local algebra, in 𝒜: its first block, pulled back along IsFinitePair.equivA.

Equations
Instances For
    source
    noncomputable def MIPRE.LIDT.Co.Doubling.compB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) :
    Loc M →⋆ₐ[ℂ] ℬ

    The second component of an element of the doubled local algebra, in ℬ: its second block, pulled back along IsFinitePair.equivB.

    Equations
    Instances For
      source
      theorem MIPRE.LIDT.Co.Doubling.π_πA_compA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x : Loc M) :
      M.π (M.πA ((compA hM) x)) = ↑x.1

      The operator of the first component is the first block.

      source
      theorem MIPRE.LIDT.Co.Doubling.π_πB_compB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x : Loc M) :
      M.π (M.πB ((compB hM) x)) = ↑x.2

      The operator of the second component is the second block.

      source
      @[simp]
      theorem MIPRE.LIDT.Co.Doubling.compA_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (n : 𝒜 × ℬ) :
      (compA hM) ((equiv hM) n) = n.1

      The first component of a translated element of 𝒜 × ℬ is its first coordinate.

      source
      @[simp]
      theorem MIPRE.LIDT.Co.Doubling.compB_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (n : 𝒜 × ℬ) :
      (compB hM) ((equiv hM) n) = n.2

      The second component of a translated element of 𝒜 × ℬ is its second coordinate.

      source
      theorem MIPRE.LIDT.Co.Doubling.bornProb_compA_compB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (x y : Loc M) :
      M.bornProb ((compA hM) x) ((compB hM) y) = Op.qform M.ψ (↑x.1 * ↑y.2)

      The Born probability of M at two components is the operator Born probability of the blocks.

      Born probabilities #

      source
      theorem MIPRE.LIDT.Co.Doubling.bornProb_model_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (x y : Loc M) :
      (model hM hψ).toBipartite.bornProb x y = 2⁻¹ * (M.bornProb ((compA hM) x) ((compB hM) y) + M.bornProb ((compA hM) y) ((compB hM) x))

      The role average for Born probabilities (Theorem C of reports/c6b-paper-proofs.md, §4): bornProb_D(x, y) = ½ (bornProb_M(x¹, y²) + bornProb_M(y¹, x²)).

      source
      theorem MIPRE.LIDT.Co.Doubling.bornProb_model_equiv {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (n n' : 𝒜 × ℬ) :
      (model hM hψ).toBipartite.bornProb ((equiv hM) n) ((equiv hM) n') = 2⁻¹ * (M.bornProb n.1 n'.2 + M.bornProb n'.1 n.2)

      The role average for Born probabilities, on the report's local algebra 𝒜 × ℬ: bornProb_D((a, b), (a', b')) = ½ (bornProb_M(a, b') + bornProb_M(a', b)).

      The halving of the consistency quantities #

      source
      theorem MIPRE.LIDT.Co.Doubling.max_sum_sub_diag {ι : Type u_4} [Fintype ι] [DecidableEq ι] {f : ι → ι → ℝ} (hf : ∀ (a b : ι), 0 ≤ f a b) :
      max 0 (∑ a : ι, ∑ b : ι, f a b - ∑ a : ι, f a a) = ∑ a : ι, ∑ b : ι, if a = b then 0 else f a b

      The defect max 0 (total − match) of a nonnegative double sum is its off-diagonal part.

      source
      theorem MIPRE.LIDT.Co.Doubling.sum_ne_half {ι : Type u_4} [Fintype ι] [DecidableEq ι] (f g : ι → ι → ℝ) :
      (∑ a : ι, ∑ b : ι, if a = b then 0 else 2⁻¹ * (f a b + g b a)) = 2⁻¹ * ((∑ a : ι, ∑ b : ι, if a = b then 0 else f a b) + ∑ a : ι, ∑ b : ι, if a = b then 0 else g a b)

      The off-diagonal part of a role-averaged double sum is the average of the two off-diagonal parts, the second with its indices exchanged.

      source
      theorem MIPRE.LIDT.Co.Doubling.bornProb_comp_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {x y : Loc M} (hx : 0 ≤ x) (hy : 0 ≤ y) :
      0 ≤ M.bornProb ((compA hM) x) ((compB hM) y)

      The Born probabilities of M at the components of nonnegative elements are nonnegative.

      source
      theorem MIPRE.LIDT.Co.Doubling.bornProb_total_comp {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (X Y : SubMeas Outcome (Loc M)) :
      M.bornProb ((compA hM) X.total) ((compB hM) Y.total) = ∑ a : Outcome, ∑ b : Outcome, M.bornProb ((compA hM) (X.outcome a)) ((compB hM) (Y.outcome b))

      The total Born probability of two submeasurements of the doubled local algebra, at the components, is the double sum of the outcome Born probabilities.

      source
      theorem MIPRE.LIDT.Co.Doubling.qBipartiteConsDefect_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Outcome : Type u_4} [Fintype Outcome] [DecidableEq Outcome] (X Y : SubMeas Outcome (Loc M)) :
      (model hM hψ).qBipartiteConsDefect X Y = 2⁻¹ * (max 0 (M.bornProb ((compA hM) X.total) ((compB hM) Y.total) - ∑ a : Outcome, M.bornProb ((compA hM) (X.outcome a)) ((compB hM) (Y.outcome a))) + max 0 (M.bornProb ((compA hM) Y.total) ((compB hM) X.total) - ∑ a : Outcome, M.bornProb ((compA hM) (Y.outcome a)) ((compB hM) (X.outcome a))))

      The submeasurement consistency defect halves (Theorem C, Lemma 5 of reports/c6b-paper-proofs.md, §4): the port's bipartite defect of two submeasurements of the doubled model is the average of the two defects max 0 (total − match) of M, at the components X¹, Y² and Y¹, X².

      POVMs #

      source
      noncomputable def MIPRE.LIDT.Co.Doubling.povmA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (Loc M)) :
      POVMIn Λ 𝒜

      The first components of a POVM of the doubled local algebra, a POVM of 𝒜 (the report's G¹).

      Equations
      Instances For
        source
        noncomputable def MIPRE.LIDT.Co.Doubling.povmB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (Loc M)) :
        POVMIn Λ ℬ

        The second components of a POVM of the doubled local algebra, a POVM of ℬ (the report's G²).

        Equations
        Instances For
          source
          noncomputable def MIPRE.LIDT.Co.Doubling.povmPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (𝒜 × ℬ)) :
          POVMIn Λ (Loc M)

          The translation of a POVM of the report's local algebra 𝒜 × ℬ, a POVM of the doubled local algebra.

          Equations
          Instances For
            source
            @[simp]
            theorem MIPRE.LIDT.Co.Doubling.povmA_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (Loc M)) (a : Λ) :
            (povmA hM P).op a = (compA hM) (P.op a)

            The operators of povmA hM P are the first components of those of P.

            source
            @[simp]
            theorem MIPRE.LIDT.Co.Doubling.povmB_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (Loc M)) (a : Λ) :
            (povmB hM P).op a = (compB hM) (P.op a)

            The operators of povmB hM P are the second components of those of P.

            source
            @[simp]
            theorem MIPRE.LIDT.Co.Doubling.povmPair_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (𝒜 × ℬ)) (a : Λ) :
            (povmPair hM P).op a = (equiv hM) (P.op a)

            The operators of povmPair hM P are the translations of those of P.

            source
            @[simp]
            theorem MIPRE.LIDT.Co.Doubling.povmA_povmPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (𝒜 × ℬ)) :
            povmA hM (povmPair hM P) = P.fst

            The first components of a translated POVM of 𝒜 × ℬ are its first coordinates.

            source
            @[simp]
            theorem MIPRE.LIDT.Co.Doubling.povmB_povmPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ (𝒜 × ℬ)) :
            povmB hM (povmPair hM P) = P.snd

            The second components of a translated POVM of 𝒜 × ℬ are its second coordinates.

            source
            theorem MIPRE.LIDT.Co.Doubling.dis_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P Q : POVMIn Λ (Loc M)) :
            (model hM hψ).toBipartite.dis P Q = 2⁻¹ * (M.dis (povmA hM P) (povmB hM Q) + M.dis (povmA hM Q) (povmB hM P))

            The disagreement halves: the disagreement of two POVMs of the doubled model is the average of the disagreements of M at their components.

            source
            theorem MIPRE.LIDT.Co.Doubling.dis_model_pair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] (P Q : POVMIn Λ (𝒜 × ℬ)) :
            (model hM hψ).toBipartite.dis (povmPair hM P) (povmPair hM Q) = 2⁻¹ * (M.dis P.fst Q.snd + M.dis Q.fst P.snd)

            The disagreement halves, for POVMs of the report's local algebra 𝒜 × ℬ.

            source
            theorem MIPRE.LIDT.Co.Doubling.inconsistency_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] [DecidableEq Λ] {X : Type u_5} [Fintype X] (μ : X → ℝ) (P Q : X → POVMIn Λ (Loc M)) :
            (model hM hψ).toBipartite.inconsistency μ P Q = 2⁻¹ * ((M.inconsistency μ (fun (x : X) => povmA hM (P x)) fun (x : X) => povmB hM (Q x)) + M.inconsistency μ (fun (x : X) => povmA hM (Q x)) fun (x : X) => povmB hM (P x))

            The inconsistency halves: the inconsistency of two families of POVMs of the doubled model is the average of the inconsistencies of M at their components.

            source
            theorem MIPRE.LIDT.Co.Doubling.inconsistency_model_pair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {Λ : Type u_4} [Fintype Λ] [DecidableEq Λ] {X : Type u_5} [Fintype X] (μ : X → ℝ) (P Q : X → POVMIn Λ (𝒜 × ℬ)) :
            ((model hM hψ).toBipartite.inconsistency μ (fun (x : X) => povmPair hM (P x)) fun (x : X) => povmPair hM (Q x)) = 2⁻¹ * ((M.inconsistency μ (fun (x : X) => (P x).fst) fun (x : X) => (Q x).snd) + M.inconsistency μ (fun (x : X) => (Q x).fst) fun (x : X) => (P x).snd)

            The inconsistency halves, for families of POVMs of the report's local algebra 𝒜 × ℬ.