\documentclass[11pt]{amsart}
\usepackage[theo]{kbexo}
\def\d{\delta}
\def\e{\varepsilon}
\def\a{\alpha}
\def\b{\beta}
\def\o{\omega}
\def\g{\gamma}
\def\s{\sigma}
\begin{document}
\agregtitle{Preuves en géométrie par le calcul formel}

\section{Introduction}

Les théorèmes classiques de géométrie, connus et démontrés depuis bien
longtemps, peuvent maintenant être démontrés en un instant par le calcul
formel. Il suffit en effet de définir quelques procédures de bases, pour
calculer des chose comme l'équation d'une droite passant par deux points, ou
tangente à un cercle, une conique en un point, l'intersection de deux
droites, etc.~: toutes ces notions qui interviennent dans les constructions
géométriques. Ensuite, on peut aussi définir d'autres procédures qui
permettent de vérifier les faits qui interviennent souvent dans les
théorèmes~: la concourance de trois droites, l'alignement de trois points,
l'orthogonalité, le fait qu'un triangle soit rectangle, isocèle, équilatéral,
etc. 

Il ne reste alors qu'à suivre l'énoncé du théorème choisi, après avoir choisi
un repère, construisant les objets selon les hypothèses imposées, puis à
vérifier que la conclusion est bien vérifiée. Nous proposons ici d'illustrer
ce fait par des exemples. Bien sûr, d'autres exemples que ceux-ci peuvent
être choisis.

\medskip

On peut également se servir du calcul formel comme aide à la démonstration de
certains théorèmes. Nous proposons ici un exemple où le calcul sur machine de
résultants donne une solution au problème posé. Le logiciel peut bien sûr
aussi illuster ces théorèmes par des figures.

\bigskip

%En fait, on pourrait aller plus loin, et faire un programme
%produisant, à partir par exemple un triangle, des droites,
%des points, de différents manières, et cherchant à
%chaque étape si dans la construction des propriétés
%remarquables apparaissent. Alors, la machine ne se contenterait
%pas de démontrer des théorèmes dont l'énoncé lui
%aurait été donné~: elle énoncerait et dé\-mon\-tre\-rait
%ses propres théorèmes.

\section{Le théorème de Morley}


\begin{theo}\label{morley}
Soit $ABC$ un triangle, et soient $3a$, $3b$ et $3c$ les angles
en $A$, $B$ et $C$ de ce triangle. Soient $P$ le point tel que
$(\widehat{[AP),[AC)})=a$ et $(\widehat{[CA),[CP)})=c$,
$Q$ le point tel que
$(\widehat{[BQ),[BA)})=b$ et $(\widehat{[AB),[AQ)})=a$,
et $R$ le point tel que
$(\widehat{[CR),[CB)})=c$ et $(\widehat{[BC),[BR)})=b$.
Alors le triangle $BQR$ est
équilatéral.
\end{theo}

Pour montrer cela, on peut choisir un repère orthonormé
où $A$ et $B$ ont pour coordonnées respectives $(0,0)$
et $(1,0)$. On peut
définir une procédure qui donne l'équation de
la droite passant par un point et faisant un angle donné
avec l'axe des abscisses, et une procédure calculant
le point d'intersection de deux droites dont on connaît les
équations. On peut alors calculer les coordonnées de
$C$ en fonction des angles $a$ et $b$, ainsi que les
coordonnées de $P$, $Q$ et $R$. Il nous faut
aussi une procédure calculant le carré de la distance
entre deux points,
et enfin une dernière procédure testant si un triangle
est équilatéral.

Attention, pour les comparaisons, il faut utiliser une fonction
qui simplifie les expressions. Dans Maple~: {\tt simplify}, avec,
ici, option {\tt trig}.

\section{Le théorème de Brianchon}

\begin{theo}\label{brianchon}
Soit $E$ une ellipse. Soient $P_i$, $i=0,\dots,5$ six points deux à deux
distincts tels que les droites $(P_i,P_{i+1})$ et $(P_5,P_0)$ soient
tangentes à $E$. Alors les droites $(P_0,P_3)$, $(P_1,P_4)$ et $(P_2,P_5)$
sont concourantes.
\end{theo}

