Ce type de théoreme donne des conditions d'indépendance algébriques de fonctions du type $f_i(t(s))$ avec $f_i$ vérifiants des EDO très particulières et $t(s)$ des séries formelles non constantes ; par exemple :
Thm(Ax) : Pour t dans $(C[[s]]-C)^n$, si $tr.deg C( t_1, ..., t_n , exp(t_1), ... exp(t_n))/C < 1+n$ alors une combinaison Z- linéaire des t_i est constante
Thm(Pila-Tsimerman) : Pour $t$ dans $(C[[s]]-C)^n$, si $tr.deg. C( t_1, ..., t_n , j(t_1), ... j(t_n), ... j''(t_n)/C < 1+3n$ alors il existe $k<l$ et $h$ dans $PGL_2^+(Q)$ tels que $t_k = h(t_l)$.
Nous obtenons une généralisation de ces résultats en terme d'intersection improbable entre une feuille de feuilletage holomorphe (transversalement de Lie) et une sous variété algébrique. L'outil principal est la théorie de Galois des équations différentielles linéaires (Théorie de Picard-Vessiot).
Travail avec D. Blazquez-Sanz, J. Freitag et R. Nagloo
It is commonplace to split a complex, formally verified piece of software (e.g., CompCert) into a formally verified part (e.g. written in Coq/Rocq) and an unverified part (e.g., written in OCaml). There are many pitfalls when doing this (types of values exchanged, assumptions of purity, modeling of pointer equality…). We shall in particular discuss situations where the unverified part submits a result, together with an optional certificate, to a verified checker, and illustrate them with examples from the Verified Polyhedra Library and CompCert- Chamois .
We present the study of the non-linear stability of a class of travelling-wave solutions to the compressible pressureless Navier-Stokes system with a singular viscosity. These solutions encode the effect of congestion by connecting a congested left state to an uncongested right state. By using carefully weighted energy estimates we are able to prove the non-linear stability of viscous shock waves to this system under a small zero integral perturbation, which in particular extends previous results that do not handle the case where the viscosity is singular. This is a joint work with Muhammed Ali Mehmood from Imperial College, London.
Cette présentation vise à introduire un schéma monolithique GD/VF (Galerkin Discontinu/Volumes Finis) préservant les propriétés convexes (principes du maximum, positivité, entropie, ...) pour la résolution des systèmes de lois de conservation sur maillages non-structurés. Il est bien connu que les méthodes Galerkin discontinue (GD) nécessitent une limitation non linéaire pour éviter les oscillations parasites ou les instabilités non linéaires, susceptibles de provoquer l´arrêt anticipé du code de simulation. L'idée principale de ce travail est d'améliorer la robustesse des schémas GD tout en préservant autant que possible leur grande précision et leur résolution de sous-maille. Pour ce faire, une combinaison convexe entre un schéma GD d'ordre élevé et un schéma volumes finis (VF) d'ordre un sera localement effectué, à l'échelle des sous-mailles, où cela sera nécessaire. À cette fin, nous prouverons tout d'abord qu'il est possible de réécrire un schéma GD comme un schéma VF défini sur un sous-maillage, en introduisant des flux numériques spécifiques, qu'on appellera flux reconstruits GD. Le schéma monolithique GD/VF sera alors défini de la manière suivante : à chaque face de chaque sous-cellule seront assignés deux flux, un flux VF d'ordre un et un flux reconstruit d'ordre élevé, qui seront finalement combinés de manière convexe. L'objectif est alors de déterminer, par analyse, les coefficients de combinaison optimaux pour atteindre les propriétés souhaitées (par exemple, positivité, absence d´oscillations, inégalités d´entropie) tout en préservant la grande précision du schéma. Des résultats numériques sur divers types de problèmes hyperboliques seront présentés pour évaluer les performances de la méthode proposée.
Grâce à ce formalisme monolithique, nous tenterons de répondre à certaines questions : est-il possible d'assurer une stabilité entropique ? de quelle stabilité entropique parlons-nous (discrète, semi-discrète, de maille, de sous-maille, pour quelle entropie, ...) ? quels sont les coûts de telles stabilités (en terme de précision ou de perte d'autres propriétés) ? À quel point est-ce essentiel pour les problèmes qui nous intéressent ? Nous présenterons différents résultats numériques pour tenter de partiellement répondre à ces questions
Nous discuterons de certains problèmes en systèmes dynamiques où ces équations apparaissent et nous présenterons une méthode permettant d’obtenir une borne supérieure du nombre de solutions réelles à l’aide d’un algorithme de dérivation-division. Nous montrerons que cet algorithme conduit également à un nouvel ensemble de fonctions de Chebyshev spécifiquement adaptées aux problèmes de dynamique.
Le but de mon exposé est de vous présenter mon thème de recherche, qui était également celui de l'équipe de logique lors de sa création. L'objectif est d'étudier la relation entre les démonstrations mathématiques complètement formalisées et la programmation à l'aide d'un langage fonctionnel très basique.
Plusieurs questions nous intéressent dans ce domaine :
L'exposé sera en français, avec des diapositives en anglais, et ne nécessitera pas de connaissances avancées dans ce domaine.
In this seminar we present a mathematical model to describe the evolution of a city, which is determined by the interaction of two large populations of agents, workers and firms. The map of the city is described by a network with the edges representing at the same time residential areas and communication routes. The two populations compete for space while interacting through the labour market. The resulting model is described by a two population Mean-Field Game system coupled with an Optimal Transport problem. We prove existence and uniqueness of the solution and we provide some numerical tools to develop several numerical simulations. This is a joint work with Fabio Camilli (Sapienza Roma) and Luciano Marzufero (Libera Università di Bolzano).
Solar photovoltaic (PV) systems are complex, dynamic systems influenced by a wide range of environmental and operational factors. Accurately modelling their performance and detecting anomalies require integrating diverse data sources and capturing intricate dependencies. In this talk will present a graph-oriented information fusion framework designed to enhance solar PV performance analysis. The framework begins with the analysis of temperature and irradiance data using graph-based techniques, which are then extended to incorporate additional PV parameters such as module temperature, ambient air temperature, global shortwave and longwave radiation, and power output. By constructing temporal graphs, the framework captures both spatial and temporal dependencies, enabling a holistic understanding of system behaviour under varying conditions. This talk will explain the development of a Temporal Graph Neural Network (TGN) model that leverages these fused data sources for performance prediction and anomaly detection. The TGN model integrates Graph Convolutional Networks (GCNs) and Gated Recurrent Units (GRUs) to simultaneously model spatial and temporal dependencies, offering a robust approach to analyse complex PV system dynamics. The talk will highlight the mathematical foundations of the framework, including network analysis, information fusion, and deep learning, and demonstrate its practical applications in solar PV diagnostics. By combining diverse data sources and advanced graph-based techniques, this framework provides a powerful tool for improving the reliability and efficiency of solar energy systems.
The goal of this talk is to give an overview of two new results in the development of hybrid methods for elliptic and hyperbolic partial differential equations (PDEs). A hybrid method combines classical numerical analysis techniques (finite element method (FEM), discontinuous Galerkin (DG), ...) with tools from machine learning (ML). The first part of this talk is dedicated to a broad presentation of such ML tools, including a common framework to represent PDE approximators, be they classical or ML-based. Then, in a second part, we explain how to use a physics-informed prior to lower the error constant of the FEM while keeping the same order of accuracy. Thanks to the FEM framework applied to elliptic PDEs, we rigorously prove that our correction improves the FEM error constant by a factor depending on the prior quality. If time permits, in a third part, we discuss how to enhance the DG basis with physics-informed priors, to increase the resolution of near-equilibrium solutions to hyperbolic systems of balance laws. Once again, we rigorously prove that the error constant is improved. Numerical illustrations will be present throughout the presentation, to validate our results.
Les circuits arithmétiques sont un modèle de calcul des polynômes multivariés sur un corps $\mathbb{K}$. Des problèmes classiques difficiles sur les circuits sont notamment les questions de calcul de bornes inférieures (quelle est la taille minimale d'un circuit calculant un certain polynôme), de test d'identité (donné un circuit, quelle est la complexité de tester si ce circuit calcule le polynôme identiquement nul) ou de reconstruction (Étant donné un accès oracle à un polynôme $f$ calculé par un certain circuit $C$, peut-on reconstruire un circuit similaire $C'$ calculant $f$). On se penchera sur le dernier problème. La question de la reconstruction est ouverte dans le cas général mais il existe des méthodes de reconstruction pour certaines classes de circuits et notamment pour des sous-familles de profondeur constante.
Les langages graphiques sont des formalismes de plus en plus utilisés dans le contexte de l'informatique quantique. Ils permettent de faire des calculs sans utiliser d'équations, uniquement par des opérations de réécriture de diagrammes. Dans cet exposés, je commencerai par une petite introduction douce au ZW-calcul, inventé en 2010 par Coecke and Kissinger. Je montrerai que ce langage graphique peut être utilisé pour traiter des problème complètement combinatoires (et "classiques"), comme le comptage de couplages parfaits dans des graphes. En utilisant ce formalisme, nous sommes parvenus (avec Titouan Carette, Thomas Perez et Renaud Vilmart) à une nouvelle technique permettant de compter les couplages parfaits d'un graphe planaire en un nombre polynomial d'opérations (un résultat dû à Kasteleyn en 1967 en utilisant la notion d'orientations Pfaffiennes).
Le modèle Euler compressible bifluide ne présente pas de difficultés théoriques supplémentaires comparé au cas monofluide. Mais sa résolution numérique est notoirement plus difficile à cause du phénomène d'oscillations de pression à l'interface entre fluides. Nous présentons une approche basée sur un échantillonnage aléatoire "à la Glimm" à l'interface, qui permet de s'affranchir de ce défaut. Le schéma obtenu est applicable à des maillages non structurés, il a d'excellentes propriétés de robustesse et de convergence. Nous l'appliquons à des cas de déferlement.
Le Voyageur Canadien essaye, dans un graphe pondéré donné, d'aller d'un sommet à un autre. Mais certaines arêtes sont bloquées ; il les découvre en visitant une de leurs extrémités. Une façon d'évaluer la stratégie du voyageur est de chercher à minimiser le ratio entre la distance parcourue et celle qui l'aurait été avec l'information parfaite : c'est le ratio compétitif. Il est connu qu'aucune stratégie ne peut avoir de ratio compétitif meilleur que 2k+1 (où k est le nombre d'arêtes bloquées), même dans les graphes planaires non-pondérés de largeur arborescente 2.
Nous étudions le cas des graphes planaires extérieurs, où nous déterminons une stratégie ayant ratio compétitif 9 dans le cas non-pondéré (ce qui implique un ratio constant lorsque l'écart entre les pondérations est borné). Nous montrons aussi que cette valeur de 9 est une borne inférieure : il existe une famille sur laquelle aucune stratégie ne peut avoir de ratio compétitif 9-epsilon. Enfin, nous montrons que le ratio compétitif ne peut pas être borné dans les graphes planaires extérieurs arbitrairement pondérés.
La conjecture de Yau--Tian--Donaldson (YTD) propose un critère purement algébrique pour détecter l'existence de métriques kählériennes à courbure scalaire constante sur une variété projective. Si elle est résolue dans le cas Fano, sa version générale demeure ouverte à ce jour. Nous fournissons une réponse positive à une conjecture de Tian, vérifiant une étape de son programme visant à résoudre la conjecture de YTD générale. Nous nous appuyons sur des travaux de Paul concernant la stabilité des paires (qui généralise la notion de stabilité au sens de la théorie géométrique des invariants), ainsi que sur la notion d'arc pour une variété projective - dont l'intérêt dans le cadre de cette conjecture a autrefois été suggéré par Donaldson et Wang. Cet exposé se base sur des travaux en commun avec Ruadhai Dervan.
Pendant l'élongation de l’axe de l'embryon de vertébré, on observe, grâce à l’imagerie live, un phénomène de turbulence cellulaire dans les différents tissus embryonnaires. Nous proposons un modèle mécanique en 2D pour modéliser la croissance des tissus pendant l'élongation de l'embryon, qui permet de retrouver ces flux turbulents à travers un rotationnel non trivial pour les vitesses des tissus. Une autre spécificité de ce modèle est que la ségrégation entre les tissus est assurée par une pression de ségrégation. Après avoir déterminé (formellement) la limite incompressible, nous étudions le comportement qualitatif à la limite et discutons d'un effet fantôme.
Plusieurs modèles physiques permettent de comprendre la dynamique des mélanges de fluides, parmi lesquels figurent les modèles dits de Baer-Nunziato. Les équations aux dérivées partielles associées à ces modèles ressemblent à celles de Navier-Stokes, avec, en plus, de nouveaux termes de relaxation.
Une stratégie pour obtenir ces modèles est l'homogénéisation : à partir d'un mélange mésoscopique, où deux fluides purs satisfaisant les équations de Navier-Stokes compressibles se répartissent l'espace, on effectue un changement d'échelle pour obtenir un mélange macroscopique, où, en chaque point de l'espace, les deux fluides peuvent coexister.
Ce problème relève de l'étude des équations de Navier-Stokes avec des données initiales fortement oscillantes. On commencera donc par expliquer certains résultats dans ce cadre de travail, en dimension un d'espace et sur le tore, d'abord pour des fluides barotropes, puis pour des gaz parfaits non barotropes. On détaillera ensuite les différentes étapes de la démonstration de l'homogénéisation.
Un corps de Hardy est un corps différentiel, pour les opérations point par point, de germes à l'infini de fonctions réelles définies sur des voisinages de l'infini. Si son sous-ensemble des germes de fonctions tendant vers l'infini à l'infini est stable par composition et inversion fonctionnelle des germes, alors cet ensemble a une structure de groupe totalement ordonné. Il n'est certes pas commutatif, mais présente des traits commutatifs permettant de simplifier l'étude d'équations et inégalités fonctionnelles, relativement à leur étude dans des groupes ordonnés généraux. Je définirai ces objets et notions, et présenterai des propriétés élémentaires de ces groupes ordonnés de germes. Je montrerai comment résoudre des équations fonctionnelles sur ces groupes dans des extensions qui sont des groupes de séries formelles généralisées, comme les transséries.
La théorie des types observationnelle (OTT) est une extension de la théorie des types dépendants conçue par Altenkirch et McBride dans les années 2000. L'idée centrale d'OTT est qu'en modifiant le concept d'égalité, il devient possible d'avoir des types quotients et des fonctions extensionnelles sans compromettre le caractère constructif de la théorie des types dépendants.
Lors de cet exposé, j'expliquerai comment combiner la théorie observationnelle d'Altenkirch et McBride avec le Calcul des Constructions, la théorie des types qui sous-tend l'assistant à la preuve Coq. En particulier, j'expliquerai comment caractériser l'égalité des types inductifs de Coq, et comment les éliminateurs des types indexés utilisent une règle de calcul délicate à intégrer à la théorie.
Si le temps le permet, j'en profiterai pour faire une démonstration de la branche expérimentale Coq-observationnel, et pour discuter d'avancées récentes dans la sémantique ensembliste de la théorie des types observationnelle.
Les compactifications équivariantes de groupes, comme les variétés toriques ou les compactifications d’espaces vectoriels, sont des familles-tests régulièrement mises à contribution dans l’étude de la répartition des points rationnels sur les variétés algébriques (conjecture de Manin-Peyre).
Notamment, à la fin des années 90, l’emploi d’outils d'analyse harmonique a permis à Victor Batyrev et Yuri Tschinkel d’établir une formule asymptotique pour le nombre de points rationnels de hauteur anticanonique bornée sur une variété torique, en faisant un usage clef d’une formule de Poisson adélique. Puis, au début des années 2000, ce résultat a été étendu aux corps de fonction de charactérique positive par David Bourqui. Un peu plus tard encore, une approche similaire a permis à Antoine Chambert-Loir et Yuri Tschinkel de traiter le cas des compactifications équivariantes d’espaces vectoriels sur un corps de nombres.
Ces dix dernières années, une version motivique additive de ces outils et résultats pour les compactifications d’espaces vectoriel a été développée successivement par Antoine Chambert-Loir et François Loeser puis Margaret Bilu, ce qui a servi de base à la formulation d’un principe de Manin-Peyre dans une version motivique.
L’objet de cet exposé est le fruit d'un travail en collaboration avec Margaret Bilu dans lequel nous développons une version motivique multiplicative de cette approche, laquelle nous permet de démontrer un phénomène de stabilisation motivique dans l’espace de module des morphismes d’une courbe lisse projective complexe quelconque vers une variété torique.