Cabri-géomètre est un logiciel qui permet l'exploration de figures géométriques par manipulation directe des objets géométriques qui les constituent. Ce logiciel plonge l'utilisateur dans un micromonde intelligent et constitue ainsi un environnement d'apprentissage pour la géométrie. Les utilisateurs peuvent construire des figures géométriques, explorer le champ des animations et déformations de la construction, élaborer de nouveaux outils avec des macro-constructions, et spécialiser leur environnement pour des tâches spécifiques en y intégrant éventuellement leurs outils personnels. Le logiciel offre des possibilités de programmation par démonstration, mais les utilisateurs ont souvent besoin de manipuler la structure logique du programme construit pour le mettre au point et le maîtriser. Le choix d'une forme particulière pour présenter ce programme tient compte des spécificités du domaine de la géométrie dynamique et de la diversité des utilisateurs. Dans notre travail de prototypage, nous avons spécifié et implémenté un support textuel, mais laissé ouverte la possibilité de le compléter par un graphe. Le profil des utilisateurs a été pris en compte pour définir la forme de ce texte : en effet, la formalisation d'un langage de programmation sous-jacent aux constructions visuelles directes ne doit pas constituer une contrainte, et la familiarisation avec ce langage (moyen de communication entre l'utilisateur et le logiciel) doit se faire de façon inconsciente. Ces exigences ont abouti à l'intégration dans Cabri-II d'une vue textuelle des figures, équivalente à la vue graphique, dynamique autant que la figure (dans ce sens que le programme se construit en même temps que la figure), et où l'ubiquité des objets dans les vues synchrones permet un apprentissage implicite du langage de Cabri-programmation. La "qualité dynamique" de la géométrie dans la figure est traduite par la "qualité formelle" du langage induit, et les manipulations de l'interface sont transcrites en des animations du texte. La démarche consistant à partir d'une programmation visuelle pour l'expliciter en une programmation textuelle est nouvelle, pose des problèmes spécifiques intéressants, et pourrait assez rapidement être complétée, puis être appliquée avec profit à d'autres environnements analogues.

Ce document traite de plusieurs aspects de la vision stéréoscopique par ordinateur. Cette méthode consiste à partir d'une ou de plusieurs paires d'images à " reconstruire " une scène observée en trois dimensions, c'est-à-dire à produire une description des objets et surfaces observés ainsi que leur position dans l'espace. Le premier problème abordé est celui du calibrage, dont l'objet est de calculer les paramètres des caméras (focale, centre optique, etc.) ainsi que leur position, soit à partir d'images d'objets de géométrie et de position connue, soit de manière automatique (on parle alors d'auto-calibrage). Des résultats nouveaux sont présentés sur l'auto-calibrage de la distorsion optique et sur l'auto-calibrage d'une paire de caméras rigidement liées à partir de plusieurs paires d'images. Ensuite sont présentées différentes méthodes permettant de rectifier les images de manière à simplifier la mise en correspondance, puis d'effectuer cette mise en correspondance par une technique de corrélation. Outre des améliorations des résultats classiques, de nouvelles méthodes permettant d'obtenir une plus grande précision sont discutées. La dernière phase, dite de reconstruction, permet d'obtenir une description des surfaces observée allant jusqu'aux propriétés différentielles d'ordre un et deux (plan tangent et courbures à la surface), à partir des résultats de stéréoscopie par corrélation. Ce document se termine par quelques applications réalisées au cours de ces recherches telles qu'un système d'aide chirurgicale pré-opératoire ou une caméra stéréo bon marché.