Pour démontrer ce théorème, on peut utiliser une équation paramétrée d'une
ellipse. L'ellipse d'équation 
$$\left(\frac{x-c_1}{d_1}\right)^2+\left(\frac{y-c_2}{d_2}\right)^2=1$$
a pour équation paramétrée
$$x=c_1+d_1\cos t\hbox{ , }y=c_2+d_2\sin t,$$
où $t$ parcourt $\RM$. On peut aussi utiliser
$$x=c_1+d_1\frac{t+1/t}2,\quad y = c_2+d_2\frac{t-1/t}{2i},$$
où $t$ parcourt le cercle des nombres complexes de module $1$. On peut
définir une procédure qui calcule la tangente à l'ellipse au point
correspondant à une valeur donnée du paramètre $t$, et appliquer cette
procédure à des valeurs indéterminées $t_1,\dots,t_5$. Puis, on calcule les
coordonnées des points $P_i$, grâce à une procédure qui calcule le point
d'intersection de deux droites. Une autre fonction permettant de calculer
l'équation d'une droite passant par deux points donnés nous donne les droites
$(P_0,P_3)$, $(P_1,P_4)$ et $(P_2,P_5)$. Grâce aux équations obtenues, on
vérifie la propriété requise.

\section{Le théorème des six cercles}

Ici, nous allons donner l'esquisse d'une démonstration
pour un théorème de géométrie.
Cette démonstration utilise un calcul
de résultant.

