von Neumann entropy in simple type theory

[José Manuel Rodríguez Caballero]

Dear FOM members,
   For the researchers who are interested in developing mathematics in
simple type theory rather than in ZFC, to express the following theorem
(Ref 1. page 16) in the language of simple type theory may be rather
challenging:

Theorem A. Let S be a complex Hilbert space. Let P be a density operator
defined on S and let T be a closed subspace of S; we define P(T), called
the P-mass of T, as the sum of P(t), where t runs through an orthonormal
basis of T (this definition is independent of the chosen basis). Let E(P)
be the infimum of the logarithm of the dimension of T, where T runs through
the subspaces of T such that P(T) is greater than one half of P(S). Then,
the sequence E(P^N) / N, indexed by N, converges, where P^N is the N-th
tensor power of P and E(P^N) is taken with respect to the Hilbert space S^N
(N-th tensor power of S).

By the way, the limit in Theorem A is called the von Neumann entropy of P
(Ref. 2).

I would like to ask two complementary questions:
1. Is there a way to express Theorem A in a simple type theory?
2. If the answer to question 1 is negative, how could it be proved that
this theorem cannot be expressed in simple type theory?

Kind regards,
Jose M.

References:
[1] M. Gromov, In a search for a structure, part 1: On entropy. Entropy 17
(2013): 1273-1277.
URL =
https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/structre-serch-entropy-july5-2012.pdf

[2] B. Baumgartner, Characterizing Entropy in Statistical Physics and in
Quantum Information Theory
URL = https://arxiv.org/pdf/1206.5727.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200228/68db5f46/attachment.html>