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.

Cette thèse est consacrée à l'étude de deux sujets de géométrie symplectique inspirés<p>de la physique mathématique. Les thèmes que nous développerons mettent en évidence certaines <p>connexions avec la topologie symplectique d'une part, la géométrie Riemannienne d'autre part.<p><p>Dans la partie 1, nous étudions la quantification par déformation formelle d'une variété <p>symplectique, à l'aide de produits star. Nous définissons le groupe des automorphimes<p>hamiltoniens d'un produit star formel. En nous inspirant d'idées de Banyaga, nous <p>identifions ce groupe comme étant le noyau d'un morphisme remarquable sur le groupe<p>des automorphismes du produit star. Nous relions certaines propriétés géométriques de <p>ce groupe d'automorphismes hamiltoniens à la topologie du groupe des difféomorphismes<p>hamiltoniens.<p><p>Dans la partie 2, nous étudions les opérateurs de Dirac symplectiques. Les ingrédients<p>nécessaires à leur construction (algèbre de Weyl, structures $Mp^c$, champs de spineurs <p>symplectiques, connexions symplectiques,) sont également utilisés en quantification géométrique et en<p>quantification par déformation formelle. Les opérateurs de Dirac symplectiques sont construits<p>de manière analogue à l'opérateur de Dirac de la géométrie Riemannienne. Une formule de Weitzenbock<p>lie les opérateurs de Dirac symplectiques à un opérateur elliptique $mathcal{P}$ d'ordre 2. Nous étudions<p>les noyaux de ces opérateurs de Dirac symplectiques et leur lien avec le noyau de P.<p>Sur l'espace hermitien symétrique $CP^n$, nous calculerons le spectre de $mathcal{P}$ et nous <p>prouverons un théorème de Hodge pour les opérateurs de Dirac-Dolbeault symplectiques.<p><p>/<p><p>In this thesis we study two topics of symplectic geometry inspired from mathematical physics.<p><p>Part 1 is devoted to the study of deformation quantization of symplectic manifolds. More precisely, we consider formal star products on a symplectic manifold. We define the group of Hamiltonian automorphisms of a formal star product. Following ideas of Banyaga, we describe this group as the kernel<p>of a morphism on the group of automorphisms of the star product. We relate geometric properties of the group of Hamiltonian automorphisms to the topology of the group of Hamiltonian diffeomorphisms. <p><p>Part 2 is devoted to the study of symplectic Dirac operators. The construction of those operators relies on many concepts used in geometric quantization and formal deformation quantization such as Weyl algebra, $Mp^c$ structures, symplectic spinors, symplectic connections, The construction of symplectic Dirac operators is analogous to the one of Dirac operators in Riemannian geometry. A Weitzenbock formula relates the symplectic Dirac operators to an elliptic operator $mathcal{P}$ of order 2. We study the kernels of the symplectic Dirac operators and relate them to the kernel of $mathcal{P}$. On the hermitian symmetric space <p>$CP^n$, we compute the spectrum of $mathcal{P}$ and we prove a Hodge theorem for the symplectic Dirac-Dolbeault operator. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Dans cette thèse, nous appliquons des outils issus de la théorie d’Arakelov à l’étude de problèmes de géométrie diophantienne. Une notion centrale dans notre étude est la théorie des pentes des fibrés vectoriels hermitiens, introduite par Bost dans les années 90. Nous travaillons plus précisément avec sa généralisation dans le cadre adélique, inspirée par Zhang et développée par Gaudron. Ce mémoire s’articule autour de deux axes principaux. Le premier consiste en l’étude d’un remarquable théorème de géométrie diophantienne dû à Faltings etWüstholz, qui généralise le théorème du sous-espace de Schmidt. Nous commencerons par retranscrire la démonstration de Faltings et Wüstholz dans le langage de la théorie des pentes. Dans un second temps, nous établirons des variantes effectives de ce théorème, que nous appliquerons pour démontrer une généralisation effective du théorème de Liouville valable pour les points fermés d’une variété projective fixée. Ce résultat fournit en particulier une majoration explicite de la hauteur des points satisfaisant une inégalité analogue à celle du théorème de Liouville classique. Dans la seconde partie de cette thèse, nous établirons de nouvelles mesures d’indépendance linéaire de logarithmes dans un groupe algébrique commutatif, dans le cas dit rationnel.Notre approche utilise les arguments de la méthode de Baker revisitée par Philippon et Waldschmidt, combinés avec des outils de la théorie des pentes. Nous y intégrons un nouvel argument, inspiré par des travaux antérieurs de Bertrand et Philippon, nous permettant de contourner les difficultés introduites par le cas périodique. Cette approche évite le recours à une extrapolation sur les dérivations à la manière de Philippon et Waldschmidt. Nous parvenons ainsi à supprimer une hypothèse technique contraignante dans plusieurs théorèmes de Gaudron, tout en précisant les mesures obtenues. / In this thesis, we study diophantine geometry problems on projective varieties and commutative algebraic groups, by means of tools from Arakelov theory. A central notion in this work is the slope theory for hermitian vector bundles, introduced by Bost in the 1990s. More precisely, we work with its generalization in an adelic setting, inspired by Zhang and developed by Gaudron. This dissertation contains two major lines. The first one is devoted to the study of a remarkable theorem due to Faltings and Wüstholz, which generalizes Schmidt’s subspace theorem. We first reformulate the proof of Faltings and Wüstholz using the formalism of adelic vector bundles and the adelic slope method. We then establish some effective variants of the theorem, and we deduce an effective generalization of Liouville’s theorem for closed points on a projective variety defined over a number field. In particular, we give an explicit upper bound for the height of the points satisying a Liouville-type inequality. In the second part, we establish new measures of linear independence of logarithms over a commutative algebraic group. We focus our study on the rational case. Our approach combines Baker’s method (revisited by Philippon and Waldschmidt) with arguments from the slope theory. More importantly, we introduce a new argument to deal with the periodic case, inspired by previous works of Bertrand and Philippon. This method does not require the use of an extrapolation on derivations in the sense of Philippon-Waldschmidt. In this way, we are able to remove an important hypothesis in several theorems of Gaudron establishing lower bounds for linear forms in logarithms.