Mon travail de thèse consiste à comprendre une géométrie introduite par Cartan en 1933 \cite{Cartan1933}. \textit{La géométrie de Finsler} présente de nombreuses analogies avec cette théorie. Nous avons étudié les grandes lignes de cette géométrie. Le point de départ de Cartan qui est analogue à celui qui conduit à la géométrie finslerienne, est d'imaginer l'espace comme étant un lieu ''d'éléments de contact'', un élément étant la donnée d'un point $M\in\mathcal{M}^n$ et d'un hyperplan $H$ passant par ce point et orienté dans l'espace tangent $T_M\mathcal{M}^n$. Nous avons ainsi défini \textit{la géométrie de Cartan fondée sur la notion d'aire} dans un premier temps, je me suis intéressé à la notion d'orthogonalité dans cette géométrie. La méthode de Cartan pour étudier le problème d'équivalence est un outil puissant qui est implicitement décrit dans cette géométrie. Nous avons ensuite appliqué cette méthode aux équations de Monge-Ampère (cas elliptique), en s'inspirant des travaux de R. Bryant, D. Grossmann et P. Griffiths. Plusieurs faits ne sont pas encore suffisamment clairs pour disposer d'un dictionnaire évident entre ces travaux et celui donné par Cartan.

Notre travail de thèse vise à étudier des utilisations réelles des TICE dans les classes par des enseignants, grâce à une méthodologie basée sur l'observation de séances ordinaires.<br />Nous partons du constat d'écart entre, d'une part, les potentialités des TICE soulignées par la recherche et la volonté institutionnelle d'insérer les TICE, et d'autre part, la réalité de la faible intégration de la technologie dans les classes. Nous considérons cet écart comme l'effet des contraintes d'utilisation des TICE mentionnée dans de nombreux travaux en didactique des mathématiques. L'hypothèse est que l'enseignant, qui prend la décision d'utiliser les TICE, est motivé par des potentialités de la technologie présentes dans ses représentations et qu'il effectue des choix ayant une certaine conscience des contraintes de leur utilisation. Nous cherchons à étudier des rapports entre ces potentialités et celles qui sont exprimées dans la recherche et les instructions officielles, et leur actualisation dans la pratique en classe. Nous nous intéressons plus spécifiquement aux usages de la géométrie dynamique dans des classes du collège (élèves de 12-15 ans), car les potentialités de la géométrie dynamique font l'objet de nombreux travaux et écrits, et les instructions officielles en France insistent sur leurs apports possibles à l'enseignement à ce niveau. <br />Dans la thèse, nous présentons l'analyse des séances illustrant deux types d'usages rencontrés chez trois enseignants. Dans le but de caractériser plus finement le fonctionnement de ces enseignants dans sa complexité, nous interprétons l'analyse des séances à l'aide d'un modèle théorique.

Dans cette thèse nous introduisons la notion de fibré tt* (E,D,S), de fibré tt* métrique (E,D,S,g) et de fibré tt* symplectique (E,D,S,w) sur un fibré vectoriel E au-dessus d'une variété complexe, dans le langage de la géométrie différentielle réelle. Grâce à cette notion on obtient une correspondance entre des fibrés tt* métriques et des applications pluriharmoniques admissibles de (M,J) dans l'espace symétrique pseudo-Riemannien GL(r,R)/O(p,q), avec (p,q) la signature de la métrique g. En utilisant ce résultat on obtient dans le cas où M est compact Kählérienne, un résultat de rigidité, puis un cas particulier du théorème de Lu. <br />De plus nous étudions des fibrés tt* sur le fibré tangent TM et caractérisons une classe spéciale qui contient les variétés spéciales complexes et les variétés nearly Kählériennes plates, et la sous-classe qui admet un fibré tt* métrique ou symplectique. En outre on analyse les fibrés tt* qui proviennent de variations de structures de Hodge (VHS) et de fibrés harmoniques. Pour les fibrés harmoniques, la correspondance permet de généraliser un résultat de Simpson. L'application pluriharmonique associée à une variété spécialement Kählérienne reliée à l'application de Gauß duale, et celle associée à une VHS de poids impair est l'application de périodes. Si la structure complexe n'est pas intégrable, on doit généraliser la notion de pluriharmonicité. <br />Hors la rigidité ces résultats sont généralisés au cas para-complexe.

L'objet de cette thèse est la formalisation et l'automatisation du raisonnement géométrique au sein de l'assistant de preuve Coq.<br />Dans une première partie, nous réalisons un tour d'horizon des principales axiomatiques de la géométrie puis nous présentons une formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie.<br />Dans la seconde partie, nous présentons l'implantation en Coq d'une procédure de décision pour la géométrie affine plane : la méthode des aires de Chou, Gao et Zhang. Cette méthode produit des preuves courtes et lisibles.<br />Dans la troisième partie, nous nous intéressons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof. GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq.<br />Enfin, nous proposons un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.

La gravité quantique à boucles est une théorie candidate à la description unifiée de la relativité générale et de la mécanique quantique à l'échelle de Planck. Cette théorie peut être formulée de deux manières. L'approche canonique, d'une part, cherche à résoudre l'équation de Wheeler--DeWitt et à définir les états physiques. L'approche par les écumes de spins, d'autre part, a pour but de calculer les amplitudes de transition de la gravité quantique via une intégrale de chemin covariante. Ces deux approches s'appuient sur a même structure d'espace de Hilbert, mais la question de leur correspondance exacte reste un important problème ouvert à ce jour. Dans ce travail de thèse, nous présentons quatre résultats en rapport avec ces deux approches. Après un premier chapitre introductif, le second chapitre concerne l'étude de la théorie classique. Historiquement, l'introduction des variables d'Ashtekar complexes (self-duales) dans la formulation hamiltonienne de la relativité générale fut motivée par l'obtention d'une contrainte scalaire polynomiale. Cette simplification drastique est à la base du programme de la gravité quantique à boucles. Pour un certain nombre de raisons techniques, ces variables complexes furent ensuite abandonnées au profit des variables d'Ashtekar-Barbero, pour lesquelles le groupe de jauge est SU(2). Avec ce choix de variables réelles, la contrainte hamiltonienne n'est malheureusement plus polynomiale. La formulation en terme des variables SU(2) réelles peut être obtenue à partir de l'action de Holst, qui contient le paramètre dit de Barbero-Immirzi comme constante de couplage additionnelle. Dans un premier temps, nous allons utiliser les variables d'Ashtekar complexes pour effectuer l'analyse canonique de l'action de Holst avec un paramètre de Barbero-Immirzi réel. Les contraintes qui découlent de cette analyse canonique dépendent de ce paramètre libre, et ont l'avantage d'être polynomiales. Afin de garantir que la métrique soit une quantité réelle, un ensemble de contraintes de réalité doivent être imposées. Il s'avère que ces conditions de réalité correspondent aux contraintes de simplicité linéaires utilisées pour la construction des modèles d'écumes de spins. Ces contraintes sont préservées par l'évolution hamiltonienne si et seulement si la connexion est sans torsion. Cette condition sur l'absence de torsion est en fait une contrainte secondaire de l'analyse canonique. La second chapitre concerne également la théorie classique, mais s'intéresse à sa discrétisation en terme des variables de premier ordre dites holonomie-flux. L'espace des phases qui résulte de cette construction possède une structure non-linéaire. Le formalisme des twisteurs permet d'accommoder cette non-linéarité en travaillant sur un espace des phases linéaire paramétré par les coordonnées canoniques de Darboux. Ce formalisme fut introduit par Freidel et Speziale, mais uniquement dans le cas des variables SU(2) d'Ashtekar-Barbero. Nous généralisons ce résultat au cas du groupe de Lorentz. Nous étudions ensuite la dynamique en terme d'écumes de spins obtenue à partir de ces variables, et développons une nouvelle formulation hamiltonienne de la gravité discrétisée. Ce nouveau formalisme est obtenu en écrivant l'action de la théorie continue sur une discrétisation simpliciale de l'espace-temps fixée. L'action discrète ainsi obtenue est la somme de l'analogue en terme de spineurs d'une action topologique de type BF et des contraintes de réalité qui garantissent l'existence d'une métrique réelle. Cette action est polynomiale en terme des spineurs, ce qui permet de procéder à sa quantification canonique de manière relativement aisée. Le dernier chapitre s'intéresse à la théorie quantique obtenue suivant cette procédure. Les amplitudes de transition reproduisent celles du modèle d'écume de spins EPRL (Engle Pereira Rovelli Livine). Ce résultat est intéressant car il démontre que la formulation de la gravité quantique en termes d'écumes de spins peut être obtenue à partir d'une action classique écrite en terme de spineurs.

Les dernières années ont vu émerger différents points de vue sur les espaces analytiques p-adiques. Ce texte est consacré spécifiquement à celui qu'a introduit Vladimir G. Berkovich à la fin des années quatre-vingt, et qui s'est révélé l'un des plus féconds. Nous en aborderons divers aspects. Dans la première partie du manuscrit, nous dépasserons le cadre p-adique pour nous intéresser aux espaces analytiques globaux : ceux qui sont définis sur Z ou les anneaux d'entiers de corps de nombres. Nous prouverons qu'ils jouissent, au moins localement, de propriétés analogues à celles des espaces analytiques complexes classiques. Par la suite, nous nous tournerons vers les espaces p-adiques pour étudier leur topologie et démontrer plusieurs résultats de modération. Finalement, nous présenterons quelques applications aux équations différentielles p-adiques sur les courbes analytiques et expliquerons notamment pourquoi leur comportement est contrôlé par un graphe localement fini.

L'ensemble des thématiques abordées s'inscrivent dans le contexte de la modélisation et du calcul géométrique.

Cette thèse est consacrée à la géométrie des variétés de Fano et des fibrés projectifs sur une courbe projective lisse.Dans la première partie on étudie la géométrie des variétés de Fano pas trop singulières admettant un diviseur premier de nombre de Picard 1. En étudiant les contractions associées aux rayons extrémaux dans le cône de Mori de ces variétés nous fournissons un théorème de structure en dimension 3 pour les variétés dont le nombre de Picard est maximal. Ensuite, nous traitons le cas des variétés toriques et nous étendons le théorème de structure aux variétés toriques de dimension supérieure à 3 dont le nombre de Picard est maximal. Enfin, nous traitons les relèvements des contractions extrémales aux espaces de revêtement universels en codimension 1.Dans la deuxième partie on étudie les corps de Newton-Okounkov sur les fibrés projectifs sur une courbe projective lisse. En nous inspirant des estimations de Wolfe utilisées pour calculer la fonction de volume sur ces variétés, nous calculons tous les corps de Newton-Okounkov par rapport aux drapeaux linéaires et nous étudions comment ces corps dépendent de la décomposition en cellules de Schubert par rapport aux drapeaux linéaires compatibles avec la filtration de Harder-Narasimhan du fibré. De plus, nous caractérisons les fibrés vectoriels semi-stables sur une courbe projective lisse à l'aide des corps de Newton-Okounkov. / This thesis is devoted to the geometry of Fano varieties and projective vector bundles over a smooth projective curve.In the first part we study the geometry of mildly singular Fano varieties on which there is a prime divisor of Picard number 1. By studying the contractions associated to extremal rays in the Mori cone of these varieties, we provide a structure theorem in dimension 3 for varieties with maximal Picard number. Afterwards, we address the case of toric varieties and we extend the structure theorem to toric varieties of dimension greater than 3 and with maximal Picard number. Finally, we treat the lifting of extremal contractions to universal covering spaces in codimension 1.In the second part we study Newton-Okounkov bodies on projective vector bundles over a smooth projective curve. Inspired by Wolfe's estimates used to compute the volume function on these varieties, we compute all Newton-Okounkov bodies with respect to linear flags and we study how these bodies depend on the Schubert cell decomposition with respect to linear flags which are compatible with the Harder-Narasimhan filtration of the bundle. Moreover, we characterize semi-stable vector bundles over smooth projective curves via Newton-Okounkov bodies.