Proof of Mean-Square Deviation of the Empirical Average of a Bounded Borel Function under a Tensor Power

Each result cited is universally quantified over the data in its own statement, and is applied to the data named here. The field axioms and the rules for adding inequalities, for multiplying them by nonnegative or positive real numbers, and for handling absolute values, from Elementary Order Arithmetic in an Ordered Field, Elementary Arithmetic in an Ordered Field and Properties of the Absolute Value in an Ordered Field, are used without further mention.

Step 0 (Conventions). $N^{-1}$ exists and $0<N^{-1}$ by claim 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field. For every real $\lambda$, claim 3 of Properties of Finite Sums gives $\sum_{k=1}^{N}\lambda=\lambda\sum_{k=1}^{N}1=\lambda N$, the image of $N$ being the sum of $N$ ones by The Canonical Map from the Natural Numbers to a Field. Write $Q=\rho^{\otimes N}$, and fix a bound $M\ge0$ for $\varphi$ (Bounded Real-Valued Function on a Set). For $k\in[N]$ the block map $\mathfrak{p}_{k}$ is Borel by Particle Blocks: Linearity, Splitting of Inner Products, Product Maps and Diagonal Shifts §linear, so $\varphi_{k}=\varphi\circ\mathfrak{p}_{k}$ is Borel (a composition of Borel maps, Probability Measures on Euclidean Space and Random Vectors: Standing Notation §borel-maps) with $|\varphi_{k}|\le M$. Every bounded Borel function on $\mathbb{R}^{q}$ or on $\mathbb{R}^{qN}$ is integrable with respect to every probability measure there (Probability Measures on Euclidean Space and Random Vectors: Standing Notation §measures); products of two bounded Borel functions are bounded Borel functions (claim 3 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions); and constant functions are bounded and Borel (claim 1 there), a constant $c$ having integral $c$ against a probability measure by claim 6(a) of Borel Measurability and Bounded Integration on a Metric Space.

Step 1 (Claim 1). By Basic Properties of Empirical Measures: Values, Integrals, Push-Forwards, Second Moment, and Lipschitz Dependence on the Configuration §integral, applied to the Borel function $\varphi:\mathbb{R}^{q}\to\mathbb{R}$, $\varphi$ is integrable with respect to $\mu^{N}_{x}$ and $g(x)=N^{-1}\sum_{k=1}^{N}\varphi_{k}(x)$ for every $x$. Hence $g$ is Borel by claim 2 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions, and by claims 2 and 1 of Comparison and Absolute Value Bounds for Finite Sums of Real Numbers, claim 3 of Properties of Finite Sums and Step 0,

so $g$ is bounded.

Step 2 (One- and two-particle moments). Let $k\in[N]$. By Tensor Powers and One-Particle Marginals: Particle Laws, Product Integrals, Push-Forwards, Moments, Product Maps and Diagonal Shifts §particle-laws, $(\mathfrak{p}_{k})_{\#}Q=\rho$, so the change-of-variables formula of Probability Measures on Euclidean Space and Random Vectors: Standing Notation §pushforward, applied to the bounded Borel functions $\varphi$ and $\varphi^{2}$, gives

Now let $k,l\in[N]$ with $k\ne l$. For $m\in[N]$ let $f_{m}=\varphi$ if $m\in\{k,l\}$ and let $f_{m}$ be the constant function $1$ otherwise; these are bounded Borel functions, so Tensor Powers and One-Particle Marginals: Particle Laws, Product Integrals, Push-Forwards, Moments, Product Maps and Diagonal Shifts §product-integral gives

The finite products of Finite Product Notation are those of Finite Product Notation in a Field in the field $\mathbb{R}$, both being given by the recursion recorded in claim 1 of Properties of Finite Products. Fix $x\in\mathbb{R}^{qN}$ and, for $m\in[N]$, let $\alpha_{m}=\varphi_{k}(x)$ if $m=k$ and $\alpha_{m}=1$ otherwise, and $\beta_{m}=\varphi_{l}(x)$ if $m=l$ and $\beta_{m}=1$ otherwise. Since $k\ne l$, $f_{m}(\mathfrak{p}_{m}(x))=\alpha_{m}\beta_{m}$ for every $m$, so claims 2 and 3 of Properties of Finite Products give $\prod_{m=1}^{N}f_{m}(\mathfrak{p}_{m}(x))=\bigl(\prod_{m}\alpha_{m}\bigr)\bigl(\prod_{m}\beta_{m}\bigr)=\varphi_{k}(x)\varphi_{l}(x)$. In the same way, since $\int f_{m}\,d\rho$ is $a$ for $m\in\{k,l\}$ and $\rho(\mathbb{R}^{q})=1$ otherwise (Step 0), $\prod_{m=1}^{N}\int f_{m}\,d\rho=a\cdot a$. Therefore

Step 3 (The pair integrals). For $k\in[N]$ let $h_{k}=\varphi_{k}-a$ on $\mathbb{R}^{qN}$. For $k,l\in[N]$ the field axioms give, pointwise, $h_{k}h_{l}=\varphi_{k}\varphi_{l}-a\,\varphi_{k}-a\,\varphi_{l}+a^{2}\cdot1$, a linear combination of four integrable functions; so by Linearity of the Lebesgue Integral over a Finite Sum of Integrable Functions §integrable and Linearity of the Lebesgue Integral over a Finite Sum of Integrable Functions §linear, $h_{k}h_{l}$ is integrable and, by Steps 0 and 2,

Step 4 (Claim 2). Fix $x$ and put $T(x)=\sum_{k=1}^{N}h_{k}(x)$. By claim 2 of Properties of Finite Sums and Step 0, $T(x)=\sum_{k=1}^{N}\varphi_{k}(x)-aN$, so by Step 1 and $N^{-1}N=1$, $N^{-1}T(x)=g(x)-a$. Two applications of claim 3 of Properties of Finite Sums (with $\lambda=T(x)$, then with $\lambda=h_{k}(x)$) and commutativity give

For each $k$, Linearity of the Lebesgue Integral over a Finite Sum of Integrable Functions §integrable and Linearity of the Lebesgue Integral over a Finite Sum of Integrable Functions §linear show that $H_{k}$ is integrable with $\int H_{k}\,dQ=\sum_{l=1}^{N}e_{kl}=e_{kk}=b-a^{2}$, the middle equality by claim 7 of Properties of Finite Sums, as $e_{kl}=0$ for $l\ne k$. Applying the same lemma once more, $(g-a)^{2}$ is integrable and

by Step 0. The integral in claim 2 is that of the nonnegative Borel function $(g-a)^{2}$; it equals the real integral just computed, because the negative part of a nonnegative function is $0$ and its positive part is the function itself (Integrable Function and the Lebesgue Integral). Finally $0\le a^{2}$ by claim 2 of Nonnegativity of Squares in an Ordered Field, so $b-a^{2}\le b$, and multiplying by $0<N^{-1}$ gives $\frac{1}{N}(b-a^{2})\le\frac{1}{N}b$. This proves claim 2.