Une théorie fixé de la gravitation est loin d' être complète. La théorie plus prometteuse parmi ces théories de la gravité dans ce siècle est la relativité générale (RG), qui est toujours rencontre des obstacles par plusieurs problèmes. Les problèmes que nous soulignons dans cette thèse sont les aspects thermodynamiques et la quantification de la gravitation. Les tentatives proposées pour comprendre d'aspect thermodynamique de RG ont déjà été étudiés par la thermodynamique des trous noirs, alors que la théorie de la gravité quantique a déjà eu plusieurs des candidats, l'un d' entre eux était la gravité quantique à boucles (LQG), celui qui est la théorie base de notre travail. La théorie correcte de la gravité quantique devrait offrir une limite classique qui est correcte et consistent , ce qui évidemment , la relativité générale. / A fixed theory of gravity is far from being complete. The most promising theory of gravity in this century is general relativity (GR), which is still plagued by several problems. The problems we highlight in this thesis are the thermodynamical aspects and the quantization of gravity. Attempts to understand the termodynamical aspect of GR have already been studied through the thermodynamics of black holes, while the theory of quantum gravity has already had several candidates, one of them being the canonical loop quantum gravity (LQG), which is the base theory in our work.

L'objet de cette thèse est l'étude mathématique de familles d'espaces-temps satisfaisant aux équations d'Einstein de la Relativité Générale. Deux approches sont considérées pour cette étude. La première partie, composée des trois premiers chapitres, examine les propriétés géométriques des espaces-temps d'Emparan-Reall et dePomeransky-Senkov, de dimension 5. Nous montrons qu'ils contiennent un trou noir, dont l'horizon des événements est à sections compactes non-homéomorphes à la sphère. Nous en construisons une extension analytique et prouvons que cette extension est maximale et unique dans une certaine classe d'extensions pour les espaces-temps d'Emparan-Reall. Nous établissons ensuite le diagramme de Carter-Penrose de ces extensions, puis analysons la structure de l'ergosurface des espaces-temps de Pomeransky-Senkov. La deuxième partie est consacrée à l'étude de données initiales, solutions des équations des contraintes, induites par les équations d'Einstein. Nous effectuons un recollement d'une classe de données initiales avec des données initiales d'espaces-temps de Kerr-Kottler-deSitter, en utilisant la méthode de Corvino. Nous construisons, d'autre part, des métriques asymptotiquement hyperboliques en dimension 3, satisfaisant les hypothèses du théorème de masse positive à l'exception de la complétude, et ayant un vecteur moment-énergie de genre causal arbitraire. / The aim of this thesis is the mathematical study of families of spacetimes satisfying the Einstein's equations of General Relativity. Two methodsare used in this context.The first part, consisting of the first three chapters of this work,investigates the geometric properties of the Emparan-Reall andPomeransky-Senkov families of 5-dimensional spacetimes. We show that they contain a black-hole region, whose event horizon has non-spherical compact cross sections. We construct an analytic extension, and show its maximality and its uniqueness within a natural class in the Emparan-Reallcase. We further establish the Carter-Penrose diagram for these extensions, and analyse the structure of the ergosurface of the Pomeransky-Senkovspacetimes.The second part focuses on the study of initial data, solutions of theconstraint equations induced by the Einstein's equations. We perform agluing construction between a given family of inital data sets andinitial data of Kerr-Kottler-de Sitter spacetimes, using Corvino'smethod.On the other hand, we construct 3-dimensional asymptotically hyperbolicmetrics which satisfy all the assumptions of the positive mass theorem but the completeness, and which display an energy-momentum vector of arbitry causal type.

En informatique, les images sont numériques et donc composées de pixels en 2D et de voxels en 3D. Dans une scène virtuelle 3D, il est impossible de manipuler directement les objets comme des ensembles de voxels en raison du trop gros volume de données. Les objets sont alors polyédrisés, c’est-à-dire remplacés par une collection de facettes. Pour ce faire, il est primordial de savoir décider si un sous-ensemble de voxels peut être transformé en une facette dans la représentation polyédrique. Ce problème est appelé reconnaissance de plans discrets. Pour le résoudre, nous mettons en place un nouvel algorithme spécialement adapté pour les ensembles de voxels denses dans une boite englobante. Notre méthode atteint une complexité quasi-linéaire dans ce cas et s’avère efficace en pratique. En parallèle, nous nous intéressons à un problème algorithmique annexe intervenant dans notre méthode de reconnaissance de plans discrets. Il s’agit de calculer les deux enveloppes convexes des points de Z2 contenus dans un domaine vertical borné et situés de part et d’autre d’une droite quelconque. Nous proposons une méthode de complexité optimale et adaptative pour calculer ces enveloppes convexes. Nous présentons le problème de manière détournée : déterminer le nombre rationnel à dénominateur borné qui approxime au mieux un nombre réel donné. Nous établissons le lien entre ce problème numérique et son interprétation géométrique dans le plan. Enfin, nous proposons indépendamment un nouvel algorithme pour calculer l’épaisseur d’un ensemble de points dans le réseau Zd. Notre méthode est optimale en 2D et gloutonne mais efficace en dimension supérieure / In computer science, pictures are digital and so, they are composed of pixels in 2D or of voxels in 3D. In 3D virtual scenes, we cannot directly manipulate objects as sets of voxels because the data are too huge. As a result, the objects are transformed into polyhedra, i.e. collections of facets. For this, we must be able to decide if a subset of voxels can be replaced by a facet in the polyhedrisation. This problem is called digital plane recognition. To solve it, we design a new algorithm especially adapted for sets of voxels which are dense in a bounding box. Our method achieves a quasi-linear worst-case time complexity in this case and it is efficient in practice. In parallel, we study another algorithmic problem which occures in our digital plane recognition algorithm. It is computing the two convex hulls of grid points lying in a bounded vertical domain and located on either side of a straight line. We propose an optimal time complexity method to compute these convex hulls and which is also output sensitive. We present the problem in a different way : find the rational number of bounded denominator that best approximates a given real number. We establish the link between this numerical problem and geometry. Finally, we independently propose a new algorithm to compute the lattice width of a set of points in Zd. Our method is optimal in 2D and is greedy but efficent in higher dimension