Journée Analyse Appliquée Hauts-de-France

mardi 31 mai 2022, 09:00 → 17:00 Europe/Paris

Université de Technologie de Compiègne

Cet événement a pour but de rassembler les différents membres des laboratoires de la Fédération de Recherche Mathématique des Hauts-de-France travaillant sur les thèmes de l'analyse théorique et numérique des EDP lors d'une journée d'exposés scientifiques. Pour la première fois cette journée est organisée à l'Université de Technologie de Compiègne (UTC), son organisation est soutenue financièrement par la Fédération et l'UTC. Durant cette journée nous aurons le plaisir d'écouter les orateurs suivant :

 Tony Lelièvre (CERMICS),

 Frédérique Charles (Paris 6),

 Caterina Calgaro (Université de Lille),

 Vincent Martin (UTC).

Le café d'accueil ainsi que les conférences se dérouleront au rez-de-chaussée du bâtiment du Génie Informatique du Centre d'Innovation de l'UTC.

 

 

Fiche horaires ligne 5

Plan lignes bus.pdf

09:00 Café d'accueil des participants

Vincent Martin: Quelques étapes vers la preuve formelle des éléments finis

La méthode des éléments finis est largement employée pour résoudre de nombreux problèmes issus de la physique, de la biologie... Elle s'enrichit quotidiennement de nouveaux développements à la fois en termes d'applications, de méthodes mathématiques, numériques et de calcul scientifiques. L'un de ses avantages est qu'elle s'appuie sur des fondations mathématiques solides. De nombreux codes de calcul basés sur les éléments finis, libres ou non, sont disponibles. La question se pose à chaque fois de la confiance qu'on peut avoir dans les résultats fournis par ces codes, les sources d'erreur étant nombreuses : erreur de programmation, méthode mathématique incorrecte, convergence incomplète (méthode elle-même, résolution non linéaire ou linéaire), maillage inadapté, accumulation d'erreurs flottantes...

Les physiciens, les mathématiciens et les informaticiens cherchent et donnent des moyens pour augmenter cette confiance : la validation est une étape systématiquement nécessaire, avant tout calcul. Il nous semble qu'au-delà des techniques de validation, un niveau supplémentaire de confiance peut être fourni par la vérification formelle de la méthode des éléments finis, ainsi que d'une bibliothèque, ou tout au moins des pans d'une bibliothèque d'éléments finis.

La preuve formelle a été développée par des chercheurs en informatique pour prouver qu'un programme ou un théorème est correct par rapport à sa spécification. Le théorème est mathématiquement vrai et le programme fait ce qui lui a été spécifié (la spécification du programme doit également être formalisée pour pouvoir dérouler la totalité du processus formel), étant donnés le contexte de départ. Des assistants de preuve, comme Coq, permettent de prouver formellement des théorèmes et des programmes.
L'objet de cet exposé est donc de présenter quelques étapes vers la preuve formelle en Coq de la méthode mathématique des éléments finis, ainsi que de parties de programmes d'éléments finis. Une première expérience avait été menée avec la preuve formelle complète des différences finies 1D pour l'équation des ondes (méthode et programme), incluant une borne de l'erreur due aux calculs en arithmétique flottante.
Pour les éléments finis (EF), nous avons commencé par la preuve formelle en Coq du Théorème de Lax-Milgram et du Lemme de Céa, dans l'objectif de prouver les EF pour le problème de Poisson. On se limitera pour le moment à ce type de problèmes et aux méthodes "classiques" (EF de Lagrange). Dans une seconde étape, nous avons construit formellement en Coq la théorie d'intégration de Lebesgue, afin de mettre en place dans un troisième temps (à venir) les espaces de Sobolev et appliquer le théorème de Lax-Milgram. Quelques résultats préliminaires concernant la définition formelle des éléments finis proprement dits seront présentés.

Frédérique Charles: Modèles cinétiques pour les écoulements gaz-particules

On s'intéresse dans cet exposé à des modèles décrivant l'évolution de particules (telles que des particules solides de poussière ou des goutelettes) dans un gaz raréfié. De nombreux modèles de spray pour les mélanges gaz-particules existent, mais la plupart du temps le gaz (appelé aussi la "phase porteuse" dans les modèles de spray) est décrit par des équations portant sur les grandeurs macroscopiques du fluide. On adopte ici une approche à l'échelle mésoscopique pour décrire le gaz. Je présenterai deux types de modèles destinés à décrire une situation où les particules (correspondant à la phase "dispersée" du spray) sont macroscopiques comparées aux molécules.

