Proof of Integrals Preserve Order, Symmetry and Positive Semidefiniteness

Real numbers are computed with as in The Real Numbers as a Type.

Proof of (i). If $u=v$, then $\int_{u}^{v}f=0=\int_{u}^{v}g$ by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vii). Let $u<v$. By The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii) and The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi), $[u,v]\subseteq E$, the restrictions $f|_{[u,v]}$ and $g|_{[u,v]}$ are bounded and integrable on $[u,v]$, and $\int_{u}^{v}f=\int_{u}^{v}f|_{[u,v]}$ and $\int_{u}^{v}g=\int_{u}^{v}g|_{[u,v]}$. For $r\in[u,v]$, $f|_{[u,v]}(r)=f(r)\le g(r)=g|_{[u,v]}(r)$, by Domains and Restrictions of Maps (iii). So Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (iii), with $u$, $v$ for $a$, $b$ and $f|_{[u,v]}$, $g|_{[u,v]}$ for $f$, $g$, gives $\int_{u}^{v}f\le\int_{u}^{v}g$.

Quadratic forms of the integral. Let $a$, $b$, $u$, $v$, $M$ and $N$ be as in the statement. By Basic Facts about Intervals of the Real Line (v), $[a,b]$ is an interval containing two distinct points; it is the interval $I$ of Rules for the Riemann Integral of Vector- and Matrix-Valued Maps, with $n$ for $p$ and $q$. By Rules for the Riemann Integral of Vector- and Matrix-Valued Maps (i), $\int_{u}^{v}M$ and $\int_{u}^{v}N$ are defined. Let $\xi\in\mathbb{R}^{n}$, and let $f_{\xi},g_{\xi}:[a,b]\to\mathbb{R}$ be the maps $r\mapsto\xi\cdot(M(r)\xi)$ and $r\mapsto\xi\cdot(N(r)\xi)$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v)). By Rules for the Riemann Integral of Vector- and Matrix-Valued Maps (vi), first with $\xi$ for $z$ and $M$ for $A$, the integral from $u$ to $v$ of $r\mapsto M(r)\xi$ is defined and equals $\bigl(\int_{u}^{v}M\bigr)\xi$; then, with $\xi$ for $z$ and $r\mapsto M(r)\xi$ for $x$, the integral of $f_{\xi}$ from $u$ to $v$ is defined and

$$\int_{u}^{v}f_{\xi}=\xi\cdot\int_{u}^{v}M(r)\xi\,dr=\xi\cdot\Bigl(\Bigl(\int_{u}^{v}M\Bigr)\xi\Bigr).\tag{1}$$

Likewise $\int_{u}^{v}g_{\xi}$ is defined and equals $\xi\cdot\bigl(\bigl(\int_{u}^{v}N\bigr)\xi\bigr)$.

Proof of (ii). $\int_{u}^{v}M$ is defined, as shown above. By Rules for the Riemann Integral of Vector- and Matrix-Valued Maps (vii), the integral from $u$ to $v$ of $r\mapsto M(r)^{\top}$ is defined and equals $\bigl(\int_{u}^{v}M\bigr)^{\top}$. Since $M(r)\in\mathcal{S}(n)$, $M(r)^{\top}=M(r)$ for every $r\in[a,b]$, by Euclidean Space and Real Matrices: Standing Notation (iv), so the map $r\mapsto M(r)^{\top}$ is $M$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)). Hence $\bigl(\int_{u}^{v}M\bigr)^{\top}=\int_{u}^{v}M$, and $\int_{u}^{v}M$, a matrix in $\mathcal{M}_{n}(\mathbb{R})$ by Riemann Integral of a Vector-Valued or Matrix-Valued Map (iv), lies in $\mathcal{S}(n)$ by Euclidean Space and Real Matrices: Standing Notation (iv).

Proof of (iii). Let $\xi\in\mathbb{R}^{n}$. For $r\in[a,b]$ with $u\le r\le v$, $f_{\xi}(r)=\xi\cdot(M(r)\xi)\ge0$, by Positive Semidefinite and Positive Definite Real Matrices (i). By Rules for Oriented Riemann Integrals of Real-Valued Maps: Sums, Scalar Multiples, Constants, Continuous Maps, Additivity and Evaluation by an Antiderivative (iii), with $[a,b]$ for $E$ and $0$ for $c$ (if $u<v$, then $[u,v]\subseteq[a,b]$ by Basic Facts about Intervals of the Real Line (ii)), the integral from $u$ to $v$ of the constant map $[a,b]\to\mathbb{R}$ with value $0$ is defined and equals $(v-u)\cdot0=0$. So (i), with $[a,b]$ for $E$, this constant map for $f$ and $f_{\xi}$ for $g$, together with (1), gives $0\le\int_{u}^{v}f_{\xi}=\xi\cdot\bigl(\bigl(\int_{u}^{v}M\bigr)\xi\bigr)$. As $\xi$ was arbitrary and $\int_{u}^{v}M\in\mathcal{S}(n)$ by (ii), $\int_{u}^{v}M$ is positive semidefinite, by Positive Semidefinite and Positive Definite Real Matrices (i).

Proof of (iv). By (ii), applied to $M$ and to $N$, $\int_{u}^{v}M$ and $\int_{u}^{v}N$ lie in $\mathcal{S}(n)$. Let $\xi\in\mathbb{R}^{n}$. For $r\in[a,b]$ with $u\le r\le v$, $M(r)\preceq N(r)$ gives $f_{\xi}(r)=\xi\cdot(M(r)\xi)\le\xi\cdot(N(r)\xi)=g_{\xi}(r)$, by The Positive Semidefinite Ordering on Symmetric Matrices (i). By (i), with $[a,b]$ for $E$ and $f_{\xi}$, $g_{\xi}$ for $f$, $g$, and by (1) and its analogue for $N$,

$$\xi\cdot\Bigl(\Bigl(\int_{u}^{v}M\Bigr)\xi\Bigr)=\int_{u}^{v}f_{\xi}\le\int_{u}^{v}g_{\xi}=\xi\cdot\Bigl(\Bigl(\int_{u}^{v}N\Bigr)\xi\Bigr).$$

As $\xi$ was arbitrary, $\int_{u}^{v}M\preceq\int_{u}^{v}N$, by The Positive Semidefinite Ordering on Symmetric Matrices (i).