Pour tout entier $p\geq 0$ et tout nombre réel $\eta>0$, Demailly définit dans [26], Lemme 5.18, une fonction $M_{\eta}\colon\mathbf{R}^{p}\rightarrow\mathbf{R}$ vérifiant les propriétés suivantes :

1. 1.

   La fonction $M_{\eta}$ est lisse, convexe et croissante en chaque variable ;

2. 2.

   Pour tout $(t_{1},\dots,t_{p})\in\mathbf{R}^{p}$,

   $$\max(t_{1},\dots,t_{p})\leq M_{\eta}(t_{1},\dots,t_{p})\leq\max(t_{1},\dots,t_{p})+\eta;$$

3. 3.

   Si $t_{j}+\eta\leq\max_{i\neq j}(t_{i}-\eta)$, on a

   $$M_{\eta}(t_{1},\dots,t_{p})=M_{\eta}(t_{1},\dots,\widehat{t_{j}},\dots,t_{p})\ ;$$

4. 4.

   Pour tout $t\in\mathbf{R}$,

   $$M_{\eta}(t_{1}+t,\dots,t_{p}+t)=M_{\eta}(t_{1},\dots,t_{p})+t.$$

Il résulte de la continuité de la fonction $M_{\eta}$ et de la propriété d) que l’on définit une métrique continue $\mathopen{\|}{\cdot}\mathclose{\|}_{\eta}$ sur $\mathscr{O}(1)$ en posant

$$\log\mathopen{\|}{s_{P}}\mathclose{\|}_{\eta}^{-1}([x_{0}:\dots:x_{n}])=-\log\mathopen{|}{P(x_{0},\dots,x_{n})}\mathclose{|}+M_{\eta}(\log\mathopen{|}{x_{0}}\mathclose{|},\dots,\log\mathopen{|}{x_{n}}\mathclose{|})$$

pour tout polynôme $P$ homogène de degré $1$. En outre, la propriété b) ci-dessus entraîne que

$$\log\mathopen{\|}{s_{P}}\mathclose{\|}_{\eta}^{-1}-\log\mathopen{\|}{s_{P}}\mathclose{\|}^{-1}=M_{\eta}(\log\mathopen{|}{x_{0}}\mathclose{|},\dots,\log\mathopen{|}{x_{n}}\mathclose{|})-\max(\log\mathopen{|}{x_{0}}\mathclose{|},\dots,\log\mathopen{|}{x_{n}}\mathclose{|}$$

appartient à l’intervalle $[0,\eta]$. Par suite, la métrique $\mathopen{\|}{\cdot}\mathclose{\|}_{\eta}$ converge uniformément vers $\mathopen{\|}{\cdot}\mathclose{\|}$ lorsque $\eta\rightarrow 0$. Il reste à démontrer que la métrique $\mathopen{\|}{\cdot}\mathclose{\|}_{\eta}$ est lisse et psh.

Soit $x=[x_{0}:\dots:x_{n}]$ un point de $\mathbf{P}^{n}$ ; supposons pour fixer les idées que $x_{0},\dots,x_{p}\neq 0$ mais $x_{p+1}=\dots=x_{n}=0$. Prenons pour $P$ le polynôme $X_{0}$. Les fonctions rationnelles $f_{1}=x_{1}/x_{0},\dots,f_{p}=x_{p}/x_{0}$ sont inversibles au voisinage de $x$ ; dans ce voisinage,

	$\displaystyle\log\mathopen{\|}{s_{P}}\mathclose{\|}_{\eta}^{-1}(x)$	$\displaystyle=-\log\mathopen{|}{x_{0}}\mathclose{|}+M_{\eta}(\log\mathopen{|}{x_{0}}\mathclose{|},\dots,\log\mathopen{|}{x_{n}}\mathclose{|})$
		$\displaystyle=M_{\eta}(0,\log\mathopen{|}{f_{1}(x)}\mathclose{|},\dots,\log\mathopen{|}{f_{p}(x)}\mathclose{|})$

si $U$ est pris assez petit pour que l’on ait

$$\sup_{U}\sup_{j>p}\log\mathopen{|}{x_{j}/x_{0}}\mathclose{|}+\eta\leq\inf_{U}\max_{i\leq p}\log\mathopen{|}{x_{i}/x_{0}}\mathclose{|}-\eta.$$

Comme $M_{\eta}$ est lisse et convexe sur $\mathbf{R}^{p+1}$, cette formule prouve que la métrique $\mathopen{\|}{\cdot}\mathclose{\|}_{\eta}$ est lisse et psh sur $U$, d’où l’assertion. ∎

Par hypothèse, il existe un entier $d\geq 1$ et un morphisme $p\colon X\rightarrow\mathbf{P}^{n}_{k}$ tel que $p^{*}\mathscr{O}(1)$ soit isomorphe à $L^{\otimes d}$. L’image réciproque d’une métrique lisse psh sur $\mathscr{O}(1)$ induit une métrique lisse psh sur $L^{\otimes d}$, et donc aussi sur $L$. ∎

Par hypothèse, il existe un entier $d\geq 1$ et un morphisme $p\colon\mathfrak{X}\rightarrow\mathbf{P}^{N}_{k^{0}}$ tel que $p^{*}\mathscr{O}(1)$ soit isomorphe à $\mathfrak{L}^{\otimes d}$. Cela prouve que la métrique sur $L^{\otimes d}$ déduite de la métrique formelle de $L$ est l’image réciproque par $p$ de la métrique de Weil sur $\mathscr{O}(1)$. Le lemme en résulte. ∎

Soit $(\mathfrak{X},\mathfrak{L})$ un modèle formel de $(X,L)$ induisant la métrique formelle donnée de $\bar{L}$. Comme $X$ possède un modèle formel qui est projectif, on peut supposer que $\mathfrak{X}$ est projectif sur $k^{0}$. Il résulte alors du théorème de comparaison géométrie algébrique/géométrie formelle (théorème 2.13.8 de [1]) que $\mathfrak{L}$ est un fibré en droites algébrique sur $\mathfrak{X}$. Dans ces conditions, il existe deux fibrés en droites amples $\mathfrak{L}_{1}$ et $\mathfrak{L}_{2}$ sur $\mathfrak{X}$ tels que $\mathfrak{L}\simeq\mathfrak{L}_{1}\otimes\mathfrak{L}_{2}^{-1}$. Pour $i\in\{1,2\}$, soit $\bar{L}_{i}$ la fibre générique de $\mathfrak{L}_{i}$, muni de sa métrique formelle canonique  ; c’est une métrique psh-approchable. L’isomorphisme $\mathfrak{L}\simeq\mathfrak{L}_{1}\otimes\mathfrak{L}_{2}^{-1}$ induit un isomorphisme $L\simeq L_{1}\otimes L_{2}^{-1}$. C’est même une isométrie, d’où le corollaire. ∎