\section[Cote 1 : le système d'inégalités des valeurs singulières, coefficients de Fredholm]{Cote 1 : le système d'inégalités des valeurs singulières, coefficients de Fredholm\protect\verifie{Folder1}}\label{sec:1}

La cote 1, \emph{Analyse fonctionnelle : notes manuscrites (s.d.), lettre (1953)}, compte cent quarante-neuf pages, que l'inventaire date de 1953. Les pages~70 à~73 sont une mise au net sur les puissances extérieures des opérateurs à trace. La page~71 démontre, pour $u$, $v$ à trace, l'inégalité $\alpha_n(|u+v|) \leq \sum_{p} \alpha_p(|u|)\,\alpha_{n-p}(|v|)$ (corollaire~2, formule~(14), encadrée), par le développement de $\Lambda^n(u+v)$ en produits $(\Lambda^p u) \wedge (\Lambda^{n-p} v)$. Elle énonce ensuite le théorème~2 pour $u$, $v$ compacts : la forme produit~(15), encadrée, et \q{plus précisément} le système~(16), encadré lui aussi,
\[
  \sigma_n^m(u+v) \leq \sum_{p=0}^{m} \sigma_n^p(u)\,\sigma_n^{m-p}(v), \qquad 0 \leq m \leq n,
\]
où $\sigma_n^m(w)$ est la fonction symétrique élémentaire de degré $m$ des $n$ premières valeurs singulières de $w$ (formule~(17)). La marge gauche porte \q{à réviser} le long du théorème (\lot{1}{4}{71}). La page~72 démontre~(16) par la proposition~3, $\sigma_n^m(u) = \sup |\alpha_m(v_n u)|$ sur les contractions $v_n$ de rang $\leq n$, et par~(14) appliquée à $wu$ et $wv$ (\lot{1}{4}{72}). La page~73 juge le système, en mots lus avec doute, \q{les plus fortes possibles} des inégalités qui majorent les $\rho_i(u+v)$ en fonction des $\rho_i(u)$ et des $\rho_i(v)$ (\lot{1}{4}{73}).

La piste porte sur le système~(16) tout entier. On le démontre d'abord en dimension finie pour $m \leq 2$ et pour tout $n$, sur $\mathbb R$ comme sur $\mathbb C$ : pour $m = 0$ les deux membres valent~$1$, pour $m = 1$ c'est l'inégalité de Ky Fan, et le cas $m = 2$ suit la voie de la page par $\Lambda^2$, écrite avec des mineurs d'ordre~$2$. On démontre aussi que le système, s'il vaut pour tous les $m \leq n$, entraîne la forme produit~(15). Le dernier encadré de la section démontre le système pour tous $m$ et $n$, en dimension finie complexe, d'où~(15) pour tout~$n$ et la sous-additivité de $S_p$ des pages~128 et~129 ; deux encadrés le suivent, qui l'étendent à la dimension finie réelle et démontrent la proposition~3 comme borne supérieure atteinte.

\noindent\emph{Conventions.} Les espaces $E$ et $F$ sont des espaces préhilbertiens de dimension finie sur $\mathbb R$ ou $\mathbb C$, et $d = \dim E$. Pour $T : E \to F$ linéaire, les valeurs singulières $s_0(T) \geq s_1(T) \geq \cdots$ sont les racines carrées des valeurs propres de $T^*T$, rangées par ordre décroissant et répétées selon leur multiplicité, prolongées par $0$ au-delà de l'indice $d - 1$. C'est la définition de la bibliothèque, qui indexe à partir de $0$ ; les $\rho_1, \ldots, \rho_n$ de la page sont $s_0, \ldots, s_{n-1}$. On note $(e_j)_{j < d}$ une base orthonormée de vecteurs propres de $T^*T$, rangée dans le même ordre, de sorte que $T^*T e_j = s_j(T)^2 e_j$, et l'on pose $f_j = s_j(T)^{-1}\, T e_j$, avec $f_j = 0$ lorsque $s_j(T) = 0$. Enfin
\[
  \sigma_n^m(T) = \sum_{\substack{t \subseteq \{0, \ldots, n-1\} \\ |t| = m}} \ \prod_{i \in t} s_i(T).
\]

\begin{enonce}[Pages 71 et 72, le système (16) pour $m \leq 1$\piste{1-sigma-nm-system}]
Soient $u, v : E \to F$ linéaires et $n \geq 0$.
\begin{enumerate}
\item (Ky Fan) $\displaystyle\sum_{j < n} s_j(u+v) \leq \sum_{j < n} s_j(u) + \sum_{j < n} s_j(v)$.
\item Pour $m \in \{0, 1\}$, $\sigma_n^m(u+v) \leq \sum_{p=0}^{m} \sigma_n^p(u)\,\sigma_n^{m-p}(v)$.
\end{enumerate}
\end{enonce}

\begin{enonce}[Page 71, du système (16) à la forme produit (15)]
Soient $u, v : E \to F$ linéaires et $n \geq 0$. Si $\sigma_n^m(u+v) \leq \sum_{p=0}^{m} \sigma_n^p(u)\,\sigma_n^{m-p}(v)$ pour tout $m \leq n$, alors pour tout $r \geq 0$
\[
  \prod_{i < n} \bigl(1 + r\,s_i(u+v)\bigr) \leq \prod_{i < n} \bigl(1 + r\,s_i(u)\bigr) \prod_{i < n} \bigl(1 + r\,s_i(v)\bigr).
\]
En particulier $1 + r\,s_0(u+v) \leq (1 + r\,s_0(u))(1 + r\,s_0(v))$.
\end{enonce}

\begin{lemme}\label{lem:1-bessel}
Soient $(y_i)_{i \in I}$ une famille finie de vecteurs deux à deux orthogonaux, de normes $\leq 1$, et $z$ un vecteur. Alors $\sum_i |\langle y_i, z\rangle|^2 \leq \|z\|^2$.
\end{lemme}

\begin{proof}
Posons $c_i = \langle y_i, z\rangle$, $p = \sum_i c_i y_i$ et $S = \sum_i |c_i|^2$. On a $\langle p, z\rangle = \sum_i \bar c_i c_i = S$. Par l'orthogonalité, $\langle y_i, p\rangle = c_i \|y_i\|^2$, d'où $\|p\|^2 = \sum_i |c_i|^2 \|y_i\|^2 \leq S$. L'inégalité de Cauchy-Schwarz donne $S \leq \|p\|\,\|z\|$, donc $S^2 \leq \|p\|^2 \|z\|^2 \leq S\,\|z\|^2$. Si $S > 0$, on divise par $S$ ; si $S = 0$, il n'y a rien à démontrer.
\end{proof}

\begin{lemme}\label{lem:1-poids}
Soient $(s_j)_{j \geq 0}$ une suite réelle positive et décroissante, et $c_0, \ldots, c_{d-1}$ des réels de $[0,1]$ de somme $\leq n$. Alors $\sum_{j < d} s_j c_j \leq \sum_{j < n} s_j$.
\end{lemme}

\begin{proof}
Posons $\varepsilon_j = 1$ si $j < n$ et $\varepsilon_j = 0$ sinon. Pour tout $j < d$, on a $s_j c_j \leq \varepsilon_j s_j + s_n(c_j - \varepsilon_j)$. Si $j < n$, cela s'écrit $s_j(c_j - 1) \leq s_n(c_j - 1)$, qui vient de $s_j \geq s_n$ et $c_j \leq 1$ ; si $j \geq n$, cela s'écrit $s_j c_j \leq s_n c_j$, qui vient de $s_j \leq s_n$ et $c_j \geq 0$. En sommant, $\sum_j s_j c_j \leq \sum_{j < \min(n,d)} s_j + s_n\bigl(\sum_j c_j - \min(n,d)\bigr)$. La somme des $c_j$ est $\leq n$ par hypothèse et $\leq d$ puisque chaque $c_j$ est $\leq 1$ ; le second terme est donc $\leq 0$, et le premier est $\leq \sum_{j<n} s_j$ puisque les $s_j$ sont positifs.
\end{proof}