Dans la première modélisation que nous considérons, la phase de particules est décrite par une fonction de densité, dont les variables sont le temps, la position, la vitesse, et éventuellement de la température de surface des particules. L'évolution des densités en gaz et en particules est décrite par un couplage de deux équations de type Boltzmann, dont les opérateurs intégraux décrivent l'interaction entre les molécules et les particules. Différents mécanismes collisionnels sont considérés, conduisant à des modèles plus simples à étudier d'un point de vue mathématique, ou plus riches d'un point de vue physique. Une aymptotique de masse faible permet ensuite de dériver un couplage de type Vlasov-Boltzmann, moins coûteux à simuler par méthode particulaire.

Dans une seconde modélisation, le système gaz-particules est cette fois vu comme un gaz évoluant en domaine mouvant. Les particules sont alors traitées individuellement au lieu d'être considérées au niveau mésoscopique comme dans le modèle précédent. Nous montrons l'existence de solutions pour un problème aux limites avec conditions de réflexion diffuse aux bords. Des simulations numériques 2d-2v illustrent l'effet du mouvement des particules sur la densité et la température du gaz.

12:00 Déjeuner

Tony Lelièvre: Analyse spectrale pour la métastabilité des processus stochastiques

La simulation de la matière à l'échelle moléculaire est devenue une des pierres angulaires de la recherche dans de nombreux domaines, notamment en biologie, en sciences des matériaux ou en chimie. Les applications sont très variées: conception de médicaments, étude de l'évolution de défauts dans un réseau crystallin, analyse et optimisation de réactions catalytiques, etc.

Malgré l'augmentation des puissances de calcul, il reste difficile de simuler des systèmes suffisamment gros sur des temps suffisamment longs pour estimer les quantités d'intérêt. En particulier, le temps caractéristique d'une simulation à l'échelle moléculaire est de plusieurs ordres de grandeur inférieur à la durée physique des phénomènes que l'on souhaite étudier. Les mathématiques jouent un rôle fondamental à la fois pour dériver de manière rigoureuse des modèles réduits moins coûteux, et pour analyser et améliorer les algorithmes conçus pour simuler des systèmes moléculaires de manière efficace.

L'objectif de l'exposé sera d'introduire des modèles utilisés en dynamique moléculaire, ainsi que des questions mathématiques soulevées par leur simulation. En particulier, nous présenterons des résultats récents permettant de faire un lien rigoureux entre la dynamique de Langevin ou de Langevin sur-amortie, et des modèles de saut entre conformations moléculaires (modèle de Monte Carlo cinétique). L'analyse mathématique repose sur des outils d'analyse semi-classique, et utilise de manière fondamentale le concept de distribution quasi-stationnaire pour étudier la métastabilité des processus stochastiques. Cette approche permet à la fois de justifier et développer des algorithmes de dynamique moléculaire accélérée, et de donner un fondement rigoureux à l'utilisation des lois d'Eyring-Kramers pour paramétrer les modèles de Monte Carlo cinétiques.

References :
- T. Lelièvre and G. Stoltz, Partial differential equations and stochastic methods in molecular dynamics, Acta Numerica, 25, 2016.
- G. Di Gesù, T. Lelièvre, D. Le Peutrec and B. Nectoux, Jump Markov models and transition state theory: the Quasi-Stationary Distribution approach, Faraday Discussion, 195, 2016.
- G. Di Gesù, T. Lelièvre, D. Le Peutrec et B. Nectoux, Sharp asymptotics of the first exit point density, Annals of PDE, 5(1), 2019.

Caterina Calgaro: A finite volume approximation of the temperature in a low Mach combustion model

Given a specific low-Mach model expressed in velocity, pressure and temperature variables, we
focus our attention on the convergence of a finite volume method to approximate the solution of a
convection-diffusion equation involving a Joule term. In particular:
- we establish a discrete version of a Gagliardo-Nirenberg inequality, to apply it to the analysis
of the numerical scheme,
- we consider a discretization of the Joule term consistent with the non linear diffusion one, in
order to ensure the maximum principle on the solution,
- we prove the convergence of the numerical scheme by compactness arguments.

16:00 Café