Conditioning on a classical question register #
Exact squared-norm identities behind lem:conditional and
lem:commutation-simplification. The question-indexed versions allow different
tensor decompositions for different outcomes; they introduce no dimension factor.
In a bipartite model (Phase 4 of planning/mipco-track.md) the auxiliary state is a model Ξ,
and the question register a vector ψ of ℂ^{V × W} adjoined to it
(BipartiteModel.expand): a product operator Q ⊗ A of the matrix analysis is smulKron A Q.
theorem
MIPRE.Introspection.stateSqNorm_expVec_kron
{V : Type u_1}
{W : Type u_2}
[Fintype V]
[DecidableEq V]
[Fintype W]
[DecidableEq W]
{H : Type u_3}
{K : Type u_4}
[Fintype H]
[DecidableEq H]
[Fintype K]
[DecidableEq K]
(ψ : V × W → ℂ)
(ξ : H × K → ℂ)
(Q : Matrix V V ℂ)
(A : Matrix H H ℂ)
:
stateSqNorm (expVec ψ ξ) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Q A) = stateSqNorm ψ Q * stateSqNorm ξ A
A product operator's squared state norm factors over a product state, in the matrix model:
the register statements of RegisterEPR and the Pauli basis test use it.
theorem
MIPRE.Introspection.stateSqNorm_one_eq
{V : Type u_1}
{W : Type u_2}
[Fintype V]
[DecidableEq V]
[Fintype W]
[DecidableEq W]
(ψ : V × W → ℂ)
:
The identity's squared state norm is the squared norm of the state.
theorem
MIPRE.Introspection.stateSqNorm_expand_smulKron
{V : Type u_1}
{W : Type u_2}
[Fintype V]
[DecidableEq V]
[Fintype W]
[DecidableEq W]
{𝒞 : Type u_3}
{𝒜 : Type u_4}
{ℬ : Type u_5}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(ψ : V × W → ℂ)
(Q : Matrix V V ℂ)
(A : 𝒜)
:
A product operator's squared state norm factors over a product state.
theorem
MIPRE.Introspection.stateSqNorm_one_of_norm
{𝒞 : Type u_3}
{𝒜 : Type u_4}
{ℬ : Type u_5}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(hΞ : ‖Ξ.ψ‖ = 1)
:
The squared norm of the identity on a unit state.
theorem
MIPRE.Introspection.conditional_sqNorm
{V : Type u_1}
{W : Type u_2}
[Fintype V]
[DecidableEq V]
[Fintype W]
[DecidableEq W]
{𝒞 : Type u_3}
{𝒜 : Type u_4}
{ℬ : Type u_5}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(ψ : V × W → ℂ)
(hψ : ‖evec ψ‖ = 1)
(hΞ : ‖Ξ.ψ‖ = 1)
(Q : Matrix V V ℂ)
(A B : 𝒜)
:
(Ξ.expand ψ).stateSqNorm (smulKron A Q - smulKron B Q) = (Ξ.expand ψ).stateSqNorm (smulKron 1 Q) * (Ξ.expand ψ).stateSqNorm (smulKron A 1 - smulKron B 1)
Selecting a question fibre is exactly averaging with its Born weight.
theorem
MIPRE.Introspection.smulKron_projector_commutator
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{𝒜 : Type u_4}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
(Q : Matrix V V ℂ)
(hQ : Q * Q = Q)
(A B : 𝒜)
:
A common projector factors out of a commutator.
theorem
MIPRE.Introspection.conditional_commutator
{V : Type u_1}
{W : Type u_2}
[Fintype V]
[DecidableEq V]
[Fintype W]
[DecidableEq W]
{𝒞 : Type u_3}
{𝒜 : Type u_4}
{ℬ : Type u_5}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(ψ : V × W → ℂ)
(hψ : ‖evec ψ‖ = 1)
(hΞ : ‖Ξ.ψ‖ = 1)
(Q : Matrix V V ℂ)
(hQ : Q * Q = Q)
(A B : 𝒜)
:
Removing the shared question projector preserves precisely the conditional error.
theorem
MIPRE.Introspection.conditional_sqNorm_sum
{X : Type u_3}
{Y : Type u_4}
[Fintype X]
[Fintype Y]
{V : X → Type u_6}
{W : X → Type u_7}
[(x : X) → Fintype (V x)]
[(x : X) → DecidableEq (V x)]
[(x : X) → Fintype (W x)]
[(x : X) → DecidableEq (W x)]
{𝒞 : X → Type u_8}
{𝒜 : X → Type u_9}
{ℬ : X → Type u_10}
[(x : X) → Ring (𝒞 x)]
[(x : X) → StarRing (𝒞 x)]
[(x : X) → Algebra ℂ (𝒞 x)]
[(x : X) → Ring (𝒜 x)]
[(x : X) → StarRing (𝒜 x)]
[(x : X) → Algebra ℂ (𝒜 x)]
[∀ (x : X), StarModule ℂ (𝒜 x)]
[(x : X) → Ring (ℬ x)]
[(x : X) → StarRing (ℬ x)]
[(x : X) → Algebra ℂ (ℬ x)]
(Ξ : (x : X) → BipartiteModel (𝒞 x) (𝒜 x) (ℬ x))
(ψ : (x : X) → V x × W x → ℂ)
(hψ : ∀ (x : X), ‖evec (ψ x)‖ = 1)
(hΞ : ∀ (x : X), ‖(Ξ x).ψ‖ = 1)
(Q : (x : X) → Matrix (V x) (V x) ℂ)
(A B : (x : X) → Y → 𝒜 x)
:
∑ x : X, ∑ y : Y, ((Ξ x).expand (ψ x)).stateSqNorm (smulKron (A x y) (Q x) - smulKron (B x y) (Q x)) = ∑ x : X,
((Ξ x).expand (ψ x)).stateSqNorm (smulKron 1 (Q x)) * ∑ y : Y, ((Ξ x).expand (ψ x)).stateSqNorm (smulKron (A x y) 1 - smulKron (B x y) 1)
Conditioning with outcome-dependent tensor decompositions, summing every answer.
theorem
MIPRE.Introspection.conditional_commutator_sum
{X : Type u_3}
{Y : Type u_4}
{Z : Type u_5}
[Fintype X]
[Fintype Y]
[Fintype Z]
{V : X → Type u_6}
{W : X → Type u_7}
[(x : X) → Fintype (V x)]
[(x : X) → DecidableEq (V x)]
[(x : X) → Fintype (W x)]
[(x : X) → DecidableEq (W x)]
{𝒞 : X → Type u_8}
{𝒜 : X → Type u_9}
{ℬ : X → Type u_10}
[(x : X) → Ring (𝒞 x)]
[(x : X) → StarRing (𝒞 x)]
[(x : X) → Algebra ℂ (𝒞 x)]
[(x : X) → Ring (𝒜 x)]
[(x : X) → StarRing (𝒜 x)]
[(x : X) → Algebra ℂ (𝒜 x)]
[∀ (x : X), StarModule ℂ (𝒜 x)]
[(x : X) → Ring (ℬ x)]
[(x : X) → StarRing (ℬ x)]
[(x : X) → Algebra ℂ (ℬ x)]
(Ξ : (x : X) → BipartiteModel (𝒞 x) (𝒜 x) (ℬ x))
(ψ : (x : X) → V x × W x → ℂ)
(hψ : ∀ (x : X), ‖evec (ψ x)‖ = 1)
(hΞ : ∀ (x : X), ‖(Ξ x).ψ‖ = 1)
(Q : (x : X) → Matrix (V x) (V x) ℂ)
(hQ : ∀ (x : X), Q x * Q x = Q x)
(A : (x : X) → Y → 𝒜 x)
(B : (x : X) → Z → 𝒜 x)
:
∑ x : X,
∑ y : Y,
∑ z : Z,
((Ξ x).expand (ψ x)).stateSqNorm
(smulKron (A x y) (Q x) * smulKron (B x z) (Q x) - smulKron (B x z) (Q x) * smulKron (A x y) (Q x)) = ∑ x : X,
((Ξ x).expand (ψ x)).stateSqNorm (smulKron 1 (Q x)) * ∑ y : Y,
∑ z : Z,
((Ξ x).expand (ψ x)).stateSqNorm
(smulKron (A x y) 1 * smulKron (B x z) 1 - smulKron (B x z) 1 * smulKron (A x y) 1)
The commutation-simplification identity with varying question and answer registers.