\begin{lemme}\label{lem:1-schmidt}
Soit $T : E \to F$ linéaire. Pour tous $j$, $k < d$, $\langle Te_j, Te_k\rangle = s_k(T)^2 \langle e_j, e_k\rangle$. En conséquence $\|Te_j\| = s_j(T)$, $Te_j = s_j(T)\, f_j$, les $f_j$ sont deux à deux orthogonaux et de normes $\leq 1$, et $\langle f_j, Te_j\rangle = s_j(T)$.
\end{lemme}

\begin{proof}
On a $\langle Te_j, Te_k\rangle = \langle e_j, T^*Te_k\rangle = s_k(T)^2 \langle e_j, e_k\rangle$. Pour $j = k$, cela donne $\|Te_j\|^2 = s_j(T)^2$. Si $s_j(T) = 0$, alors $Te_j = 0 = s_j(T) f_j$ ; sinon $s_j(T) f_j = Te_j$ par définition. Pour $j \neq k$, $\langle f_j, f_k\rangle$ est un multiple de $\langle Te_j, Te_k\rangle = 0$. La norme de $f_j$ vaut $s_j(T)^{-1} s_j(T)$, c'est-à-dire $1$, ou $0$ si $s_j(T) = 0$. Enfin $\langle f_j, Te_j\rangle = s_j(T)^{-1} \|Te_j\|^2 = s_j(T)$, les deux membres étant nuls si $s_j(T) = 0$.
\end{proof}

\begin{lemme}[principe de Ky Fan, majoration]\label{lem:1-kyfan}
Soient $T : E \to F$ linéaire, $I$ un ensemble fini à au plus $n$ éléments, $(x_i)_{i \in I}$ dans $E$ et $(y_i)_{i \in I}$ dans $F$ deux familles chacune formée de vecteurs deux à deux orthogonaux de normes $\leq 1$. Alors
\[
  \Bigl| \sum_{i \in I} \langle y_i, T x_i\rangle \Bigr| \leq \sum_{j < n} s_j(T).
\]
\end{lemme}

\general{SingularValuesSigmaTwo}

\begin{proof}[Démonstration du premier énoncé]
(1) Appliquons le lemme~\ref{lem:1-schmidt} à $w = u + v$, et soit $I$ l'ensemble des $j < d$ tels que $j < n$ ; il a $\min(n, d)$ éléments. Comme $s_j(w) = 0$ pour $j \geq d$, $\sum_{j < n} s_j(w) = \sum_{j \in I} s_j(w) = \sum_{j \in I} \langle f_j, w e_j\rangle$, et cette somme est égale à
\[
  \sum_{j \in I} \langle f_j, u e_j\rangle + \sum_{j \in I} \langle f_j, v e_j\rangle .
\]
Les familles $(e_j)$ et $(f_j)$, indexées par $I$, vérifient les hypothèses du lemme~\ref{lem:1-kyfan}. Appliqué à $T = u$ puis à $T = v$, il majore les deux sommes en module par $\sum_{j<n} s_j(u)$ et $\sum_{j<n} s_j(v)$.

(2) On a $\sigma_n^0 = 1$, la seule partie à $0$ élément étant vide, et $\sigma_n^1(T) = \sum_{j<n} s_j(T)$. Pour $m = 0$, l'inégalité est $1 \leq 1$. Pour $m = 1$, son second membre est $\sigma_n^1(v) + \sigma_n^1(u)$, et c'est~(1).
\end{proof}

\begin{proof}[Démonstration du second énoncé]
En développant le produit,
\[ \textstyle\prod_{i<n}(1 + r a_i) = \sum_{m=0}^{n} r^m e_m(a_0, \ldots, a_{n-1}), \]
où $e_m$ est la fonction symétrique élémentaire de degré $m$ ; appliqué aux valeurs singulières, cela donne $\prod_{i<n}(1 + r s_i(T)) = \sum_{m \leq n} r^m \sigma_n^m(T)$. Posons $A_m = \sigma_n^m(u)$, $B_m = \sigma_n^m(v)$ et $C_m = \sigma_n^m(u+v)$, tous positifs. L'hypothèse donne
\[
  \sum_{m \leq n} r^m C_m \leq \sum_{m \leq n} \ \sum_{p \leq m} r^p A_p\, r^{m-p} B_{m-p} .
\]
En échangeant les sommations et en posant $k = m - p$, le second membre est la somme des $r^p A_p\, r^k B_k$ sur les couples $(p, k)$ tels que $p + k \leq n$. Les termes étant positifs, elle est au plus la somme sur tous les couples $p, k \leq n$, qui vaut $\bigl(\sum_{p \leq n} r^p A_p\bigr)\bigl(\sum_{k \leq n} r^k B_k\bigr)$. Pour $n = 1$, l'hypothèse porte sur $m \in \{0, 1\}$ et c'est le premier énoncé.
\end{proof}

\begin{remarque}
Pour $m = 1$, le système~(16) est l'inégalité de Ky Fan, publiée en 1951 \cite{fan1951} ; l'inventaire date la cote de 1953. L'inégalité est démontrée ici par la voie classique du principe du maximum, et non par celle des pages~71 et~72, qui passe par les puissances extérieures, le corollaire~2 et la proposition~3 ; pour $m = 1$, la démonstration de la page revient d'ailleurs au même principe : $\alpha_1(|wu|) = \operatorname{Tr}|wu|$ avec $w$ de rang $\leq n$ et de norme $\leq 1$. La bibliothèque utilisée définit les valeurs singulières d'une application linéaire entre espaces de dimension finie et en démontre la décroissance, mais elle ne contient ni le principe de Ky Fan ni son inégalité (voir aussi \cite{bhatia1997}). Le lemme~\ref{lem:1-kyfan} ne demande pas que les familles soient orthonormées : il suffit qu'elles soient orthogonales et de normes $\leq 1$, et l'on peut donc y prendre la famille $(f_j)$, dont certains termes peuvent être nuls.
\end{remarque}

\begin{remarque}
Le second énoncé est l'implication que la page énonce par \q{et plus précisément} : le système~(16) donne~(15) coefficient par coefficient, sans autre hypothèse que la positivité des valeurs singulières. La réciproque n'est pas démontrée ici ; la piste affirme que le système est strictement plus fort que~(15), et ce point n'est pas vérifié. Pour $n = 1$, (15) se réduit à $s_0(u+v) \leq s_0(u) + s_0(v)$, qui est l'inégalité triangulaire pour la norme d'opérateur. La ligne coupée au bas de la page~71 mentionne~(16) et $n = 1$ ; le reste de la ligne est illisible.
\end{remarque}

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 71 et 72, le système (16) pour $m = 2$\piste{1-sigma-nm-system}]
Soient $u, v : E \to F$ linéaires et $n \geq 0$. Alors
\[
  \sigma_n^2(u+v) \leq \sigma_n^2(u) + \sigma_n^1(u)\,\sigma_n^1(v) + \sigma_n^2(v).
\]
Le système~(16) vaut donc pour $m \leq 2$ et tout $n$, et la forme produit~(15) pour $n \leq 2$.
\end{theoreme}
\end{encadre}

