une sous-variété minimale de R^n est une sous-variété qui minimisent le volume riemannien localement autour de chaque point. Trouver des hypersurfaces algébriques minimales dans R^n pour chaque n est un problème ouvert qui a été posé par Hsiang. En 2010, Tkachev a donné une solution partielle à ce problème en montrant que l'hypersurface de n x n matrices réelles de rang n-1 est minimale. Je discuterai la généralisation suivante de ce fait : pour tout m, n et r < min(m,n), la sous-variété de m x n matrices réelles de rang r est minimale. De plus, la sous-variété de n x n matrices antisymétriques de rang 2r < n et la sous-variété de n x n matrices symétriques réelles dont les valeurs propres ont des multiplicités prescrites sont également minimales.
Abstract GSOS is a categorical framework for operational semantics, in which rules are modeled as natural transformations of a certain type. Rule systems that fit the constraints imposed by the framework are guaranteed to have desirable properties, mainly that coalgebraic behavioural equivalence, which roughly corresponds to bisimilarity, is a congruence. While bisimilarity is central in process algebra, it is far from the only notion of process equivalence of interest. However, abstract GSOS is not easily applicable to these other equivalences. This work focuses on the other extremum of the linear time-branching time spectrum (bisimilarity being the finest), namely trace equivalence. We wonder under which assumptions on abstract GSOS laws this notion of equivalence is a congruence. A study of trace equivalence for a concrete instance of abstract GSOS (to labelled transition systems with explicit termination) identifies necessary and sufficient conditions to this end. We then transpose abstract GSOS to Kleisli semantics and investigate how, with conditions on the monad (affineness) and the GSOS law (dubbed linearity and smoothness) inspired by the concrete study, trace equivalence can be shown to be a congruence.
Dans cet exposé, je commencerai par mettre en contexte une série de travaux explorant dans un sens large une méthodologie basée sur des représentations «shallow» de calculs dans Rocq. Je me concentrerai ensuite plus spécifiquement sur un travail récent qui argue que de tels interprètes monadiques construits comme des couches d'interprétation empilées sur la monade libre constituent une manière prometteuse d'implémenter et de vérifier des interprètes abstraits.
L'approche permet des preuves modulaires de la correction des interprètes résultants. Nous fournissons des combinateurs génériques de contrôle de flôt abstraits dont la correction est prouvée une fois pour toute relativement à leur contrepartie concrète. Nous démontrons comment relier des gestionnaires concrets implémentant des effets à des variantes abstraites de ces gestionnaires, en capturant essentiellement la correction habituelle des fonctions de transfert dans le contexte des interprètes monadiques. Enfin, nous fournissons des résultats génériques pour transporter les résultats de correction par interprétation des effets d'état et d'échec.
Nous avons formalisé tous les combinateurs et théories susmentionnés dans Rocq, et démontré leurs avantages en implémentant et en prouvant la correction de deux interprètes abstraits illustratifs pour un langage impératif structuré et un assembleur jouet.
Cette contribution est un travail conjoint avec Sébastien Michelland et Laure Gonnord, et a fait l'objet d'un article à ICFP'24.
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.