À venir
TBA
À venir
À venir
TBA
Soit $f : (\mathbb{R}^n, 0) \to (\mathbb{R}, 0)$ un germe de fonction définissable de classe $C^2$ et soit $(X,0) \subset (\mathbb{R}^n, 0)$ un germe d'ensemble définissable fermé. On étudie des invariants topologiques associés à $f_{\vert X}$. En particulier, on donne plusieurs formules topologiques pour des caractéristiques d'Euler. On relie aussi la topologie de $f_{\vert X}$ à la topologie d'une fonction définissable avec un point critique stratifié isolé à l'origine.
Travail en commun avec Juan Antonio Moya Pérez (Valencia).
Dans cet exposé, on va étudier des fonctions rationnelles localement bornées. C’est-à-dire, les fonctions rationnelles qui sont bornées au voisinage de chaque point de leur domaine. Ces fonctions ont déjà été étudiées de point de vue algébrique. Cependant, on va les regarder de manière géométrique. On commencera par leur caractérisation. Il existe deux points de vue équivalents de caractériser cette classe de fonctions. Le premier est celui qui vient de la lemme de sélection de courbes. Le deuxième vient de la résolution de singularités. L’observation la plus intéressante ici est que cette classe des fonctions est exactement la classe des fonctions qui peuvent être transformées en fonctions régulières ayant des valeurs dans le corps de définition (on considère ici un corps réel clos). Ensuite, on définira le lieu d’annulation d’une fonction rationnelle localement bornée. Étant donné que ces fonctions sont, en général, multi-valuées, une analyse soigneuse est nécessaire. Enfin on va démontrer une version de l’inégalité de Lojasiewicz pour cette classe de fonctions et qu’il existe, dans le cas de dimension deux une bonne correspondance entre l’algèbre et la géométrie liées à ces fonctions. Cet exposé contient des travaux réalisés en collaboration avec Victor Delage et Goulwen Fichou.
Travail en commun avec Chen Gong. J'expliquerai comment analyser les dégénérescences dynamiques de suites de fractions rationnelles à l'aide de la théorie de Berkovich. L'analyse non-standard joue un rôle clef dans cette approche inspirée de travaux de Yusheng Luo.
Shape optimization is a central field in applied mathematics and engineering, with applications ranging from aerodynamics to material design. The objective is to find the optimal shape of a domain that minimizes a given criterion, such as energy or resistance, while satisfying geometric constraints like fixed volume, surface area, or minimal height. Classically, solving these optimization problems requires numerical methods that rely on shape derivatives and adjoint calculations, which are computationally expensive and difficult to adapt to complex geometries. To overcome these challenges and the inherent limitations in parallelization found in classical approaches, our objective is to find a good methodology that relies on neural networks and benefits on their specific properties (easy parallelization, automatic differentiation, and a meshless approach). This requires suitable representations for both the solution of the state equation and the shape of the domain in which the equation is defined. For this purpose, we introduce the DeepRitz method to approximate solutions to the state equation and symplectic neural networks to model the domain shape effectively. We illustrate this approach through an example: minimizing the Dirichlet energy of a domain under a volume constraint. We will then propose an extention of this work for odd dimensions.
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.