\noindent\emph{Notations.} Pour une partie finie $I$, des familles $(x_i)_{i \in I}$ dans $E$, $(y_i)_{i \in I}$ dans $F$ et $T, T' : E \to F$, on pose
\[
  B(T, T') = \sum_{i, j \in I} \bigl( \langle y_i, Tx_i\rangle \langle y_j, T'x_j\rangle - \langle y_i, Tx_j\rangle \langle y_j, T'x_i\rangle \bigr),
\]
somme des mineurs principaux mixtes d'ordre~$2$ des matrices $(\langle y_i, Tx_j\rangle)$ et $(\langle y_i, T'x_j\rangle)$, prise sur les couples ordonnés. Pour des familles $(g_k)$, $(g'_l)$, $(h_i)$ d'un même espace, on pose $M_{kl,ij} = \langle g_k, h_i\rangle \langle g'_l, h_j\rangle - \langle g_k, h_j\rangle \langle g'_l, h_i\rangle$, qui est $\langle g_k \wedge g'_l, h_i \wedge h_j\rangle$ au sens de $\Lambda^2$, puis $\Lambda_{kl} = \sum_{i,j \in I} |M_{kl,ij}|^2$ et $p_k = \sum_{i \in I} |\langle g_k, h_i\rangle|^2$.

\begin{lemme}[Lagrange]\label{lem:1-lagrange}
Pour des scalaires $a_i$, $b_i$ indexés par un ensemble fini $I$, $\sum_{i,j \in I} |a_i b_j - a_j b_i|^2 \leq 2 \sum_i |a_i|^2 \sum_i |b_i|^2$. En particulier $\Lambda_{kl} \leq 2\,p_k\,p'_l$, où $p'_l$ est formé avec $(g'_l)$.
\end{lemme}

\general{SingularValuesSigmaTwo}

\begin{lemme}[poids pour $\sigma^2$]\label{lem:1-poids2}
Soient $K$ un ensemble fini, $G \subseteq K$, des réels $s_k \geq 0$ et $\theta \geq 0$ avec $s_k \geq \theta$ pour $k \in G$ et $s_k \leq \theta$ pour $k \notin G$. Soient $(\alpha_{kl})$ symétrique, à coefficients dans $[0,1]$, de diagonale nulle, et $p_k \in [0,1]$ avec $\sum_k p_k \leq |G|$ et $\sum_l \alpha_{kl} \leq (|G| - 1)\,p_k$ pour tout~$k$. Alors
\[
  \sum_{k,l} \alpha_{kl}\, s_k s_l \leq \Bigl(\sum_{k \in G} s_k\Bigr)^2 - \sum_{k \in G} s_k^2 .
\]
\end{lemme}

\begin{proof}
Posons $g = |G|$, $m_k = \min(s_k, \theta)$ et $d_k = s_k - m_k$. On a $0 \leq m_k \leq \theta$, $d_k \geq 0$, $m_k = \theta$ sur $G$ et $d_k = 0$ hors de $G$ ; soit $D = \sum_{k \in G} d_k$. On développe $s_k s_l = m_km_l + m_kd_l + d_km_l + d_kd_l$ et l'on majore les quatre sommes. D'abord $\sum \alpha_{kl} m_k m_l \leq \theta^2 \sum_k (g-1)p_k \leq \theta^2 (g-1) g$ ; si $g = 0$, la somme des $p_k$ est nulle. Ensuite $\sum \alpha_{kl} m_k d_l \leq \theta \sum_l d_l \sum_k \alpha_{lk} \leq \theta \sum_l d_l (g-1) p_l \leq \theta (g-1) D$, car $d_l = 0$ hors de $G$ et $g \geq 1$ dès que $G$ a un élément ; de même pour $\sum \alpha_{kl} d_k m_l$. Enfin $\sum \alpha_{kl} d_k d_l \leq \sum_{k \neq l} d_k d_l = D^2 - \sum_{k \in G} d_k^2$. Le total vaut $g(g-1)\theta^2 + 2(g-1)\theta D + D^2 - \sum_G d_k^2$, et c'est $(g\theta + D)^2 - \sum_G (\theta + d_k)^2$, le second membre.
\end{proof}

\begin{lemme}[Cauchy--Binet pour les mineurs d'ordre $2$]\label{lem:1-binet}
Dans un anneau commutatif, si $A_{ij} = \sum_k s_k P_{ik} Q_{kj}$ et $C_{ij} = \sum_l t_l P'_{il} Q'_{lj}$, alors
\[
  2 \sum_{i,j} (A_{ii}C_{jj} - A_{ij}C_{ji}) = \sum_{k,l} s_k t_l \sum_{i,j} (P_{ik}P'_{jl} - P_{jk}P'_{il})(Q_{ki}Q'_{lj} - Q_{kj}Q'_{li}).
\]
\end{lemme}

\begin{proof}
On développe le produit de droite en quatre termes ; l'échange de $i$ et $j$ identifie le quatrième au premier et le troisième au deuxième. Le membre de gauche, développé par bilinéarité, donne les mêmes termes.
\end{proof}

\begin{proof}[Démonstration du troisième énoncé]
Si $n = 0$, les deux membres sont nuls. Sinon, soient $w = u + v$, $I$ l'ensemble des $j < d$ tels que $j < n$, $x_i = e_i(w)$ et $y_i = f_i(w)$ pour $i \in I$ ; ces familles sont orthogonales et de normes $\leq 1$ (lemme~\ref{lem:1-schmidt}), et $|I| \leq n$.

\emph{Le cas $T = T' = w$.} On a $\langle f_i(w), w e_j(w)\rangle = s_i(w)$ si $i = j$ et $0$ sinon. Donc $B(w, w) = \sum_{i,j \in I} s_is_j - \sum_{i \in I} s_i^2 = (\sum_I s_i)^2 - \sum_I s_i^2$, avec $s_i = s_i(w)$. Comme $s_i(w) = 0$ pour $i \geq d$, cette quantité est $(\sum_{i<n} s_i)^2 - \sum_{i<n} s_i^2 = 2\sigma_n^2(w)$.

\emph{Bilinéarité.} $B(w, w) = B(u,u) + B(u,v) + B(v,u) + B(v,v)$.

\emph{Majoration générale.} Pour $T$, écrivons $s_k = s_k(T)$, $e_k = e_k(T)$, $f_k = f_k(T)$, et de même $t_l$, $e'_l$, $f'_l$ pour $T'$. Le développement de $x$ sur $(e_k)$ donne $\langle y, Tx\rangle = \sum_k s_k\, \overline{\langle f_k, y\rangle}\, \langle e_k, x\rangle$. Le lemme~\ref{lem:1-binet}, avec $P_{ik} = \overline{\langle f_k, y_i\rangle}$ et $Q_{kj} = \langle e_k, x_j\rangle$, donne
\[
  2B(T, T') = \sum_{k,l} s_k t_l \sum_{i,j \in I} \overline{M^f_{kl,ij}}\; M^e_{kl,ij},
\]
où $M^f$ est formé avec $(f_k)$, $(f'_l)$, $(y_i)$ et $M^e$ avec $(e_k)$, $(e'_l)$, $(x_i)$. Par $|ab| \leq (|a|^2 + |b|^2)/2$, on obtient $|B(T, T')| \leq \frac14 \sum_{k,l} s_k t_l (\Lambda^f_{kl} + \Lambda^e_{kl})$.

\emph{Le terme mixte.} Le lemme~\ref{lem:1-lagrange} donne $\Lambda^f_{kl} \leq 2 q_k q'_l$ et $\Lambda^e_{kl} \leq 2 p_k p'_l$, où $q_k$, $q'_l$, $p_k$, $p'_l$ sont formés avec les familles correspondantes. D'où $|B(T, T')| \leq \frac12 \bigl[ (\sum_k s_k q_k)(\sum_l t_l q'_l) + (\sum_k s_k p_k)(\sum_l t_l p'_l) \bigr]$. Comme dans la démonstration du lemme~\ref{lem:1-kyfan}, les poids $p_k$, $q_k$ sont dans $[0,1]$ et de somme $\leq |I| \leq n$, et le lemme~\ref{lem:1-poids} donne $\sum_k s_k p_k \leq \sigma_n^1(T)$, et de même pour les trois autres sommes. Donc $|B(T, T')| \leq \sigma_n^1(T)\,\sigma_n^1(T')$.

\emph{Le terme pur.} Prenons $T' = T$ et $\alpha_{kl} = \Lambda^e_{kl}/2$. La matrice $(\alpha_{kl})$ est symétrique ($M^e_{lk,ij} = -M^e_{kl,ij}$), de diagonale nulle ($M^e_{kk,ij} = 0$) et à coefficients dans $[0, 1]$ par le lemme~\ref{lem:1-lagrange}. Pour ses lignes, on écrit $M^e_{kl,ij} = \langle e_l, z\rangle$ avec $z = \langle e_k, x_i\rangle x_j - \langle e_k, x_j\rangle x_i$ ; le lemme~\ref{lem:1-bessel} appliqué à la famille $(e_l)$ donne $\sum_l |M^e_{kl,ij}|^2 \leq \|z\|^2$, et $\|z\|^2 \leq |\langle e_k, x_i\rangle|^2 + |\langle e_k, x_j\rangle|^2$ si $i \neq j$, tandis que $z = 0$ si $i = j$. En sommant sur $i \neq j$, $\sum_l \alpha_{kl} \leq (|I| - 1)\,p_k$. Le lemme~\ref{lem:1-poids2}, appliqué avec $G = I$ et $\theta = s_{n-1}(T)$ (la suite est décroissante, donc $s_k \geq \theta$ pour $k < n$ et $s_k \leq \theta$ pour $k \geq n$), donne $\sum_{k,l} \alpha_{kl} s_k s_l \leq (\sum_I s_k)^2 - \sum_I s_k^2 = 2\sigma_n^2(T)$. Le même raisonnement vaut pour $\Lambda^f/2$, avec la famille $(f_l)$ dans le lemme~\ref{lem:1-bessel}. Donc $|B(T, T)| \leq \frac12 (2\sigma_n^2(T) + 2\sigma_n^2(T)) = 2\sigma_n^2(T)$.

\emph{Conclusion.} $2\sigma_n^2(w) = |B(w,w)| \leq 2\sigma_n^2(u) + 2\sigma_n^1(u)\sigma_n^1(v) + 2\sigma_n^2(v)$. Avec le premier énoncé, cela donne~(16) pour $m \leq 2$, et le second énoncé donne~(15) pour $n \leq 2$, l'hypothèse portant sur $m \leq n \leq 2$.
\end{proof}

\begin{remarque}
La démonstration suit la voie de la page~71 par $\Lambda^2$ sans construire l'espace hilbertien $\Lambda^2 E$ : le produit scalaire $\langle a \wedge b, c \wedge d\rangle = \langle a, c\rangle\langle b, d\rangle - \langle a, d\rangle\langle b, c\rangle$ y est remplacé par les mineurs $M_{kl,ij}$, et la formule de Cauchy--Binet et l'identité de Lagrange tiennent lieu de structure hilbertienne. Le terme mixte $B(u, v) + B(v, u)$ correspond à $u \wedge v + v \wedge u$, et sa borne $2\,\sigma_n^1(u)\sigma_n^1(v)$ est celle que donne la constante $p!\,q!/(p+q)! = 1/2$ de la page pour $p = q = 1$. Le terme pur $|B(T, T)| \leq 2\sigma_n^2(T)$ est la majoration de la proposition~3 pour $m = 2$, restreinte aux contractions de la forme $\sum_i x_i \langle y_i, \cdot\rangle$ à familles orthogonales. L'inégalité de Ky Fan appliquée à $\Lambda^2 T$ n'y suffirait pas : elle majore par la somme des $\binom n2$ plus grands produits $s_is_j$, qui peut dépasser $\sigma_n^2(T)$ (pour $n = 3$ et $s = (2, 1, 1, 1)$, elle vaut $6$ et $\sigma_3^2 = 5$). La majoration des lignes $\sum_l \alpha_{kl} \leq (|I| - 1)\,p_k$, propre aux vecteurs décomposables, rend possible le lemme~\ref{lem:1-poids2}. L'énoncé vaut tel que la page l'écrit pour $m = 2$, sans hypothèse supplémentaire.
\end{remarque}

\paragraph{Coefficients de Fredholm (pages 123 et 124).} Pour un opérateur $T$, $\alpha_k(T)$ désigne le coefficient de $X^k$ dans $\det(1 + XT)$, c'est-à-dire la trace de $\Lambda^k T$ ; $|A| = (A^*A)^{1/2}$ et $|A^*| = (AA^*)^{1/2}$. La page~123 encadre le corollaire~2, la page~124 le corollaire~3, pour des opérateurs nucléaires (\lot{1}{7}{123}, \lot{1}{7}{124}).

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 123 et 124, corollaires 2 et 3, en dimension finie\piste{1-mixed-schwarz-fredholm-coefficients}]
Soient $A, B$ des matrices carrées complexes. Pour tout $k$,
\[ |\alpha_k(A + B)|^2 \leq \alpha_k(|A| + |B|)\, \alpha_k(|A^*| + |B^*|), \]
et $|\det(1 + A + B)| \leq \frac12 \big[\det(1 + |A| + |B|) + \det(1 + |A^*| + |B^*|)\big]$.
\end{theoreme}
\end{encadre}
L'énoncé tient tel que la page l'écrit (Lean : \href{\leanblob/Folder1.lean}{\texttt{corollaire2}, \texttt{corollaire3}}). La même démonstration donne la forme géométrique, énoncé de l'édition : $|\det(1 + A + B)|^2 \leq \det(1 + |A| + |B|) \det(1 + |A^*| + |B^*|)$.

\begin{remarque}
La démonstration n'est pas le développement multilinéaire de la page. La matrice par blocs $\left(\begin{smallmatrix} |A| & A^* \\ A & |A^*| \end{smallmatrix}\right)$ est $|H| + H$ pour $H = \left(\begin{smallmatrix} 0 & A^* \\ A & 0 \end{smallmatrix}\right)$, donc positive ; on ajoute celles de $A$ et de $B$, on restreint aux mineurs principaux, où le complément de Schur et la croissance du déterminant donnent $|\det T_S|^2 \leq \det P_S \det Q_S$, puis on applique l'inégalité de Cauchy--Schwarz à la somme des mineurs. Le cas des opérateurs nucléaires n'est pas formalisé.
\end{remarque}

\paragraph{La sous-additivité de $S_p$ par le déterminant (pages 126 à 139).} Pour $0 < p < 1$, on note $S_p(u) = \sum_i s_i(u)^p$ la somme des puissances $p$-ièmes des valeurs singulières. Ce n'est pas une norme, et l'inégalité $S_p(u + v) \leq S_p(u) + S_p(v)$ n'a rien d'évident. La page~129 dit ne connaître qu'une méthode analytique pour l'obtenir. Pour un réel $s \geq 0$, $s^p$ s'écrit comme une intégrale de $\log(1 + vs)$ contre la mesure $v^{-1-p}\,dv$ sur $]0, \infty[$ (lemme~1, p.~128). En sommant sur les valeurs singulières, $S_p(u)$ devient l'intégrale de $\log\det(1 + v|u|)$, et l'inégalité de déterminants~(15) passe sous l'intégrale (\lot{1}{7}{129}). Ainsi la page déduit la sous-additivité de~(15), démontrée plus haut pour $n \leq 2$ et, en dimension finie complexe, pour tout $n$ dans le dernier encadré de la section.

\begin{encadre}
\begin{theoreme}[D'après les pages 128 et 129, en dimension finie\piste{1-schatten-p-via-fredholm-determinant}]
Soit $0 < p < 1$ et $K_p = \int_0^\infty \log(1 + t)\, t^{-1-p}\,dt$. Alors $K_p > 0$ et $s^p K_p = \int_0^\infty \log(1 + vs)\, v^{-1-p}\,dv$ pour tout $s \geq 0$. Si des réels positifs vérifient $\prod_{i<n}(1 + r a_i) \leq \prod_{i<n}(1 + r b_i) \prod_{i<n}(1 + r c_i)$ pour tout $r \geq 0$, alors $\sum_{i<n} a_i^p \leq \sum_{i<n} b_i^p + \sum_{i<n} c_i^p$. En particulier $\sum_{i<n} s_i(u+v)^p \leq \sum_{i<n} s_i(u)^p + \sum_{i<n} s_i(v)^p$ dès que~(15) vaut pour cet~$n$, donc pour $n \leq 2$.
\end{theoreme}
\end{encadre}

\noindent La déduction de la page est juste. Lean vérifie la représentation intégrale par changement de variable $t = vs$, sans calculer $K_p$, qui vaut $\pi/(p \sin \pi p)$ ; la sous-additivité de $S_p$ en dimension finie complexe, pour tout $n$, découle du dernier encadré (théorèmes \texttt{integral\_kernel}, \texttt{sum\_rpow\_le\_of\_prod\_le}, \texttt{sum\_singularValues\_rpow\_add\_le}).

Ne sont pas démontrés ici : la borne $p!\,q!/(p+q)!$ de la page~71 sur $\|(\Lambda^p u) \wedge (\Lambda^q v)\|_1$ et la formule~(14) pour des opérateurs à trace ; la seconde forme de la proposition~3, $\sup \alpha_m(|v_n u|)$, et la proposition~3 sur $\mathbb R$ (sur $\mathbb C$ en dimension finie, voir plus bas) ; le passage de la dimension finie aux opérateurs compacts entre espaces de Hilbert ; l'assertion de la page~73 sur l'optimalité du système ; la proposition~4 ; les pages~74 et~75, sur la sous-additivité des fonctions concaves des valeurs singulières ; les corollaires~2 et~3 des pages~123 et~124 pour des opérateurs nucléaires ; l'inégalité de Weyl $\sum |\lambda_i|^p \leq S_p$ par la formule de Jensen et l'inégalité de Hölder des pages~130 à~139.

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 71 à 73, le système (16), en dimension finie\piste{1-sigma-nm-system}]
Soient $E$, $F$ des espaces hilbertiens complexes de dimension finie et $u, v : E \to F$ linéaires. Pour tous entiers $n$ et $m$,
\[
  \sigma_n^m(u+v) \leq \sum_{p=0}^{m} \sigma_n^p(u)\,\sigma_n^{m-p}(v).
\]
Par conséquent, pour tout $n$ et tout $r \geq 0$, $\prod_{i<n}(1 + r s_i(u+v)) \leq \prod_{i<n}(1 + r s_i(u)) \prod_{i<n}(1 + r s_i(v))$, et, pour $0 < p < 1$, $\sum_{i<n} s_i(u+v)^p \leq \sum_{i<n} s_i(u)^p + \sum_{i<n} s_i(v)^p$.
\end{theoreme}
\end{encadre}
L'énoncé tient tel que la page l'écrit, pour tout $m$, en dimension finie (Lean : \href{\leanblob/Folder1.lean}{\texttt{sigma\_system}, \texttt{prod\_one\_add\_singularValues\_add\_le}, \texttt{sum\_singularValues\_rpow\_add\_le}}). Pour $m > n$, le premier membre est nul. La démonstration utilise les coefficients $\alpha_m(M) = \sum_{|K| = m} \det M_K$ du paragraphe précédent, pour des matrices carrées quelconques, et quatre lemmes de matrices.

\begin{lemme}\label{lem:1-matrices}
\begin{enumerate}
\item (Sylvester) Pour $X$ de taille $k \times l$ et $Y$ de taille $l \times k$, $\alpha_m(XY) = \alpha_m(YX)$.
\item Pour des matrices carrées $A$ et $D$, $\alpha_m\bigl(\begin{smallmatrix} A & 0 \\ 0 & D\end{smallmatrix}\bigr) = \sum_{p \leq m} \alpha_p(A)\,\alpha_{m-p}(D)$.
\item (Fischer) Si $M = \bigl(\begin{smallmatrix} A & B \\ B^* & D\end{smallmatrix}\bigr)$ est positive, $\det M \leq \det A \det D$.
\item (Cauchy--Schwarz) Pour $X$ de taille $k \times l$ et $Y$ de taille $l \times k$, $|\det XY|^2 \leq \det(XX^*) \det(Y^*Y)$.
\end{enumerate}
\end{lemme}

\begin{proof}
(1) Par définition, $\alpha_m(M)$ est le coefficient de $X^m$ dans $\det(1 + XM)$, et $\det(1 + X\,XY) = \det(1 + YX\,X)$ (identité de Sylvester, sur l'anneau des polynômes). (2) Le déterminant d'une matrice diagonale par blocs est le produit des déterminants des blocs : $\det(1 + XM)$ est le produit de $\det(1 + XA)$ et de $\det(1 + XD)$, dont on compare les coefficients. (3) Si $\det A = 0$, un vecteur $z \neq 0$ vérifie $Az = 0$ ; la positivité de $M$ donne alors $M(z, 0) = 0$, et $\det M = 0$. Sinon $A$ est définie positive, $\det M = \det A \det(D - B^*A^{-1}B)$ (complément de Schur), et $D - B^*A^{-1}B$, $B^*A^{-1}B$ sont positives ; la croissance du déterminant (démonstration des corollaires~2 et~3) donne $\det(D - B^*A^{-1}B) \leq \det D$. (4) La matrice $\bigl(\begin{smallmatrix} X \\ Y^* \end{smallmatrix}\bigr)\bigl(\begin{smallmatrix} X^* & Y \end{smallmatrix}\bigr) = \bigl(\begin{smallmatrix} XX^* & XY \\ Y^*X^* & Y^*Y \end{smallmatrix}\bigr)$ est positive, et l'inégalité $|\det T|^2 \leq \det P \det Q$ de la démonstration des corollaires~2 et~3 s'applique.
\end{proof}

\begin{lemme}[entrelacement]\label{lem:1-entrelacement}
Soient $s_0 \geq s_1 \geq \cdots \geq 0$, $S = \operatorname{diag}(s_0, \ldots, s_{d-1})$ et $\Psi$ une matrice $d \times d$ telle que $\|\Psi z\|^2 \leq \sum_{j<n} |z_j|^2$ pour tout $z \in \mathbb C^d$. Alors
\[
  \alpha_p(\Psi^* S \Psi) \leq \sum_{\substack{t \subseteq \{0, \ldots, n-1\} \\ |t| = p}} \ \prod_{i \in t} s_i .
\]
\end{lemme}

\begin{proof}
La matrice $N = \Psi^* S \Psi$ est hermitienne positive ; soient $\lambda_0 \geq \cdots \geq \lambda_{d-1} \geq 0$ ses valeurs propres et $(b_l)$ une base orthonormée de vecteurs propres associés. En diagonalisant $N$ par une matrice unitaire $U$, le lemme~\ref{lem:1-matrices}~(1) donne $\alpha_p(N) = \alpha_p(\operatorname{diag}(\lambda))$, c'est-à-dire la fonction symétrique élémentaire de degré $p$ des $\lambda_i$. Celle-ci croît avec chacune de ses variables positives ; il suffit donc de montrer que $\lambda_i \leq s_i$ si $i < n$ et que $\lambda_i = 0$ si $i \geq n$. C'est l'argument de dimension du principe du min-max. Fixons $i$ et imposons à $z \in \mathbb C^d$ les conditions $\langle b_l, z\rangle = 0$ pour $l > i$, et $(\Psi z)_k = 0$ pour $k < i$ si $i < n$, ou $z_k = 0$ pour $k < i$ si $i \geq n$. Cela fait $(d - 1 - i) + i < d$ équations linéaires : il existe $z \neq 0$ qui les vérifie. D'une part, $\langle z, Nz\rangle = \sum_l \lambda_l |\langle b_l, z\rangle|^2$, où seuls les $l \leq i$ comptent et $\lambda_l \geq \lambda_i$, d'où $\langle z, Nz\rangle \geq \lambda_i \|z\|^2$. D'autre part, $\langle z, Nz\rangle = \sum_k s_k |(\Psi z)_k|^2$. Si $i < n$, les termes $k < i$ sont nuls et $s_k \leq s_i$ pour $k \geq i$, d'où $\langle z, Nz\rangle \leq s_i \|\Psi z\|^2 \leq s_i \|z\|^2$. Si $i \geq n$, les $z_j$ d'indice $j < n \leq i$ sont nuls, donc $\Psi z = 0$ par l'hypothèse, et $\langle z, Nz\rangle = 0$. On divise par $\|z\|^2 > 0$.
\end{proof}

\begin{proof}[Démonstration du théorème]
Posons $T = u + v$ ; soient $(e_j, f_j)$ ses vecteurs de Schmidt (conventions du début de la section), et $x_j = e_j$, $y_j = f_j$ pour $j < n$, $x_j = y_j = 0$ pour $n \leq j < d$. Pour $w : E \to F$ linéaire, notons $C_w$ la matrice $d \times d$ de coefficients $\langle y_i, w x_j\rangle$.

\emph{Le premier membre.} Le lemme~\ref{lem:1-schmidt} montre que $C_T$ est diagonale, de coefficients $s_j(T)$ pour $j < n$ et $0$ ensuite. Ses mineurs principaux sont des produits de coefficients diagonaux, et $\sigma_n^m(T) = \alpha_m(C_T)$, les $s_j(T)$ d'indice $j \geq d$ étant nuls.

\emph{Factorisation.} Soient $w \in \{u, v\}$, $(e_k(w), f_k(w))$ ses vecteurs de Schmidt et $S_w = \operatorname{diag}(s_k(w))$. En écrivant $x_j = \sum_k \langle e_k(w), x_j\rangle\, e_k(w)$ et $w\,e_k(w) = s_k(w) f_k(w)$, on obtient $\langle y_i, w x_j\rangle = \sum_k \langle y_i, f_k(w)\rangle\, s_k(w)\, \langle e_k(w), x_j\rangle$, c'est-à-dire
\[
  C_w = (S_w^{1/2} \Phi_w)^* (S_w^{1/2} \Psi_w), \qquad \Phi_w = \bigl(\langle f_k(w), y_j\rangle\bigr)_{k,j}, \quad \Psi_w = \bigl(\langle e_k(w), x_j\rangle\bigr)_{k,j}.
\]
Comme $C_T = C_u + C_v$, on a $C_T = G^* H$, où $H$ (resp.\ $G$) est la matrice $2d \times d$ formée des blocs $S_u^{1/2}\Psi_u$ et $S_v^{1/2}\Psi_v$ (resp.\ $S_u^{1/2}\Phi_u$ et $S_v^{1/2}\Phi_v$) placés l'un sous l'autre.

\emph{Cauchy--Schwarz et Fischer.} Par le lemme~\ref{lem:1-matrices}~(1),
\[ \alpha_m(C_T) = \alpha_m(HG^*) = \sum_K \det(H_K G_K^*), \]
où $K$ parcourt les parties à $m$ éléments des deux copies de $\{0, \ldots, d-1\}$ et $H_K$ désigne les lignes de $H$ d'indices dans $K$. Par~(4), $|\det(H_K G_K^*)|^2 \leq \det(HH^*)_K \det(GG^*)_K$. La matrice $(HH^*)_K$ est positive, et ses lignes se répartissent entre les deux copies ; par~(3), $\det(HH^*)_K \leq \det(P_H)_K$, où $P_H$ est la partie diagonale par blocs de $HH^*$, de blocs $S_u^{1/2}\Psi_u\Psi_u^*S_u^{1/2}$ et $S_v^{1/2}\Psi_v\Psi_v^*S_v^{1/2}$. De même pour $G$. L'inégalité de Cauchy--Schwarz sur la somme en $K$ donne
\[
  \sigma_n^m(T) \leq \alpha_m(P_H)^{1/2}\, \alpha_m(P_G)^{1/2}.
\]

\emph{Entrelacement.} Par~(2), $\alpha_m(P_H) = \sum_p \alpha_p(S_u^{1/2}\Psi_u\Psi_u^*S_u^{1/2})\, \alpha_{m-p}(S_v^{1/2}\Psi_v\Psi_v^*S_v^{1/2})$, et par~(1), $\alpha_p(S_w^{1/2}\Psi_w\Psi_w^*S_w^{1/2}) = \alpha_p(\Psi_w^* S_w \Psi_w)$. Pour $z \in \mathbb C^d$, $(\Psi_w z)_k = \langle e_k(w), \sum_j z_j x_j\rangle$ ; le lemme~\ref{lem:1-bessel} et l'orthogonalité des $x_j$, de normes $\leq 1$ et nuls pour $j \geq n$, donnent $\|\Psi_w z\|^2 \leq \|\sum_j z_j x_j\|^2 \leq \sum_{j<n} |z_j|^2$. Le lemme~\ref{lem:1-entrelacement} donne alors $\alpha_p(\Psi_w^* S_w \Psi_w) \leq \sigma_n^p(w)$. Les $f_k(w)$ et les $y_j$ vérifient les mêmes hypothèses, et le même raisonnement vaut pour $G$. Les deux facteurs sont donc majorés par $\sum_p \sigma_n^p(u)\,\sigma_n^{m-p}(v)$, d'où~(16). La forme produit s'en déduit par l'énoncé \q{du système~(16) à la forme produit~(15)}, et la sous-additivité de $S_p$ par le théorème des pages~128 et~129.
\end{proof}

\begin{remarque}
La page majore $\|(\Lambda^p u) \wedge (\Lambda^q v)\|_1$ par $p!\,q!\,\|\Lambda^p u\|_1\|\Lambda^q v\|_1/(p+q)!$, en déduit la formule encadrée~(14), $\alpha_n(|u+v|) \leq \sum_p \alpha_p(|u|)\,\alpha_{n-p}(|v|)$, puis~(16) par la proposition~3. La démonstration ci-dessus garde le développement de $\Lambda^m(u+v)$, écrit avec des mineurs principaux, mais ne sépare jamais les termes mixtes : la factorisation de $C_T$ à travers $\mathbb C^{2d}$ range $u$ et $v$ dans deux blocs, et c'est l'inégalité de Fischer qui les sépare ; la constante $p!\,q!/(p+q)!$ n'apparaît pas. Le lemme~\ref{lem:1-entrelacement} est la moitié de la proposition~3 qui sert, la majoration de $|\alpha_m|$ d'une compression de $w$ par $\sigma_n^m(w)$, pour des compressions par des familles orthogonales de normes $\leq 1$. Lean écrit $C_w$ (\texttt{compr}), sa factorisation (\texttt{compr\_eq}), $\sigma_n^m(T) \leq \operatorname{Re} \alpha_m(C_T)$ (\texttt{sigma\_le\_alpha\_compr}), les points~(1) à~(4) du lemme~\ref{lem:1-matrices} (\texttt{alpha\_mul\_comm}, \texttt{alpha\_fromBlocks\_zero}, \texttt{det\_fromBlocks\_le} et sa forme \texttt{det\_le\_det\_blockMask}, \texttt{norm\_det\_mul\_sq\_le}), l'étape de Cauchy--Schwarz et Fischer (\texttt{norm\_alpha\_mul\_conjTranspose\_le}) et l'entrelacement (\texttt{eigenvalues}$_0$\texttt{\_le\_of\_conj\_diagonal}, \texttt{alpha\_conj\_diagonal\_le}, avec l'hypothèse de Bessel \texttt{gramMat\_bound}). Les lemmes de matrices sont écrits sur $\mathbb C$ ; le cas réel s'en déduit par complexification (énoncé suivant), et la proposition~3 comme borne supérieure fait l'objet de l'énoncé d'après. Ne sont pas formalisés la formule~(14) pour des opérateurs à trace et le passage aux opérateurs compacts, énoncé plus bas.
\end{remarque}

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 71 à 73, le système (16) sur $\mathbb R$\piste{1-sigma-nm-system}]
Soient $E$, $F$ des espaces euclidiens réels de dimension finie et $u, v : E \to F$ linéaires. Pour tous entiers $n$ et $m$, $\sigma_n^m(u+v) \leq \sum_{p=0}^{m} \sigma_n^p(u)\,\sigma_n^{m-p}(v)$ ; par conséquent la forme produit~(15) vaut pour tout $n$ et tout $r \geq 0$, et $\sum_{i<n} s_i(u+v)^p \leq \sum_{i<n} s_i(u)^p + \sum_{i<n} s_i(v)^p$ pour $0 < p < 1$.
\end{theoreme}
\end{encadre}
L'énoncé tient tel que la page l'écrit (Lean : \href{\leanblob/Folder1.lean}{\texttt{sigma\_system\_real}, \texttt{prod\_one\_add\_singularValues\_add\_le\_real}, \texttt{sum\_singularValues\_rpow\_add\_le\_real}}).
\begin{proof}
On complexifie. Soient $M$ la matrice réelle de $u$ dans des bases orthonormées de $E$ et de $F$, et $u_{\mathbb C} : \mathbb C^{\dim E} \to \mathbb C^{\dim F}$ l'application de matrice $M$ lue sur $\mathbb C$. La matrice de $u^*u$ dans la base orthonormée de $E$ est $M^{\mathsf T} M$, celle de $u_{\mathbb C}^* u_{\mathbb C}$ est $M^* M = M^{\mathsf T} M$ lue sur $\mathbb C$ : les deux opérateurs ont le même polynôme caractéristique, à l'inclusion $\mathbb R \subset \mathbb C$ près. Les valeurs propres d'un opérateur autoadjoint, rangées par ordre décroissant, sont les racines de ce polynôme ainsi rangées ; le polynôme réel est scindé sur $\mathbb R$, et ses racines dans $\mathbb C$ sont les mêmes. Donc $u^*u$ et $u_{\mathbb C}^*u_{\mathbb C}$ ont les mêmes valeurs propres, et $s_i(u_{\mathbb C}) = s_i(u)$ pour tout $i$. Comme $(u+v)_{\mathbb C} = u_{\mathbb C} + v_{\mathbb C}$, le théorème complexe appliqué à $u_{\mathbb C}$ et $v_{\mathbb C}$ donne~(16) ; (15) et la sous-additivité s'en déduisent comme sur $\mathbb C$.
\end{proof}

\begin{encadre}
\begin{theoreme}[Grothendieck, page 72, la proposition~3 en dimension finie\piste{1-sigma-nm-system}]
Soient $E$, $F$ des espaces hilbertiens complexes de dimension finie, $u : E \to F$ linéaire et $m, n$ des entiers. Alors
\[
  \sigma_n^m(u) = \max\bigl\{ |\alpha_m(w u)| : w : F \to E \text{ linéaire},\ \|w\| \leq 1,\ \operatorname{rang} w \leq n \bigr\},
\]
où $\alpha_m(wu)$ est le coefficient de $X^m$ dans $\det(1 + X\,wu)$, calculé dans une base quelconque de $E$.
\end{theoreme}
\end{encadre}
L'énoncé tient tel que la page l'écrit, sous la forme de la première égalité, et la borne supérieure est atteinte (Lean : \href{\leanblob/Folder1.lean}{\texttt{isGreatest\_norm\_alpha\_comp}, \texttt{norm\_alpha\_comp\_le}}). La seconde forme, $\sup_w \alpha_m(|wu|)$, n'est pas formalisée.
\begin{proof}
Le coefficient $\alpha_m$ de la matrice d'un endomorphisme ne dépend pas de la base : un changement de base conjugue la matrice, et le lemme~\ref{lem:1-matrices}~(1) s'applique. \emph{Majoration.} Soit $w$ comme dans l'énoncé, et $w^* : E \to F$ son adjoint, contraction de même rang. Soient $(e_i, f_i)$ les vecteurs de Schmidt de $w^*$ et $t_i = s_i(w^*)$ ; alors $t_i \leq 1$, $t_i = 0$ pour $i \geq n$, et $w^* e_i = t_i f_i$. Dans la base $(e_i)$, la matrice de $wu$ a pour coefficients $\langle e_i, wu\,e_j\rangle = \langle w^* e_i, u e_j\rangle = t_i \langle f_i, u e_j\rangle$ ; elle s'écrit $DN$ avec $D = \operatorname{diag}(\sqrt{t_i})$ et $N_{ij} = \sqrt{t_i}\langle f_i, u e_j\rangle$, et $\alpha_m(DN) = \alpha_m(ND)$, où $(ND)_{ij} = \langle y_i, u x_j\rangle$ pour $x_j = \sqrt{t_j}\, e_j$ et $y_i = \sqrt{t_i}\, f_i$. Ces deux familles sont orthogonales, de normes $\leq 1$ et nulles à partir de l'indice $n$. Comme dans la démonstration du théorème complexe, la compression $(\langle y_i, u x_j\rangle)$ se factorise en $(S_u^{1/2}\Phi)^*(S_u^{1/2}\Psi)$ ; l'inégalité de Cauchy--Schwarz sur les mineurs (lemme~\ref{lem:1-matrices}~(4), sommée sur les parties $K$) et le lemme~\ref{lem:1-entrelacement} appliqué à chaque facteur donnent $|\alpha_m(ND)| \leq \sigma_n^m(u)^{1/2}\,\sigma_n^m(u)^{1/2}$. \emph{Égalité.} Soient $(e_j, f_j)$ les vecteurs de Schmidt de $u$ et $w_0 = \sum_{j<n} e_j \langle f_j, \cdot\rangle$ ; c'est une contraction par l'inégalité de Bessel, de rang $\leq n$, et la matrice de $w_0 u$ dans la base $(e_j)$ est la compression $C_u$, diagonale de coefficients $s_j(u)$ pour $j < n$ ; donc $\alpha_m(w_0 u) = \sigma_n^m(u)$.
\end{proof}

\begin{enonce}[Pages 71 et 72, opérateurs compacts\piste{1-sigma-nm-system}]\nonverifie
Soient $u, v$ des opérateurs compacts entre espaces de Hilbert. Pour $0 \leq m \leq n$, $\sigma_n^m(u+v) \leq \sum_{p=0}^{m} \sigma_n^p(u)\,\sigma_n^{m-p}(v)$, coefficient par coefficient ; ce système entraîne $\prod_{i \leq n}(1 + r s_i(u+v)) \leq \prod_{i \leq n}(1 + r s_i(u)) \prod_{i \leq n}(1 + r s_i(v))$ pour tout $r \geq 0$.
\end{enonce}
\begin{demopage}[pages 71 et 72]
La page majore $\|(\Lambda^p u) \wedge (\Lambda^q v)\|_1$ par
\[
  \frac{p!\,q!}{(p+q)!}\,\|\Lambda^p u\|_1\,\|\Lambda^q v\|_1
\]
et, en développant $\Lambda^n(u+v)$, obtient la formule encadrée~(14),
\[
  \alpha_n(|u+v|) \leq \sum_p \alpha_p(|u|)\,\alpha_{n-p}(|v|)
\]
(p.~71). La proposition~3 écrit $\sigma_n^m(u)$ comme borne supérieure de $|\alpha_m(wu)|$ sur les $w$ de norme $\leq 1$ et de rang $\leq n$ (p.~72). La formule~(14) appliquée à $wu + wv$, puis la proposition~3, donnent~(16), forme précise de~(15). La prose de la page~72 est en grande partie illisible, et la page~71 porte en marge \q{à réviser}. En dimension finie complexe, l'énoncé est le théorème précédent ; pour des opérateurs compacts, il s'en déduirait en approchant $u$ et $v$ par des opérateurs de rang fini, ce que Lean ne fait pas.
\end{demopage}
\section[Cote 113 : l'enveloppe de Karoubi et l'invariance de Morita]{Cote 113 : l'enveloppe de Karoubi et l'invariance de Morita\protect\verifie{Folder113}}\label{sec:113}

La cote 113, \emph{Abelianization : notes manuscrites (s.d.)}, douze pages que l'inventaire date \q{[à partir de 1982]}, construit sous le titre \q{$\otimes$ dans Cat} le produit tensoriel de petites catégories $k$-linéaires, et montre qu'il calcule celui de leurs catégories de modules. Sur la page~3, pour $P$ petite catégorie $k$-additive, $P^k$ est \emph{défini} comme $\operatorname{Hom}_{\mathbf Z}(P^\circ, Ab)$, identifié à $\operatorname{Hom}_k(P^\circ, Ab_k)$ avec la parenthèse \q{ne dépend pas du choix de la str.\ $k$-additive}. Le plongement $P \hookrightarrow P^k$ est une \q{inclusion additive pl.\ fid.}, d'où \q{$\operatorname{Kar} P \approx \mathrm{Ul}\operatorname{Proj}(P^{k})$}, les deux lettres devant \q{Proj} n'étant pas identifiées. Une note en marge ajoute \q{$P \to \operatorname{Kar} P$ induit $(\operatorname{Kar} P)^{k} \overset{\sim}{\to} P^{k}$} (\lot{113}{1}{3}). La lecture modernisée comprend la première équivalence comme $\operatorname{Kar}(P) \simeq \operatorname{Proj}_{\mathrm{tf}}(P^k)$, les projectifs de type fini, et nomme l'ensemble invariance de Morita.

\begin{definition}
Soit $P$ une catégorie. Son \emph{enveloppe de Karoubi} $\operatorname{Kar} P$ a pour objets les couples $(X, e)$ formés d'un objet $X$ de $P$ et d'un idempotent $e = e^2$ de $\operatorname{End}(X)$, et pour flèches $(X, e) \to (Y, e')$ les $f : X \to Y$ tels que $e' f = f = f e$ ; la composition est celle de $P$, et l'identité de $(X, e)$ est $e$. Le foncteur $\iota : P \to \operatorname{Kar} P$ envoie $X$ sur $(X, \mathrm{id}_X)$. Une catégorie est \emph{karoubienne} si tout idempotent s'y scinde. Si $P$ est préadditive, $\operatorname{Kar} P$ l'est aussi, ses groupes de flèches étant des sous-groupes de ceux de $P$.
\end{definition}

\begin{enonce}[Page 3, la note marginale]
Soient $P$ une catégorie préadditive et $\mathcal D$ une catégorie préadditive karoubienne, par exemple $Ab$ ou la catégorie des $k$-modules. La restriction le long de $\iota^\circ : P^\circ \to (\operatorname{Kar} P)^\circ$ est une équivalence de la catégorie des foncteurs additifs $(\operatorname{Kar} P)^\circ \to \mathcal D$ sur celle des foncteurs additifs $P^\circ \to \mathcal D$. Pour $\mathcal D = Ab$, c'est l'équivalence $(\operatorname{Kar} P)^k \simeq P^k$, avec la définition $P^k = \operatorname{Hom}_{\mathbf Z}(P^\circ, Ab)$ de la page.
\end{enonce}

\begin{lemme}\label{lem:113-univ}
Soient $P$ une catégorie et $\mathcal D$ une catégorie karoubienne. La restriction le long de $\iota : P \to \operatorname{Kar} P$ est une équivalence de la catégorie des foncteurs $\operatorname{Kar} P \to \mathcal D$ sur celle des foncteurs $P \to \mathcal D$.
\end{lemme}

\begin{proof}
C'est la propriété universelle classique de l'enveloppe de Karoubi, complétion libre par les rétractes : un foncteur $G : P \to \mathcal D$ se prolonge en envoyant $(X, e)$ sur l'objet par lequel se scinde l'idempotent $G(e)$, et ce prolongement est unique à isomorphisme unique près. On ne la redémontre pas ici.
\end{proof}

\[
\begin{tikzcd}
P \arrow[r, "\iota"] \arrow[rd, "G"'] & \operatorname{Kar} P \arrow[d, dashed, "\overline G"] \\
& \mathcal D
\end{tikzcd}
\qquad \overline G \circ \iota \simeq G,\quad \overline G(X, e) = \text{l'objet par lequel se scinde } G(e).
\]

\begin{lemme}\label{lem:113-op}
Il existe un isomorphisme de catégories $\operatorname{Kar}(P^\circ) \to (\operatorname{Kar} P)^\circ$, bijectif sur les objets, qui fait commuter les plongements : le composé $P^\circ \xrightarrow{\iota_{P^\circ}} \operatorname{Kar}(P^\circ) \to (\operatorname{Kar} P)^\circ$ est $\iota_P^\circ$.
\end{lemme}

\begin{proof}
Un objet de $\operatorname{Kar}(P^\circ)$ est un couple $(X, e)$ où $e$ est un idempotent de $\operatorname{End}_{P^\circ}(X) = \operatorname{End}_P(X)$ ; on l'envoie sur l'objet $(X, e)$ de $(\operatorname{Kar} P)^\circ$. Une flèche $(X, e) \to (Y, e')$ de $\operatorname{Kar}(P^\circ)$ est une flèche $f : Y \to X$ de $P$ telle que $f e' = f = e f$, c'est-à-dire exactement une flèche $(Y, e') \to (X, e)$ de $\operatorname{Kar} P$, ou encore une flèche $(X, e) \to (Y, e')$ de $(\operatorname{Kar} P)^\circ$ ; on l'envoie sur elle-même. Ce foncteur respecte identités et compositions, il est bijectif sur les objets et sur chaque ensemble de flèches. Sur $X \in P$, les deux composés donnent $(X, \mathrm{id}_X)$, et sur les flèches l'identité.
\end{proof}

\begin{lemme}\label{lem:113-restr}
Pour $\mathcal D$ karoubienne, la restriction le long de $\iota_P^\circ : P^\circ \to (\operatorname{Kar} P)^\circ$ est une équivalence de la catégorie des foncteurs $(\operatorname{Kar} P)^\circ \to \mathcal D$ sur celle des foncteurs $P^\circ \to \mathcal D$.
\end{lemme}

\begin{proof}
Par le lemme~\ref{lem:113-op}, cette restriction est la composée de la restriction le long de l'isomorphisme $\operatorname{Kar}(P^\circ) \to (\operatorname{Kar} P)^\circ$, qui est une équivalence, et de la restriction le long de $\iota_{P^\circ}$, qui en est une par le lemme~\ref{lem:113-univ} appliqué à $P^\circ$.
\end{proof}

\begin{lemme}\label{lem:113-decomp}
Toute flèche $f : (X, e) \to (Y, e')$ de $\operatorname{Kar} P$ s'écrit $f = p' \circ \iota(f) \circ j$, où $j : (X, e) \to (X, \mathrm{id})$ et $p' : (Y, \mathrm{id}) \to (Y, e')$ sont les flèches données par $e$ et par $e'$.
\end{lemme}

\general{KaroubiAdditiveFunctors}

\begin{lemme}\label{lem:113-add}
Soient $P$ et $\mathcal D$ préadditives et $F : (\operatorname{Kar} P)^\circ \to \mathcal D$ un foncteur. Si $F \circ \iota^\circ$ est additif, $F$ l'est.
\end{lemme}

\begin{proof}
Par le lemme~\ref{lem:113-decomp}, pour toute flèche $h : (X, e) \to (Y, e')$ de $\operatorname{Kar} P$, on a $F(h) = F(j) \circ (F \circ \iota^\circ)(h) \circ F(p')$, les flèches $j$ et $p'$ ne dépendant que de la source et du but de $h$, et $h$ étant regardée à droite comme une flèche $Y \to X$ de $P^\circ$. Pour deux flèches $h_1, h_2$ de même source et de même but, la somme dans $\operatorname{Kar} P$ est la somme dans $P$ ; l'additivité de $F \circ \iota^\circ$ et la bilinéarité de la composition dans $\mathcal D$ donnent alors $F(h_1 + h_2) = F(h_1) + F(h_2)$.
\end{proof}

\begin{proof}[Démonstration de l'énoncé]
Les foncteurs additifs forment une sous-catégorie pleine de celle de tous les foncteurs. La restriction le long de $\iota^\circ$ étant pleinement fidèle sur tous les foncteurs par le lemme~\ref{lem:113-restr}, elle l'est sur les foncteurs additifs, et elle envoie un foncteur additif sur un foncteur additif. Elle est essentiellement surjective : soit $G : P^\circ \to \mathcal D$ additif ; par le lemme~\ref{lem:113-restr}, il existe $F : (\operatorname{Kar} P)^\circ \to \mathcal D$ et un isomorphisme $F \circ \iota^\circ \simeq G$ ; un foncteur isomorphe à un foncteur additif est additif, donc $F \circ \iota^\circ$ l'est, et $F$ est additif par le lemme~\ref{lem:113-add}. Les catégories $Ab$ et des $k$-modules sont préadditives et karoubiennes, tout idempotent y ayant une image.
\end{proof}

\begin{remarque}
L'énoncé ne demande ni que $P$ soit petite, ni que le but soit abélien. Il suffit que $P$ soit préadditive et $\mathcal D$ préadditive et karoubienne ; l'énoncé vaut en particulier pour les foncteurs additifs à valeurs dans les $k$-modules.
\end{remarque}

\begin{remarque}
L'enveloppe porte le nom de Karoubi, qui l'emploie en K-théorie en 1968 \cite{karoubi1968}. L'énoncé est l'invariance de la catégorie des modules par passage à cette enveloppe, déduite de sa propriété universelle. Le nom d'invariance de Morita renvoie à la caractérisation par Morita, en 1958, des anneaux dont les catégories de modules sont équivalentes \cite{morita1958}.
\end{remarque}

Ne sont pas démontrés ici : la forme $k$-linéaire de l'invariance de Morita ; l'indépendance de la structure $k$-additive ; l'équivalence $\mathrm{Kar}\,P \simeq \mathrm{Proj}_{\mathrm{tf}}(P^k)$ ; le théorème de Freyd--Mitchell ; l'énoncé 2-fonctoriel ; les pages~5 à~12 (produit tensoriel, contre-exemple~($\circledast$), produit dérivé).