diff --git a/Inst_eddies/Documentation_texfol/Graphiques/.gitignore b/Inst_eddies/Documentation_texfol/Graphiques/.gitignore
index f81ca1b4b6b2a57c110e4497a2a7e9afdd41ed27..eafb36aebb48d45399fe62cf1951a9ad4ab31d28 100644
--- a/Inst_eddies/Documentation_texfol/Graphiques/.gitignore
+++ b/Inst_eddies/Documentation_texfol/Graphiques/.gitignore
@@ -12,3 +12,4 @@ user_proc.pdf
user_sys.pdf
slice.pdf
nearby_extr.pdf
+descending.pdf
diff --git a/Inst_eddies/Documentation_texfol/Graphiques/GNUmakefile b/Inst_eddies/Documentation_texfol/Graphiques/GNUmakefile
index 0ff27522ba5aadd8230a28a1f06fd865539ac9b7..ec27166bc2c94cdebe6505a21cd1ea7ad7168f2b 100644
--- a/Inst_eddies/Documentation_texfol/Graphiques/GNUmakefile
+++ b/Inst_eddies/Documentation_texfol/Graphiques/GNUmakefile
@@ -1,5 +1,5 @@
objects = degeneracy.pdf periodicity.pdf copy.pdf set_all_outerm.pdf \
-SHPC.pdf plot_test_output.pdf slice.pdf nearby_extr
+SHPC.pdf plot_test_output.pdf slice.pdf nearby_extr.pdf descending.pdf
%.pdf: %.odg
unoconv --doctype=graphics $<
diff --git a/Inst_eddies/Documentation_texfol/Graphiques/descending.odg b/Inst_eddies/Documentation_texfol/Graphiques/descending.odg
new file mode 100644
index 0000000000000000000000000000000000000000..85cee50fb487ef2dbb05e916ee23ab94f343d645
Binary files /dev/null and b/Inst_eddies/Documentation_texfol/Graphiques/descending.odg differ
diff --git a/Inst_eddies/Documentation_texfol/documentation.tex b/Inst_eddies/Documentation_texfol/documentation.tex
index 51fe0c1196bfe7f7c2e88ac4a11ddcfeb0bf4953..55d89fadfc8f68e450516c1596689c4dc3aec150 100644
--- a/Inst_eddies/Documentation_texfol/documentation.tex
+++ b/Inst_eddies/Documentation_texfol/documentation.tex
@@ -965,6 +965,200 @@ des contours au cours de la boucle. En effet, les bons contours
trouvés sont de plus en plus grands, et on cherche toujours un contour
plus grand.
+\subsubsection{Décroissance des intervalles de SSH}
+
+Montrons que, Ã la sortie de \verb+get_1_outerm+, le tableau :
+\begin{verbatim}
+abs(ediff1d(cont_list(:n_cont)%ssh))
+\end{verbatim}
+est nécessairement décroissant. C'est trivial si \verb+n_cont+ à la
+sortie $\le 2$. Montrons-le si \verb+n_cont+ Ã la sortie $\ge 3$. On
+suppose donc qu'on est passé dans la boucle sur \verb+level_good+,
+\verb+level_bad+ et \verb+level_try+. Pour cette démonstration, notons
+:
+\begin{itemize}
+\item $j \in \{1, \dots, j_\mathrm{max}\}$ l'indice de l'itération
+ dans la boucle (pas de variable correspondante dans le programme) ;
+\item $g_j$ la valeur de \verb+level_good+ à l'entrée de l'itération
+ $j$ ;
+\item $b_j$ la valeur de \verb+level_bad+ à l'entrée de l'itération
+ $j$ ;
+\item $t_j$ la valeur de \verb+level_try+ à la fin de l'itération $j$ ;
+\item $s_k$ une valeur de \verb+cont_list(:n_cont)%ssh+ ;
+\item $n$ pour \verb+n_cont+.
+\end{itemize}
+Noter que $j$ est a priori différent de $n$.
+
+Mathématiquement, le problème se pose de la façon
+suivante.
+
+On se donne deux suites de réels $(g_j)$ et $(b_j)$ pour
+$1 \le j \le j_\mathrm{max}$ et on définit une troisième suite de
+réels $(t_j)$ pour $1 \le j \le j_\mathrm{max}$ par :
+\begin{equation*}
+ t_j := \frac{g_j + b_j}{2}
+\end{equation*}
+Nous supposons que :
+\begin{equation}
+ \label{eq:t_j}
+ \forall j \in \{1, \dots, j_\mathrm{max} - 1\},
+ (g_{j + 1} = t_j \land b_{j + 1} = b_j)
+ \lor (g_{j + 1} = g_j \land b_{j + 1} = t_j)
+\end{equation}
+Alors :
+\begin{equation*}
+ \forall j \in \{1, \dots, j_\mathrm{max} - 1\},
+ g_{j + 1} - b_{j + 1} = \frac{g_j - b_j}{2}
+\end{equation*}
+Supposons dans la suite qu'on a un cyclone, c'est-Ã -dire que
+\begin{equation}
+ \label{eq:cyclone}
+ g_1 < b_1
+\end{equation}
+On pourrait faire une démonstration analogue dans le cas
+d'un anticyclone. \`A partir de l'hypothèse \ref{eq:cyclone}, on
+montre facilement par récurrence :
+\begin{equation*}
+ \forall j, g_j < t_j < b_j
+\end{equation*}
+et la suite $(g_j)$ est croissante, la suite $(b_j)$ est
+décroissante. D'où aussi :
+\begin{equation*}
+ \max g_j = g_{j_\mathrm{max}} < b_{j_\mathrm{max}} = \min b_j
+\end{equation*}
+
+Remarquons que :
+\begin{equation*}
+ \left(t_{j + 1} = \frac{t_j + b_j}{2} > t_j \right)
+ \lor \left(t_{j + 1} = \frac{g_j + t_j}{2} < t_j \right)
+\end{equation*}
+donc la suite $(t_j)$ n'est a priori pas monotone.
+
+Soit $j \in \{1, \dots, j_\mathrm{max} - 1\}$.
+
+Si $g_{j + 1} = t_j$ alors :
+\begin{equation*}
+ \forall l \ge 1, t_{j + l} > g_{j + l} \ge g_{j + 1} = t_j
+\end{equation*}
+On peut aussi noter en passant la propriété qui nous sera utile :
+\begin{equation}
+ \label{eq:tjl}
+ \forall l \ge 1, t_{j + l} < b_{j + l} \le b_{j + 1} = b_j
+\end{equation}
+
+Si au contraire $b_{j + 1} = t_j$ alors :
+\begin{equation*}
+ \forall l \ge 1, t_{j + l} < b_{j + l} \le b_{j + 1} = t_j
+\end{equation*}
+Donc, dans les deux cas :
+\begin{equation*}
+ \forall j \in \{1, \dots, j_\mathrm{max} - 1\}, \forall l \ge 1,
+ t_{j + l} \ne t_j
+\end{equation*}
+Ou encore :
+\begin{equation}
+ \label{eq:injection}
+ \forall (j, j') \in \{1, \dots, j_\mathrm{max}\}^2,
+ j \ne j' \Rightarrow t_j \ne t_{j'}
+\end{equation}
+
+On se donne une quatrième suite de réels $(s_k)_{2 \le k \le n}$. On
+suppose :
+\begin{equation*}
+ \forall k, \exists j \in \{1, \dots, j_\mathrm{max} - 1\},
+ s_k = t_j = g_{j + 1}
+\end{equation*}
+(On ne peut pas supposer plus puisque dans l'algorithme, on
+n'enregistre pas forcément une nouvelle valeur de SSH à chaque fois qu'on
+trouve une valeur différente de \verb+level_good+.) D'après la
+propriété \ref{eq:injection}, $j$ est unique :
+\begin{equation*}
+ \forall k, \exists ! j \in \{1, \dots, j_\mathrm{max} - 1\},
+ s_k = t_j = g_{j + 1}
+\end{equation*}
+Notons-le $J(k)$.
+\begin{equation*}
+ \forall k, s_k = t_{J(k)} = g_{J(k) + 1}
+\end{equation*}
+Hypothèse : $J(k)$ est strictement croissant. (Les valeurs de SSH sont
+enregistrées dans l'ordre des itérations, au plus une valeur de SSH
+par itération.) Donc, avec la croissance de $(g_j)$, la suite $(s_k)$
+est croissante.
+
+Montrons que $(s_k)$ est même strictement croissante.
+\begin{equation*}
+ s_{k + 1} = t_{J(k + 1)} = g_{J(k + 1) + 1}
+\end{equation*}
+Donc (hypothèse \ref{eq:t_j}) :
+\begin{equation*}
+ g_{J(k + 1) + 1} > g_{J(k + 1)}
+\end{equation*}
+Donc :
+\begin{equation*}
+ \forall j \le J(k + 1), g_{J(k + 1) + 1} > g_{j}
+\end{equation*}
+Or :
+\begin{align}
+ & J(k) < J(k + 1)
+ \notag \\
+ \Rightarrow & J(k) + 1 \le J(k + 1)
+ \label{eq:J_k1}
+\end{align}
+D'où :
+\begin{equation*}
+ g_{J(k + 1) + 1} > g_{J(k) + 1}
+\end{equation*}
+C'est-Ã -dire :
+\begin{equation*}
+ s_{k + 1} > s_k
+\end{equation*}
+$\Box$
+
+Montrons enfin la décroissance de la suite $(s_{k + 1} -
+s_k)$. Cf. figure \ref{fig:descending}.
+\begin{figure}[htbp]
+ \centering
+ \includegraphics{descending}
+ \caption{get\_1\_outerm. Décroissance de la suite
+ $(s_{k + 1} - s_k)$.}
+ \label{fig:descending}
+\end{figure}
+Avec l'inégalité \ref{eq:J_k1} :
+\begin{equation*}
+ g_{J(k + 1)} \ge g_{J(k) + 1} = s_k
+\end{equation*}
+Avec la propriété \ref{eq:tjl} :
+\begin{equation*}
+ \forall j > J(k + 1), t_j < b_{J(k + 1)}
+\end{equation*}
+D'où, pour tout $j > J(k + 1)$ :
+\begin{equation*}
+ t_j - t_{J(k + 1)} < b_{J(k + 1)} - t_{J(k + 1)}
+ = t_{J(k + 1)} - g_{J(k + 1)}
+\end{equation*}
+et :
+\begin{equation*}
+ t_{J(k + 1)} - g_{J(k + 1)} \le t_{J(k + 1)} - s_k
+ = s_{k + 1} - s_k
+\end{equation*}
+Ainsi :
+\begin{equation*}
+ \forall j > J(k + 1), t_j - s_{k + 1} < s_{k + 1} - s_k
+\end{equation*}
+Or :
+\begin{equation*}
+ s_{k + 2} = t_{J(k + 2)}
+\end{equation*}
+et :
+\begin{equation*}
+ J(k + 2) > J(k + 1)
+\end{equation*}
+donc :
+\begin{equation*}
+ s_{k + 2} - s_{k + 1} < s_{k + 1} - s_k
+\end{equation*}
+$\Box$
+
\subsection{good\_contour}
Trouve, si elle existe, une ligne de niveau à un niveau donné,
diff --git a/Inst_eddies/get_1_outerm.f90 b/Inst_eddies/get_1_outerm.f90
index b353610a8ee7b7849efd3ad29d924806b075e0f9..597d08cc7bbb2d56e01638ac74412b33c3f9716d 100644
--- a/Inst_eddies/get_1_outerm.f90
+++ b/Inst_eddies/get_1_outerm.f90
@@ -24,7 +24,9 @@ contains
! including the outermost contour, are in monotonic order of ssh:
! ascending if the extremum is a minimum, descending if the
! extremum is a maximum. The area is only computed for the
- ! outermost contour.
+ ! outermost contour. On return, the array
+ ! abs(ediff1d(cont_list(:n_cont)%ssh)) is in descending
+ ! order. (See notes for a proof.)
! Method: dichotomy on level of ssh.