OccupationPartialTransposeSpectral

Abstract

Literal occupation operators and the exact qudit partial-estimation frontier.

Theorem 1.1 (MatrixBlocks.blockDiagonal_psd).

$$\forall s\in \mathrm{Type},\forall i\in \mathrm{Type},[\mathrm{Fintype}\left(s\right)][\mathrm{DecidableEq}\left(s\right)][\mathrm{Fintype}\left(i\right)][\mathrm{DecidableEq}\left(i\right)]\forall B\in s\to \mathrm{Matrix}\left(i,i,\mathbb{C}\right),\left(\forall x\in s,\mathrm{Matrix}.\mathrm{PosSemidef}\left(B\left(x\right)\right)\right)\Rightarrow \mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{Matrix}.\mathrm{blockDiagonal}\left(B\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockDiagonal_psd (✓ std3). ∎

Source. Repository-derived.

Commentary.

A block diagonal matrix is positive semidefinite whenever every block is positive semidefinite. The blocks and their common matrix indices range over arbitrary finite types.

Definition 1.2 (occFintype).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{occFintype}\left(N,d\right)=\mathrm{Fintype}.\mathrm{ofEquiv}\left(\mathrm{Sym}\left(\mathrm{Fin}\left(d\right),N\right),\mathrm{Sym}.\mathrm{equivNatSumOfFintype}\left(\mathrm{Fin}\left(d\right),N\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.occFintype (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The symmetric-power equivalence gives the finite occupation carrier.

Definition 1.3 (symmetricProjector).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{symmetricProjector}\left(N,d\right)=\sum _{t:\{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//{\sum }_{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=N+1\}}(\mathrm{Matrix}.\mathrm{vecMulVec}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{OccupancyWordSectors}.\mathrm{sectorVector}\left(N+1,\mathrm{val}\left(\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{Sym}.\mathrm{equivNatSumOfFintype}\left(\mathrm{Fin}\left(d\right),N+1\right),t\right)\right)\right),\mathrm{star}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{OccupancyWordSectors}.\mathrm{sectorVector}\left(N+1,\mathrm{val}\left(\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{Sym}.\mathrm{equivNatSumOfFintype}\left(\mathrm{Fin}\left(d\right),N+1\right),t\right)\right)\right)\right)\right))$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.symmetricProjector (✓ std3).

Citation. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

Equation (14), p. 3, sums the projectors onto the normalized occupation vectors on the full word space.

Definition 1.4 (occupationEmbedding).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},\forall w\in \mathrm{Fin}\left(N+1\right)\to \mathrm{Fin}\left(d\right),\forall x\in \mathrm{Prod}\left(\{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=N\},\mathrm{Fin}\left(d\right)\right),\mathrm{occupationEmbedding}\left(N,d,w,x\right)=D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{OccupancyWordSectors}.\mathrm{sectorVector}\left(N,\mathrm{val}\left(\mathrm{Equiv}.\mathrm{symm}\left(\mathrm{Sym}.\mathrm{equivNatSumOfFintype}\left(\mathrm{Fin}\left(d\right),N\right),x.1\right)\right)\right)\left(\mathrm{Fin}.\mathrm{init}\left(w\right)\right)\cdot \mathrm{if}(w\left(\mathrm{Fin}.\mathrm{last}\left(N\right)\right)=x.2)\mathrm{then}1\mathrm{else}0$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.occupationEmbedding (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The occupation embedding sends an input occupation and output level to the normalized symmetric input vector times the output coordinate.

Definition 1.5 (RF).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{RF}\left(N,d\right)=(\mathrm{Inv}.\mathrm{inv}\left((\mathrm{Nat}.\mathrm{choose}\left(N+1+d-1,d-1\right):\mathbb{C})\right))\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{occupationEmbedding}\left(N,d\right)\right)\cdot \mathrm{Matrix}.\mathrm{of}\left(\mathrm{fun}(u:\mathrm{Fin}\left(N+1\right)\to \mathrm{Fin}\left(d\right))\mapsto \mathrm{fun}(v:\mathrm{Fin}\left(N+1\right)\to \mathrm{Fin}\left(d\right))\mapsto \mathrm{symmetricProjector}\left(N,d\right)\left(\mathrm{Fin}.\mathrm{snoc}\left(\mathrm{Fin}.\mathrm{init}\left(v\right),u\left(\mathrm{Fin}.\mathrm{last}\left(N\right)\right)\right),\mathrm{Fin}.\mathrm{snoc}\left(\mathrm{Fin}.\mathrm{init}\left(u\right),v\left(\mathrm{Fin}.\mathrm{last}\left(N\right)\right)\right)\right)\right)\cdot \mathrm{occupationEmbedding}\left(N,d\right))$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.RF (✓ std3).

Citation. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

RF is R_F of Eq. (12), p. 2: normalized compression of the partially transposed full symmetric projector.

Definition 1.6 (outputReferenceProjector).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{outputReferenceProjector}\left(N,d\right)=\mathrm{Matrix}.\mathrm{kronecker}\left((1:\mathrm{Matrix}\left(\{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=N\},\{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=N\},\mathbb{C}\right)),\mathrm{Matrix}.\mathrm{diagonal}\left(\mathrm{fun}(i:\mathrm{Fin}\left(d\right))\mapsto \mathrm{if}(\mathrm{val}\left(i\right)=0)\mathrm{then}(1:\mathbb{C})\mathrm{else}0\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.outputReferenceProjector (✓ std3).

Citation. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The output reference projector is the input identity tensor the projector onto output level zero, Eq. (10), p. 2.

Definition 1.7 (RG).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},\mathrm{RG}\left(N,d\right)=\mathrm{Matrix}.\mathrm{kronecker}\left(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(\mathrm{RF}\left(N,d\right)\cdot \mathrm{outputReferenceProjector}\left(N,d\right)\right),(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right))\right)$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.RG (✓ std3).

Citation. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

RG is R_G of Eq. (10), p. 2: partial trace after multiplication by the reference projector, tensor the output identity.

Definition 1.8 (A).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},A\left(N,d\right)=((\mathrm{Nat}.\mathrm{choose}\left(N+d-1,d-1\right):\mathbb{C})\cdot (N+d:\mathbb{C}))\cdot (\mathrm{RF}\left(N,d\right))$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.A (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The scaled A operator multiplies the corresponding fidelity operator by D(N,d)(N+d).

Definition 1.9 (C).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},C\left(N,d\right)=((\mathrm{Nat}.\mathrm{choose}\left(N+d-1,d-1\right):\mathbb{C})\cdot (N+d:\mathbb{C}))\cdot (\mathrm{RG}\left(N,d\right))$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.C (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The scaled C operator multiplies the corresponding fidelity operator by D(N,d)(N+d).

Definition 1.10 (Blocks.blockIndex).

$$\forall K\in \mathbb{N},\forall d\in \mathbb{N},\forall m\in \{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=K\},\forall i\in \mathrm{Fin}\left(d\right),\mathrm{blockIndex}\left(m,i\right)=(⟨\mathrm{Function}.\mathrm{update}\left(\mathrm{val}\left(m\right),i,\mathrm{val}\left(m\right)\left(i\right)+1\right)⟩,i)$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockIndex (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

A block index pairs the occupation m plus one particle at i with output level i; the subtype proof fixes total occupation K+1.

Theorem 1.11 (EntryFormula.dimension_pos).

$$\forall N\in \mathbb{N},\forall d\in \mathbb{N},1\le d\Rightarrow 0<\mathrm{Nat}.\mathrm{choose}\left(N+d-1,d-1\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.dimension_pos (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The binomial dimension is positive for every nonempty alphabet.

Definition 1.12 (Scalar.blockMaximum).

$$\forall L\in \mathbb{R},\forall p\in \mathbb{R},\forall a\in \mathbb{R},\mathrm{blockMaximum}\left(L,p,a\right)=p+\left(1-p\right)\cdot a+\frac{p\cdot L+1-p+\mathrm{Real}.\mathrm{sqrt}\left({\left(p\cdot L-\left(1-p\right)\right)}^2+4\cdot p\cdot \left(1-p\right)\cdot a\right)}{2}$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockMaximum (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The occupation block maximum consists of its scalar shift and the larger root of its rank-two part.

Definition 1.13 (Scalar.topRoot).

$$\forall a\in \mathbb{R},\forall b\in \mathbb{R},\forall c\in \mathbb{R},\mathrm{topRoot}\left(a,b,c\right)=\frac{a+c+\mathrm{Real}.\mathrm{sqrt}\left({\left(a-c\right)}^2+4\cdot b^2\right)}{2}$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The larger root of a real symmetric two by two matrix depends on its diagonal entries and off-diagonal coupling.

Definition 1.14 (Scalar.bottomRoot).

$$\forall d\in \mathbb{R},\forall s\in \mathbb{R},\forall t\in \mathbb{R},\mathrm{bottomRoot}\left(d,s,t\right)=\frac{d+t-\mathrm{Real}.\mathrm{sqrt}\left({\left(d-t\right)}^2+4\cdot s^2\right)}{2}$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.bottomRoot (✓ std3).

Source. Repository-derived.

Commentary.

The smaller root of a real symmetric two by two matrix is the half-trace minus half the discriminant’s square root.

Theorem 1.15 (Scalar.topRoot_sum).

$$\forall d\in \mathbb{R},\forall s\in \mathbb{R},\forall t\in \mathbb{R},\mathrm{topRoot}\left(d,s,t\right)+\mathrm{bottomRoot}\left(d,s,t\right)=d+t$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The sum of the two roots equals the trace.

Theorem 1.16 (Scalar.topRoot_product).

$$\forall d\in \mathbb{R},\forall s\in \mathbb{R},\forall t\in \mathbb{R},\mathrm{topRoot}\left(d,s,t\right)\cdot \mathrm{bottomRoot}\left(d,s,t\right)=d\cdot t-s^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_product (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product of the two roots equals the determinant.

Theorem 1.17 (Scalar.topRoot_bounds).

$$\forall d\in \mathbb{R},\forall s\in \mathbb{R},\forall t\in \mathbb{R},d\le \mathrm{topRoot}\left(d,s,t\right)\wedge t\le \mathrm{topRoot}\left(d,s,t\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_bounds (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The larger root dominates both diagonal entries.

Theorem 1.18 (Scalar.topRoot_determinant).

$$\forall a\in \mathbb{R},\forall b\in \mathbb{R},\forall c\in \mathbb{R},\left(\mathrm{topRoot}\left(a,b,c\right)-a\right)\cdot \left(\mathrm{topRoot}\left(a,b,c\right)-c\right)=b^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_determinant (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The spectral gap product equals the square of the off-diagonal coupling.

Theorem 1.19 (Scalar.topRoot_quadratic_bound).

$$\forall a\in \mathbb{R},\forall b\in \mathbb{R},\forall c\in \mathbb{R},\forall x\in \mathbb{R},\forall y\in \mathbb{R},a\cdot x^2+2\cdot b\cdot x\cdot y+c\cdot y^2\le \mathrm{topRoot}\left(a,b,c\right)\cdot \left(x^2+y^2\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_quadratic_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The quadratic form of a real symmetric two-by-two matrix is bounded above by its larger eigenvalue times the squared Euclidean length.

Theorem 1.20 (Complex.distinguished_block_identity).

$$\forall n\in \mathbb{R},\forall k\in \mathbb{R},\forall p\in \mathbb{R},0\le n\cdot k\Rightarrow \mathrm{blockMaximum}\left(n+k,p,n\right)=\mathrm{topRoot}\left(n+1,p\cdot \mathrm{Real}.\mathrm{sqrt}\left(n\cdot k\right),n+p\cdot \left(k+1-n\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.distinguished_block_identity (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The block supported on the reference occupation has the stated two-dimensional root.

Theorem 1.21 (BlockSpectral.rankOneQuadratic).

$$\forall I\in Type,[\mathrm{Fintype}\left(I\right)]\forall z\in I\to \mathbb{C},\forall psi\in I\to \mathbb{C},\mathrm{dotProduct}\left(\mathrm{star}\left(z\right),\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{vecMulVec}\left(psi,\mathrm{star}\left(psi\right)\right),z\right)\right)=(\mathrm{Complex}.\mathrm{normSq}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(z\right),psi\right)\right):\mathbb{C})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.rankOneQuadratic (✓ std3). ∎

Source. Repository-derived.

Commentary.

The quadratic form of a rank-one density matrix is the squared modulus of its overlap.

Definition 1.22 (BlockSpectral.blockOperator).

$$\forall I\in Type,[\mathrm{DecidableEq}\left(I\right)]\forall v\in I\to \mathbb{R},\forall i0\in I,\forall a\in \mathbb{R},\forall p\in \mathbb{R},\mathrm{blockOperator}\left(v,i0,a,p\right)=((p+\left(1-p\right)\cdot a:\mathbb{C}))\cdot ((1:\mathrm{Matrix}\left(I,I,\mathbb{C}\right)))+((p:\mathbb{C}))\cdot (\mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{fun}(i:I)\mapsto (v\left(i\right):\mathbb{C}),\mathrm{fun}(i:I)\mapsto (v\left(i\right):\mathbb{C})\right))+((1-p:\mathbb{C}))\cdot (\mathrm{Matrix}.\mathrm{diagonal}\left(\mathrm{fun}(i:I)\mapsto \mathrm{if}(i=i0)\mathrm{then}1\mathrm{else}0\right))$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockOperator (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

Each block is a scalar identity plus a real rank-one matrix and one coordinate projector.

Theorem 1.23 (BlockSpectral.blockOperator_quadratic).

$$\forall I\in Type,[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall v\in I\to \mathbb{R},\forall i0\in I,\forall a\in \mathbb{R},\forall p\in \mathbb{R},\forall x\in I\to \mathbb{C},\mathrm{dotProduct}\left(\mathrm{star}\left(x\right),\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{blockOperator}\left(v,i0,a,p\right),x\right)\right)=(\left(p+\left(1-p\right)\cdot a\right)\cdot \sum _{i:I}(\mathrm{Complex}.\mathrm{normSq}\left(x\left(i\right)\right))+p\cdot \mathrm{Complex}.\mathrm{normSq}\left(\sum _{i:I}((v\left(i\right):\mathbb{C})\cdot x\left(i\right))\right)+\left(1-p\right)\cdot \mathrm{Complex}.\mathrm{normSq}\left(x\left(i0\right)\right):\mathbb{C})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockOperator_quadratic (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The quadratic form is the sum of its norm, coherent rank-one score and reference-coordinate score.

Definition 1.24 (BlockMatrices.blockVector).

$$\forall K\in \mathbb{N},\forall d\in \mathbb{N},\forall m\in \{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=K\},\forall i\in \mathrm{Fin}\left(d\right),\mathrm{blockVector}\left(m,i\right)=\mathrm{Real}.\mathrm{sqrt}\left((\mathrm{val}\left(m\right)\left(i\right):\mathbb{R})+1\right)$$

Formalization. D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockVector (✓ std3).

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The block vector has entries sqrt(m_i+1).

Theorem 1.25 (BlockMatrices.weighted_block).

$$\forall K\in \mathbb{N},\forall d\in \mathbb{N},1\le d\Rightarrow \left(\forall m\in \{n:\mathrm{Fin}\left(d\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(d\right)}(n\left(i\right))=K\},\forall p\in \mathbb{R},\mathrm{Matrix}.\mathrm{submatrix}\left(((p:\mathbb{C}))\cdot (A\left(K+1,d\right))+((1-p:\mathbb{C}))\cdot (C\left(K+1,d\right)),\mathrm{blockIndex}\left(m\right),\mathrm{blockIndex}\left(m\right)\right)=\mathrm{blockOperator}\left(\mathrm{blockVector}\left(m\right),(0:\mathrm{Fin}\left(d\right)),(\mathrm{val}\left(m\right)\left((0:\mathrm{Fin}\left(d\right))\right):\mathbb{R})+1,p\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.weighted_block (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

Restricting the weighted fidelity operator to an occupation block gives its rank-one-plus-coordinate form.

Theorem 1.26 (GlobalBound.global_operator_bound).

$$\forall K\in \mathbb{N},\forall k\in \mathbb{N},1\le k\Rightarrow \left(\forall p\in \mathbb{R},0\le p\Rightarrow \left(p\le 1\Rightarrow \mathrm{Matrix}.\mathrm{PosSemidef}\left(((\mathrm{blockMaximum}\left((K:\mathbb{R})+(k:\mathbb{R})+1,p,(K:\mathbb{R})+1\right):\mathbb{C}))\cdot ((1:\mathrm{Matrix}\left(\mathrm{Prod}\left(\{n:\mathrm{Fin}\left(k+1\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(k+1\right)}(n\left(i\right))=K+1\},\mathrm{Fin}\left(k+1\right)\right),\mathrm{Prod}\left(\{n:\mathrm{Fin}\left(k+1\right)\to \mathbb{N}//\sum _{i:\mathrm{Fin}\left(k+1\right)}(n\left(i\right))=K+1\},\mathrm{Fin}\left(k+1\right)\right),\mathbb{C}\right)))-\mathrm{AffineMap}.\mathrm{lineMap}\left(C\left(K+1,k+1\right),A\left(K+1,k+1\right),(p:\mathbb{C})\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.global_operator_bound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Ladislav Mišta Jr., Jaromír Fiurášek (2006). Optimal partial estimation of quantum states from several copies. DOI: 10.1103/PhysRevA.74.022316. URL: https://arxiv.org/abs/quant-ph/0606112.

Commentary.

The exhaustive occupation partition and block Rayleigh bound show that the reference block dominates the complete operator, including isolated singletons.

References

• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.A
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.C
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.RF
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.RG
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockDiagonal_psd
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockIndex
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockMaximum
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockOperator
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockOperator_quadratic
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.blockVector
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.bottomRoot
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.dimension_pos
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.distinguished_block_identity
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.global_operator_bound
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.occFintype
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.occupationEmbedding
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.outputReferenceProjector
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.rankOneQuadratic
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.symmetricProjector
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_bounds
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_determinant
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_product
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_quadratic_bound
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.topRoot_sum
• Truth anchor: D5/S3/Quantum/Measurement/OccupationPartialTransposeSpectral.weighted_block
• Dependency: D5/S3/Quantum/Entanglement/OccupancyWordSectors
• Dependency: D5/S3/Quantum/Entanglement/SequentialOccupationHistory
• Dependency: D5/S3/Quantum/Information/PartialTraceMutualInformation
• Dependency: D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace