Dans cet exposé, on étudie les ensembles de degrés Turing associés aux pavages générés par un jeu de tuile. En particulier, on prouve qu'il existe un quasi-isomorphisme entre n'importe quelle classe Pi01 de {0,1}^N et un pavage. Pour cela, on introduit une construction permettant d'avoir du calcul tout en ayant un nombre dénombrable de pavages.
On présentera deux modèles où de fortes oscillations peuvent induire sur le problème limite un gain de dissipation. Le premier concerne l'étude d'un fluide visqueux forcé par une source fortement oscillante. On perturbe une solution stationnaire à l'instant initial. On montre que le temps d'existence de la famille de solutions perturbées peut être minoré indépendamment de la taille de la perturbation. En particulier, on exhibe une solution approchée qui justifie que l'interaction d'oscillations peut se traduire au niveau macroscopique par la création d'une viscosité turbulente. Puis on développera un modèle de plasmas pour ITER avec collisions. Sous l'effet d'un champ magnétique, les particules tournent fortement autour des lignes de champ. Lorsque il devient très grand (les oscillations sont très rapides) le terme de collisions, qui dissipe uniquement en vitesse initialement, fait apparaître une dissipation en position.
Le problème de la maximisation des valeurs propres de Neunmann d'un domaine euclidien est très difficile. Pour un domaine du plan, la conjecture de Polya (1954) dit que les valeur propres mu_k de Neumann sont bornées supérieurement par 4k Pi. Dans cet exposé je présenterai une inégalité optimale pour la deuxième valeur propre non nulle mu_2. Je discuterai aussi la maximisation des valeurs propre de Steklov d'un domaine du plan, ainsi que le contrôle isopérimétrique de ce spectre en dimension supérieure à deux. Les travaux présentés sont des collaborations avec N. Nadirashvili, I. Polterovich, B. Colbois et A. El Soufi.
On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.
Nous commencerons par rappeler un résultat avec Jan Denef reliant espaces d'arcs et points fixes des itérés de la monodromie. Puis nous exposerons un travail récent en collaboration avec Ehud Hrushovski qui en donne une nouvelle démonstration. Cette nouvelle approche, plus géométrique, est basée sur la géométrie non-archimédienne.
Upper bounds are obtained for the heat content of an open set D in a geodesically complete Riemannian manifold M with Dirichlet boundary condition on the boundary of D, and non-negative initial condition. We show that these upper bounds are close to being sharp if (i) the Dirichlet-Laplace-Beltrami operator acting in L2(D) satisfies a strong Hardy inequality with weight d^{-2}, (ii) the initial temperature distribution, and the specific heat of D are given by d^{-a} and d^{-b} respectively, where d is the distance to the boundary of D, and 1 < a < 2; 1 < b < 2.
Le flot géodésique d'une variété à courbure sectionnelle majorée par une constante négative admet une mesure -- dite de Patterson-Sullivan -- relativement à laquelle il est totalement dissipatif et non ergodique ou bien totalement conservatif et ergodique. Nous montrons que cette « loi du zéro-un » est encore satisfaite pour les variétés de rang un.
On s'intéresse à trouver la constante optimale pour l'immersion de l'espace W^{2,1}_Delta(Omega) qui est l'ensemble des u dans W^{1,1}_0(Omega) tel que Delta u appartienne à L^1(Omega) dans L^1(Omega) où Omega est un domaine borné de R^n avec frontière de classe C^{1,1}. Ceci est équivalent à trouver la première valeur propre de l'opérateur 1-biharmonique avec conditions au bord de Navier (généralisées). Dans cet exposé on donne une interpretation du problème aux valeurs propres, on montre une inégalité du type Faber-Krahn, et, si Omega est une boule, on calcule explicitement la première valeur propre et la fonction propre associée. Les résultats ont été obtenus en collaboration avec Bernhard Ruf et Cristina Tarsi (Université degli Studi di Milano)
Le problème de Schottky consiste à caractériser les jacobiennes des surfaces de Riemann parmi les variétés abéliennes principalement polarisées. Ce problème classique a été abordé sous de nombreux angles. Dans ce travail en collaboration avec F. Balacheff et H. Parlier, nous généralisons l'approche géométrique développée par P. Buser et P. Sarnak en obtenant de nouvelles estimées sur les longueurs des réseaux des périodes des jacobiennes.
Cet exposé est consacré à l'étude de systèmes (elliptiques avec condition de Dirichlet sur le bord) comportant des oscillations à l'échelle microscopique. L'objectif est de caractériser la limite lorsque la taille caractéristique des oscillations tend vers 0, autrement dit d'homogénéiser les petites échelles. Suivant que les oscillations sont périodiques et concernent les coefficients du système, ou sont contenues dans la donnée sur le bord (systèmes de couche limite), leur effet sur la limite est très différent. Nous passerons en revue les résultats classiques sur les développements multi-échelles, et montrerons des résultats récents sur l'homogénéisation du problème de couche limite
La classification des matériaux élastiques est un vieux problème de mécanique assez fascinant pour les mathématiciens car sa résolution explicite nécessite de nombreux outils mathématiques : théorie des invariants, calcul de stratification, etc. Je présenterai quelques travaux récents sur ce problème et les questions ouvertes qu'il introduit.
« div(T) = 0, c'est la mécanique ! » . À partir de cette expression attribuée à Einstein, Jean-Marie Souriau a formulé une équation universelle de la mécanique, dont dérive la plupart des modèles de la mécanique des milieux continus. Cet exposé propose de présenter cette formulation géométrique, élégante et encore mal connue.
Au cours de cet exposé, j'introduirai deux approches qui aboutissent à la résolution de modèles non-locaux pour l'analyse de la dynamique sédimentaire. La première portera sur l'équation d' A.-C. Fowler qui correspond à l'équation de Burgers visqueuse modifiée par un terme non-local qui peut être identifié à un Laplacien fractionnaire anti-diffusif. Dans la seconde approche, nous utilisons les principes de minimisation pour décrire l'évolution d'un lit érodable sous l'action de l'eau. Il sera intéressant de constater que cette seconde méthode peut être liée à la première.
Dans cette exposé, nous proposons une nouvelle formulation des problèmes d'estimation de flot optique et de stéréo-vision qui repose sur une analogie avec les problèmes de débruitage. Le caractère mal posé de ces problème nous conduit à la régularisation par variation totale que nous controllons grâce a des modèles de décomposition.
L'exposé est consacré aux groupes d'homologie dans le cadre tropical. Sous certaines conditions, une variété tropicale peut être approximée par une famille à un paramètre de variétés complexes, et des caractéristiques importantes des variétés de cette famille peuvent être exprimées en termes des groupes d'homologie tropicaux de la variété tropicale considérée. (Travail en commun avec L. Katzarkov, G. Mikhalkin et I. Zharkov.)
Un résultat central de géométrie analytique réelle est le théorème de rectilinéarisation d'Hironaka, qui affirme que tout ensemble sous-analytique borné peut être décrit par un nombre fini d'égalités et inégalités satisfaites par des compositions de fonctions analytiques et de la fonction 1/x. Nous étendons cet énoncé à des algèbres quasi-analytiques, en donnant des exemples d'applications. Nous expliquons en particulier comment des arguments de théorie des modèles permettent de se passer du traditionnel théorème de préparation de Weierstrass, qui fait défaut dans les classes quasi-analytiques. (travail en commun avec J.-P. Rolin).
L'algorithme de Metropolis est un algorithme permettant de tirer un point au hasard pour une probabilité donnée. Il a été introduit en 1953 par N. Metropolis, A.-W. Rosenbluth, M.-N. Rosenbluth, A.-H. Teller, E. Teller, dans l'article '' Equations of State Calculations by Fast Computing Machines, Journal of Chemical Physics 21 (6) 1087--1092. Il a ensuite été généralisé en 1970 par W.-K. Hastings dans Monte Carlo Sampling Methods Using Markov Chains and Their Applications'', Biometrika 57 (1) 97?109. Cet algorithme, et ses variantes, est un des plus utilisés du calcul scientifique, voir par exempletop ten algorithms of the century'' sur google. Son étude mathématique est par contre très loin d'être achevée et pose des problèmes fort intéressants de géométrie, de théorie spectrale, d'analyse, et bien sur de probabilités. Dans cet exposé, je commencerai par introduire l'algorithme sous sa forme historique : Comment choisir N disques de rayon r (sans recouvrement ) au hasard dans un carré? et j'indiquerai quelques résultats et problèmes ouverts sur ce modèle. Dans une deuxième partie, je montrerai comment les plus simples des algorithmes de Metropolis, associés à des marches aléatoires à ``petits pas'', conduisent à l'étude d'opérateurs qui généralisent les opérateurs du calcul pseudodifférentiel semiclassique usuel.
The categorical presentation of the standard model of the geometry of interaction –namely the free compact closure of sets and partial injections Int(PInj)– fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.
There is a wide gap between the language of mathematics and its formalized versions. The term language of mathematics'' ormathematical language'' refers to prose that the mathematician uses in authoring textbooks and publications. It mainly consists of natural language, symbolic expressions and notations. It is flexible, structured and semantically well-understood by mathematicians. However, it is very difficult to formalize it automatically. Some of the main reasons are: complex and rich linguistic features of natural language and its inherent ambiguity; intermixing of natural language with symbolic mathematics causing problems which are unique of its kind, and therefore, posing more ambiguity; and the possibility of containing reasoning gaps, which are hard to fill using the current state of art theorem provers (both automated and interactive). One way to work around this problem is to abandon the use of the language of mathematics. Therefore in current state of art of theorem proving, mathematics is formalized manually in very precise, specific and well-defined logical systems. The languages supported by these systems impose strong restrictions. For instance, these languages have non-ambiguous syntax with a limited number of possible syntactic constructions. This enterprise divides the world of mathematics in two groups. The first group consists of a vast majority of mathematicians whose rely on the language of mathematics only. In contrast, the second group consists of a minority of mathematicians. They use formal systems such as theorem provers (interactive ones mostly) in addition to the language of mathematics. To bridge the gap between the language of mathematics and its formalized versions, we may ask the following gigantic question: Can we build a program that understands the language of mathematics used by mathematicians and can we mechanically verify its correctness? This problem can naturally be divided in two sub-problems, both very hard: 1. Parsing mathematical texts (mainly proofs) and translating those parse trees to a formal language after resolving linguistic issues. 2. Validation of this formal version of mathematics. The project MathNat (Mathematics in controlled Natural language) aims at being the first step towards solving this problem, focusing mainly on the first question. For that, first, we develop a Controlled Language for Mathematics (CLM) which is a precisely defined subset of English with restricted grammar and lexicon. To make CLM natural and expressive, we support important linguistic features such as anaphoric pronouns and references, rephrasing of a sentence in multiple ways, the proper handling of distributive and collective readings and so on. The coverage of CLM at the moment is yet rather small and to be improved as the project keeps evolving in future. Second, we develop MathAbs (Mathematical Abstract language). It is a prover independent formal language to represent the semantics of CLM texts preserving its logical and reasoning structure. MathAbs is designed as an intermediate language between CLM and the formal languages of theorem provers, allowing proof checking. Third, we propose a system that can automatically translate CLM to MathAbs, giving a precise semantics to CLM. We consider that formalizing mathematics automatically in such a formal language that has a precise semantics is an important progress even if it can't always be proof-checked. This brings us to the second question for which we report a very limited work. We only translate MathAbs to the first-order formulas. If we feed these formulas to the automated theorem provers (ATPs), then fundamentally the ATPs should be able to validate them sometimes. In other words, the resulting MathAbs document is not completely verifiable for the moment, but it represents an opportunity for the mathematician to write mathematical text (mainly proofs) without becoming expert of any theorem prover. Keywords: Computational linguistics, Controlled languages, Formalization, Formal systems, Verification, Proof checking.