Proof of Entropy on the Configuration Space: Tensorization, Subadditivity over the Particles, and the One-Particle Marginal

Each result cited is universally quantified over the data in its own statement. For $n\in\mathbb{N}$ write $\mathfrak{p}^{(n)}_{k}$, $k\in[n]$, for the block maps of $\mathbb{R}^{qn}$ (Particle Blocks of the Configuration Space: Block Maps, Configurations, Product Maps and Diagonal Points §blocks with $N=n$), and $\rho^{\otimes n}$ for the tensor power in $\mathbb{R}^{qn}$ (The Tensor Power of a Probability Measure on Euclidean Space §tensor with $N=n$). A natural number used as a real number is its image under the canonical map, as in Properties of the Canonical Map from the Natural Numbers to an Ordered Field.

Step 1 (One particle). For $n=1$ we have $q\cdot1=q$ and $b(1,i)=(1-1)q+i=i$ for $i\in[q]$, so $\mathfrak{p}^{(1)}_{1}(x)=(x_{1},\dots,x_{q})=x$: the map $\mathfrak{p}^{(1)}_{1}$ is the identity of $\mathbb{R}^{q}$. Hence $(\mathfrak{p}^{(1)}_{1})_{\#}P=P$ for every $P\in\mathcal{P}(\mathbb{R}^{q})$, and for $\rho\in\mathcal{P}(\mathbb{R}^{q})$ and $B\in\mathcal{B}(\mathbb{R}^{q})$, by The Tensor Power of a Probability Measure on Euclidean Space §tensor and Finite Product Notation, $\rho^{\otimes1}(B)=\rho^{\otimes1}\bigl((\mathfrak{p}^{(1)}_{1})^{-1}(B)\bigr)=\prod_{k=1}^{1}\rho(B)=\rho(B)$; so $\rho^{\otimes1}=\rho$.

Step 2 (Adding a particle). Let $n\in\mathbb{N}$, and write $\iota=\iota^{qn,q}$, $\mathrm{pr}_{1}=\mathrm{pr}^{qn,q}_{1}$ and $\mathrm{pr}_{2}=\mathrm{pr}^{qn,q}_{2}$, on $\mathbb{R}^{q(n+1)}=\mathbb{R}^{qn+q}$. Every $z\in\mathbb{R}^{q(n+1)}$ equals $\iota(\mathrm{pr}_{1}(z),\mathrm{pr}_{2}(z))$ by Pairs of Euclidean Points: Coordinate Projections, Pairings, the Product Measure on a Euclidean Space, Borel Norm Functions and Finite Sets §projections, so Particle Blocks: Linearity, Splitting of Inner Products, Product Maps and Diagonal Shifts §concatenation gives

Consequently, for $P\in\mathcal{P}(\mathbb{R}^{q(n+1)})$ and $Q_{1}=(\mathrm{pr}_{1})_{\#}P$, the definition of the push-forward in Probability Measures on Euclidean Space and Random Vectors: Standing Notation §pushforward gives, for $B\in\mathcal{B}(\mathbb{R}^{q})$ and $k\in[n]$, $P\bigl((\mathfrak{p}^{(n+1)}_{k})^{-1}(B)\bigr)=P\bigl(\mathrm{pr}_{1}^{-1}((\mathfrak{p}^{(n)}_{k})^{-1}(B))\bigr)=Q_{1}\bigl((\mathfrak{p}^{(n)}_{k})^{-1}(B)\bigr)$; that is,

Now let $\rho\in\mathcal{P}(\mathbb{R}^{q})$; we show $\rho^{\otimes(n+1)}=\rho^{\otimes n}\boxtimes\rho$. Let $B_{1},\dots,B_{n+1}\in\mathcal{B}(\mathbb{R}^{q})$ and $A=\bigcap_{k=1}^{n}(\mathfrak{p}^{(n)}_{k})^{-1}(B_{k})$, which belongs to $\mathcal{B}(\mathbb{R}^{qn})$ since each $\mathfrak{p}^{(n)}_{k}$ is Borel (Particle Blocks: Linearity, Splitting of Inner Products, Product Maps and Diagonal Shifts §linear). Every $k\in[n+1]$ lies in $[n]$ or equals $n+1$ (claim 5 of Properties of the Order on the Natural Numbers), so by (1) a point $z$ lies in $\bigcap_{k=1}^{n+1}(\mathfrak{p}^{(n+1)}_{k})^{-1}(B_{k})$ exactly when $\mathrm{pr}_{1}(z)\in A$ and $\mathrm{pr}_{2}(z)\in B_{n+1}$. As $z=\iota(\mathrm{pr}_{1}(z),\mathrm{pr}_{2}(z))$ and $\mathrm{pr}_{1}(\iota(u,v))=u$, $\mathrm{pr}_{2}(\iota(u,v))=v$, this holds exactly when $z\in\iota(A\times B_{n+1})$. By Pairs of Euclidean Points: Coordinate Projections, Pairings, the Product Measure on a Euclidean Space, Borel Norm Functions and Finite Sets §product, The Tensor Power of a Probability Measure on Euclidean Space §tensor for $\rho^{\otimes n}$, and the recursion of Finite Product Notation ($n+1\ge2$),

Since $\rho^{\otimes n}\boxtimes\rho\in\mathcal{P}(\mathbb{R}^{qn+q})=\mathcal{P}(\mathbb{R}^{q(n+1)})$, the uniqueness in Existence and Uniqueness of Tensor Powers, and the Average of the Block Marginals §tensor (with $N=n+1$) gives $\rho^{\otimes(n+1)}=\rho^{\otimes n}\boxtimes\rho$.

Step 3 (Claim 1). Fix $\rho\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$ and let $T$ be the set of $n\in\mathbb{N}$ with $\rho^{\otimes n}\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{qn})$ and $\mathrm{Ent}(\rho^{\otimes n})=n\,\mathrm{Ent}(\rho)$. By Step 1, $1\in T$. If $n\in T$, then by Step 2 and Entropy of Products, Subadditivity over Two Marginals, and Convexity of the Entropy §product (with dimensions $qn$ and $q$), $\rho^{\otimes(n+1)}=\rho^{\otimes n}\boxtimes\rho\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q(n+1)})$ and $\mathrm{Ent}(\rho^{\otimes(n+1)})=n\,\mathrm{Ent}(\rho)+\mathrm{Ent}(\rho)=(n+1)\,\mathrm{Ent}(\rho)$, using claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field; so $n+1\in T$. As $n+1$ is the successor of $n$ (claim 1 of Arithmetic of Addition on the Natural Numbers), Principle of Induction for the Natural Numbers gives $T=\mathbb{N}$, and in particular $N\in T$.

