Conditional subentropy and guessing

Abstract

The simplex-integral conditional subentropy of a classical-quantum state is bounded by guessing min-entropy.

Definition 1.1 (C).

$$\forall n\in \mathbb{N},C\left(n\right)=\sum _{k\in \mathrm{Finset}.\mathrm{Icc}\left(2,n\right)}(\frac{1}{(k:\mathbb{R})})$$

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

Citation. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

Equation (2), PDF page 2: “Q(ρ) = ⟨H(M(ρ))⟩_M − C_n where C_n := 1/2 + 1/3 + … + 1/n.” The sum runs from 2 through n, inclusive.

Definition 1.2 (simplexCoords).

$$\forall n\in \mathbb{N},\mathrm{simplexCoords}\left(n\right)=\{y:\mathrm{Fin}\left(n-1\right)\to \mathbb{R}|(\forall i\in \mathrm{Fin}\left(n-1\right),0\le y\left(i\right))\wedge (\sum _{i\in \mathrm{Fin}\left(n-1\right)}(y\left(i\right))\le 1)\}$$

Formalization. D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.simplexCoords (✓ std3).

Citation. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

Equation (3), PDF page 2: “this uniform measure (normalised to have total volume unity) is given by dx = (n − 1)! dx_1 … dx_{n−1}.” The first n−1 coordinates are nonnegative and have sum at most one.

Lemma 1.3 (simplex_volume).

$$\forall n\in \mathbb{N},\mathrm{volume}\left(\mathrm{simplexCoords}\left(n+1\right)\right)=(\mathrm{Nat}.\mathrm{factorial}\left(n\right):\mathrm{ENNReal}{)}^{-1}$$

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

Source. Repository-derived.

Commentary.

The standard simplex in n coordinates has volume equal to the reciprocal of n factorial.

Lemma 1.4 (simplex_sum_boundary_null).

$$\forall n\in \mathbb{N},\forall t\in \mathbb{R},(0<t)\Rightarrow (\mathrm{volume}\left(\{u:\mathrm{Fin}\left(n\right)\to \mathbb{R}|\sum _{i\in \mathrm{Fin}\left(n\right)}(u\left(i\right))=t\}\right)=0)$$

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

Source. Repository-derived.

Commentary.

Every positive level set of the coordinate sum has zero volume.

Definition 1.5 (subentropySpectrum).

$$\forall n\in \mathbb{N},\forall lam\in \mathrm{Fin}\left(n\right)\to \mathbb{R},\mathrm{subentropySpectrum}\left(n,lam\right)=(n:\mathbb{R})\cdot ((\mathrm{Nat}.\mathrm{factorial}\left(n-1\right):\mathbb{R})\cdot {\int }_{y\in \mathrm{simplexCoords}\left(n\right)}(\mathrm{Real}.\mathrm{negMulLog}\left(\sum _{i\in \mathrm{Fin}\left(n\right)}(lam\left(i\right)\cdot D5.S3.\mathrm{Geometry}.\mathrm{AlphaGeometry}.\mathrm{PositiveSimplexGeometryAndMixing}.\mathrm{chart}\left(y,i\right))\right))dy)-C\left(n\right)$$

Formalization. D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.subentropySpectrum (✓ std3).

Citation. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

Equation (4), PDF page 2: “Introducing η(y) := −y ln y, we then obtain a third expression for the subentropy from eq.(2): Q(ρ) = n ∫_{Δn} η(λ · x) dx − C_n.” Real.negMulLog is η. The Lebesgue integral is multiplied by (n−1)!, as in equation (3).

Definition 1.6 (subentropy).

$$\forall I\in \mathrm{Type},[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall R\in \mathrm{Matrix}\left(I,I,\mathbb{C}\right),\forall hR\in \mathrm{Matrix}.\mathrm{IsHermitian}\left(R\right),\mathrm{subentropy}\left(R,hR\right)=\mathrm{subentropySpectrum}\left(\mathrm{Fintype}.\mathrm{card}\left(I\right),\left(\mathrm{Matrix}.\mathrm{IsHermitian}.{\mathrm{eigenvalues}}_0\right)\left(hR\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.subentropy (✓ std3).

Citation. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

Equation (4), PDF page 2: “Introducing η(y) := −y ln y, we then obtain a third expression for the subentropy from eq.(2): Q(ρ) = n ∫_{Δn} η(λ · x) dx − C_n.” R supplies its real Hermitian eigenvalues, including zero and repeated eigenvalues.

Definition 1.7 (pGuess).

$$\forall X\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(X\right)][\mathrm{Fintype}\left(B\right)][\mathrm{DecidableEq}\left(B\right)]\forall A\in X\to \mathrm{Matrix}\left(B,B,\mathbb{C}\right),\mathrm{pGuess}\left(A\right)=\mathrm{sSup}\left(\{s:\mathbb{R}|\exists E\in X\to \mathrm{Matrix}\left(B,B,\mathbb{C}\right),(\forall x\in X,\mathrm{Matrix}.\mathrm{PosSemidef}\left(E\left(x\right)\right))\wedge ((\sum _{x\in X}(E\left(x\right))=1)\wedge (s=\mathrm{Complex}.\mathrm{re}\left(\sum _{x\in X}(\mathrm{Matrix}.\mathrm{trace}\left(E\left(x\right)\cdot A\left(x\right)\right))\right)))\}\right)$$

Formalization. D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.pGuess (✓ std3).

Citation. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

PDF page 9: “p_guess(X|B) = max_{{E_x}:POVM} Σ_x p_x Tr(E_x ρ^x_B), where the maximization is over all possible POVMs: {E_x : E_x ≥ 0 ∀ x; Σ_x E_x = I}.” A x is p_xρ_B^x. The supremum is over these finite-POVM scores.

Definition 1.8 (claim).

$$\mathrm{claim}=(\forall X\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(X\right)][\mathrm{DecidableEq}\left(X\right)][\mathrm{Fintype}\left(B\right)][\mathrm{DecidableEq}\left(B\right)]\forall A\in X\to \mathrm{Matrix}\left(B,B,\mathbb{C}\right),(\forall x\in X,\mathrm{Matrix}.\mathrm{PosSemidef}\left(A\left(x\right)\right))\Rightarrow ((\sum _{x\in X}(\mathrm{Matrix}.\mathrm{trace}\left(A\left(x\right)\right))=1)\Rightarrow (\forall hXB\in \mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{Matrix}.\mathrm{blockDiagonal}\left(A\right)\right),\forall hB\in \mathrm{Matrix}.\mathrm{IsHermitian}\left(\sum _{x\in X}(A\left(x\right))\right),\mathrm{subentropy}\left(\mathrm{Matrix}.\mathrm{blockDiagonal}\left(A\right),hXB\right)-\mathrm{subentropy}\left(\sum _{x\in X}(A\left(x\right)),hB\right)\le -\mathrm{Real}.\log \left(\mathrm{pGuess}\left(A\right)\right))))$$