\begin{theo}\label{six_cercles}
Soient $xyz$ un triangle, $i$ le centre du cercle inscrit à
$xyz$, $\mathcal T$ l'enveloppe convexe de
$xyz$, $\mathcal C_x$ (resp. $\mathcal C_y$, $\mathcal C_z$
l'ensemble des cercles tangents à $(x,y)$ et $(x,z)$ (resp.
$(y,z)$ et $(y,x)$, $(z,x)$ et $(z,y)$) centrés sur $[x,i)$
(resp. $[y,i)$, $[z,i)$) qui rencontrent $\mathcal T$.
Soit $C_u\in\mathcal C_x$ un cercle
de rayon $u$ qui rencontre $\mathcal T$. Alors il existe un
cercle $C_v\in\mathcal C_y$ de rayon $v$ tangent extérieurement à $C_u$,
un cercle $C_w\in\mathcal C_z$ de rayon $w$ tangent extérieurement à $C_v$,
et un cercle $C_{u'}\in\mathcal C_x$ de rayon $u'$ tangent
extérieurement à $C_w$. De plus, ces cercles étant donnés,
il existe
un cercle $C_{v'}\in\mathcal C_y$ de rayon $v'$ tangent
extérieurement à $C_{u'}$ et un cercle
$C_{w'}\in\mathcal C_y$ de rayon $w'$ tangent
extérieurement à $C_{v'}$ tels que $C_{w'}$ est tangent
extérieurement à $C_{u}$.
\end{theo}

Dans la démonstration, on va supposer que le cercle inscrit est
de rayon $1$.
Soient $2\a$ (resp. $2\b$, $2\g$) la mesure de l'angle en $x$
(resp. $y$, $z$) dans $]0,\pi[$.

\begin{lemme}\label{inegalite}
Le cercle $C_u$ (resp. $C_v$, $C_w$) rencontre $\mathcal T$
si et seulement si $u\leq\frac{1}{ \tan\b\tan\g }$ (resp.
$v\leq\frac1{\tan\g\tan\a}$, $w\leq\frac1{\tan\a\tan\b}$).
\end{lemme}

\begin{proof}
Soit $j$ le centre du cercle exinscrit
en $x$, c'est à dire le cercle extérieur au triangle tangent
aux droites $(x,y)$, $(x,z)$ et $(z,y)$ tel que le point de
tangence avec cette dernière droite soit dans le segment
$[y,z]$. Alors le cercle $C_u$ rencontre $\mathcal T$ si et
seulement si son centre appartient à $[x,j]$. En considérant
des triangles rectangles bien choisis, on peut montrer
que si $C_u$ est de centre $j$, alors
$\frac{u}{\tan\a}=xy+u\tan\b$, et que
$xy=\frac1{\tan\a}+\frac1{\tan\b}$. Cela donne~:
$\frac{u}{\tan\a}=\frac1{\tan\a}+\frac1{\tan\b}+u\tan\b$,
et par suite $u=\frac1{\tan\b\tan\g}$.
\end{proof}

\begin{lemme}\label{relations}
Si les cercles $C_u$, $C_v$, $C_w$ et $C_{u'}$ sont comme dans
le théorème, on a les relations
$$\left(\frac1{\tan\a}(1-u)+\frac1{\tan\b}(1-v)\right)^2=4uv,$$
$$\left(\frac1{\tan\b}(1-v)+\frac1{\tan\g}(1-w)\right)^2=4vw,$$
$$\left(\frac1{\tan\g}(1-w)+\frac1{\tan\a}(1-u')\right)^2=4wu'.$$
\end{lemme}
\begin{proof}
Soient $s$ et $t$ les centre des cercles $C_u$ et $C_v$, on 
démontre que
$$st^2=(u+v)^2=(u-v)^2+\left(\frac1{\tan\a}+\frac
1{\tan\b}-\frac u{\tan\a}-\frac v{\tan\b}\right)^2,$$
ce qui donne la
formule désirée.
\end{proof}

On change maintenant de notations, en posant $a=\frac1{\tan\a}$,
$b=\frac1{\tan\b}$, $c=\frac1{\tan\g}$. Alors $a+b+c=abc$,
$a>0$, $b>0$ et $c>0$. De plus, les relations du lemme
\ref{relations} s'écrivent
\begin{equation}\label{E1}
\left(a(1-u)+b(1-v)\right)^2-4uv=0
\end{equation}
\begin{equation}\label{E2}
\left(b(1-v)+c(1-w)\right)^2-4vw=0
\end{equation}
\begin{equation}\label{E3}
\left(c(1-w)+a(1-u')\right)^2-4wu'=0
\end{equation}
Par ailleurs, les conditions du lemme~\ref{inegalite}
s'écrivent $0\leq u\leq bc$, $0\leq v\leq ca$, $0\leq w\leq ab$.

\begin{lemme}\label{heredite}
Si $u\leq bc$, alors les éléments $v$ définis par
l'équation~\eqref{E1} sont réels positifs ou nuls
et satisfont $v\leq ca$.
\end{lemme}
\begin{proof}
L'équation \eqref{E1}, vue comme polynôme en $v$, a pour
discriminant $\Delta=4(ab-1)(bc-u)u$. Par hypothèse, $bc-u\geq0$,
et les conditions sur $a$, $b$ et $c$ montrent que
$ab-1>0$ et $bc-1>0$. Ainsi, $\Delta\geq0$ et les racines
en $v$ sont réelles. Comme le terme constant $(a(1-u)+b)^2$
est positif ou nul et que le coefficient de $v$ est négatif
ou nul, les racines sont toutes deux positives ou nulles.
Il reste à montrer que si $v$ est une racine, alors
$v\leq ca$, ce qui se fait en utilisant les formules donnant
les racines d'un polynôme de degré $2$.
\end{proof}

Soient les polynômes de $\ZM[U,V,W,U',A,B,C]$ définis
par
$$P(U,V,A,B,C)=\left(A(1-U)+B(1-V)\right)^2-4UV=0,$$
$$Q(V,W,A,B,C)=\left(B(1-V)+C(1-W)\right)^2-4VW=0,$$
$$R(W,U',A,B,C)=\left(C(1-W)+A(1-U')\right)^2-4WU'=0.$$

Soient les résultants
$$S(V,U',A,B,C)=\Res_W(Q(V,W,A,B,C),R(W,U',A,B,C)),$$
$$T(U,U',A,B,C)=\Res_V(S(V,U',A,B,C),P(U,V,A,B,C)).$$

Soient $u$, $v$, $w$, $u'$, $a$, $b$, $c$ satisfaisant
les relations \eqref{E1}, \eqref{E2} et \eqref{E3}. Alors
$S(v,u',a,b,c)=0$, et $T(u,u',a,b,c)=0$. Or, on peut
factoriser le polynôme $T(U,U',A,B,C)-T(U',U,A,B,C)$ en
$(A+B+C-ABC)\Theta$, où $\Theta\in\ZM[U,U',A,B,C]$.
Comme $a+b+c=abc$, il suit que $T(u,u',a,b,c)=T(u',u,a,b,c)$,
et donc que $T(u',u,a,b,c)=0$. De là, on peut déduire l'existence
de $v'$ et $w'$ convenables tels que
$$P(u',v',a,b,c)=Q(v',w',a,b,c)=R(w',u,a,b,c)=0,$$
et démontrer le théorème.

\vskip 1cm

\misctitle{Références}

\begin{itemize}
\item \emph{Méthodes modernes en géométrie}, par Jean Fresnel.

\item Le théorème des sept cercles, par Evelyne, Money-Coutts et Tyrrell.

\item Le site web de Doron Zeilberger
\url{http://www.math.rutgers.edu/~zeilberg/}
(Ekhad's Geometry WebBook)
\end{itemize}

\end{document}