Step 4 (Claim 2). Let $U$ be the set of $n\in\mathbb{N}$ such that for every $P\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{qn})$ each $(\mathfrak{p}^{(n)}_{k})_{\#}P$, $k\in[n]$, belongs to $\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$ and $\sum_{k=1}^{n}\mathrm{Ent}\bigl((\mathfrak{p}^{(n)}_{k})_{\#}P\bigr)\le\mathrm{Ent}(P)$. By Step 1 and $\sum_{k=1}^{1}a_{k}=a_{1}$ (claim 1 of Properties of Finite Sums), $1\in U$. Let $n\in U$ and $P\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q(n+1)})$, and put $Q_{1}=(\mathrm{pr}_{1})_{\#}P$, $Q_{2}=(\mathrm{pr}_{2})_{\#}P$ as in Step 2. By Entropy of Products, Subadditivity over Two Marginals, and Convexity of the Entropy §subadditive (with dimensions $qn$ and $q$), $Q_{1}\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{qn})$, $Q_{2}\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$ and $\mathrm{Ent}(Q_{1})+\mathrm{Ent}(Q_{2})\le\mathrm{Ent}(P)$. By (2), $(\mathfrak{p}^{(n+1)}_{n+1})_{\#}P=Q_{2}$ and, for $k\in[n]$, $(\mathfrak{p}^{(n+1)}_{k})_{\#}P=(\mathfrak{p}^{(n)}_{k})_{\#}Q_{1}$, which belongs to $\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$ since $n\in U$. Every $k\in[n+1]$ lies in $[n]$ or equals $n+1$, so all particle laws of $P$ belong to $\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$, and by the recursion in claim 1 of Properties of Finite Sums and $n\in U$,

Hence $n+1\in U$, and Principle of Induction for the Natural Numbers gives $U=\mathbb{N}$; in particular $N\in U$.

Step 5 (Claim 3). Let $P\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{qN})$ and $\mu_{k}=(\mathfrak{p}_{k})_{\#}P$ for $k\in[N]$; by Step 4, $\mu_{k}\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$ and $\sum_{k=1}^{N}\mathrm{Ent}(\mu_{k})\le\mathrm{Ent}(P)$. Put $t_{k}=N^{-1}$, which is positive by claim 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field. By The One-Particle Marginal of a Probability Measure on the Configuration Space §marginal and claim 3 of Properties of Finite Sums, $P^{[1]}(B)=N^{-1}\sum_{k=1}^{N}\mu_{k}(B)=\sum_{k=1}^{N}t_{k}\mu_{k}(B)$ for $B\in\mathcal{B}(\mathbb{R}^{q})$; for $B=\mathbb{R}^{q}$, where $\mu_{k}(\mathbb{R}^{q})=P(\mathbb{R}^{qN})=1$, this reads $\sum_{k=1}^{N}t_{k}=P^{[1]}(\mathbb{R}^{q})=1$, $P^{[1]}$ being a probability measure. Hence Entropy of Products, Subadditivity over Two Marginals, and Convexity of the Entropy §convex (with $n=N$) applies and gives $P^{[1]}\in\mathcal{P}_{2}^{\mathrm{Ent}}(\mathbb{R}^{q})$ and, with claim 3 of Properties of Finite Sums and claim 5 of Elementary Arithmetic in an Ordered Field ($0\le N^{-1}$),

Multiplying by $N\ge0$ (claim 5 of Elementary Arithmetic in an Ordered Field) gives $N\,\mathrm{Ent}(P^{[1]})\le\mathrm{Ent}(P)$.