Formalization. D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.claim (✓ std3).

Citation. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

Conjecture 2, PDF page 9: “For a c-q state ρ_XB, the conditional subentropy Q(X|B) satisfies the following bound: Q(X|B) ≤ H_min(X|B) = − ln p_guess(X|B).” Equation (13), PDF page 8: “we define the conditional subentropy to be Q(A|B)_ρ := Q(ρ_AB) − Q(ρ_B)”. X and B are arbitrary finite types with decidable equality. A has positive semidefinite blocks of total trace one. Matrix.blockDiagonal A is the joint state, and the sum of A is its B marginal. Natural logarithms are used.

Theorem 1.9 (result).

$$\forall X\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(X\right)][\mathrm{DecidableEq}\left(X\right)][\mathrm{Fintype}\left(B\right)][\mathrm{DecidableEq}\left(B\right)]\forall A\in X\to \mathrm{Matrix}\left(B,B,\mathbb{C}\right),(\forall x\in X,\mathrm{Matrix}.\mathrm{PosSemidef}\left(A\left(x\right)\right))\Rightarrow ((\sum _{x\in X}(\mathrm{Matrix}.\mathrm{trace}\left(A\left(x\right)\right))=1)\Rightarrow (\forall hXB\in \mathrm{Matrix}.\mathrm{IsHermitian}\left(\mathrm{Matrix}.\mathrm{blockDiagonal}\left(A\right)\right),\forall hB\in \mathrm{Matrix}.\mathrm{IsHermitian}\left(\sum _{x\in X}(A\left(x\right))\right),\mathrm{subentropy}\left(\mathrm{Matrix}.\mathrm{blockDiagonal}\left(A\right),hXB\right)-\mathrm{subentropy}\left(\sum _{x\in X}(A\left(x\right)),hB\right)\le -\mathrm{Real}.\log \left(\mathrm{pGuess}\left(A\right)\right)))$$

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

Resolves. Problems/datta-dorlas-jozsa-benatti-2014-conditional-subentropy-conjecture-2 (proved) by D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.result.

Source. Repository-derived.

Acknowledgement. Nilanjana Datta, Tony Dorlas, Richard Jozsa, Fabio Benatti (2014). Properties of subentropy. DOI: 10.48550/arXiv.1310.1312. URL: https://arxiv.org/abs/1310.1312v1.

Commentary.

The simplex integral equals the determinant-integral subentropy on positive semidefinite trace-one matrices. Gaussian radial decomposition proves this equality without a simple-spectrum assumption. Normalizing the nonzero blocks gives a probability ensemble; zero blocks contribute zero. The ensemble guessing bound gives the inequality.

References

• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.C
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.claim
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.pGuess
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.result
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.simplexCoords
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.simplex_sum_boundary_null
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.simplex_volume
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.subentropy
• Truth anchor: D5/S3/Quantum/Measurement/ConditionalSubentropyGuessingBound.subentropySpectrum
• Dependency: D5/S3/Geometry/AlphaGeometry/PositiveSimplexGeometryAndMixing
• Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel
• Dependency: D5/S3/Quantum/Information/OrthogonalRecordEntropy
• Dependency: D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace
• Dependency: D5/S3/Quantum/Subentropy/Basic
• Dependency: D5/S3/Quantum/Subentropy/ClassicalQuantumGram
• Dependency: D5/S3/Quantum/Subentropy/GaussianMatrix
• Dependency: D5/S3/Quantum/Subentropy/GaussianQuadratic
• Dependency: D5/S3/Quantum/Subentropy/GuessingProbability
• Dependency: D5/S3/Quantum/Subentropy/POVMGram
• Dependency: D5/S3/StatisticalMechanics/RandomWalks/RenewalMinorantMaximalityRefutation