Stability Framework for the Singularity of the Euler Equations on $\mathbb{R}^3$

Résumé Technique : Cadre de Stabilité pour la Singularité des Équations d'Euler sur $\mathbb{R}^3$

Énoncé du Problème
Le papier traite du problème ouvert central en dynamique des fluides : savoir si des données initiales lisses pour les équations d'Euler de l'incompressible en 3D peuvent conduire à la formation d'une singularité en temps fini (blowup). Bien que l'explosion en temps fini ait été établie pour les équations d'Euler avec des bordures ou sous des conditions initiales non lisses, l'existence d'une singularité issue de données lisses sur le domaine non borné $\mathbb{R}^3$ reste non prouvée. Une stratégie courante pour résoudre cela consiste à construire un profil singulier approximatif et à prouver sa stabilité non linéaire. Les auteurs notent que, bien qu'un profil auto-similaire de haute précision ait été découvert dans une étude numérique compagne utilisant des réseaux de neurones informés par la physique (PINNs), une preuve de stabilité rigoureuse pour ce profil sur $\mathbb{R}^3$ n'avait pas encore été établie. Le défi spécifique réside dans l'absence d'une propriété de flux sortant (« outgoing ») globale (qui aide typiquement la stabilité) et la présence de points fixes non triviaux dans le flux méridien qui peuvent provoquer la concentration des perturbations.

Méthodologie
Le papier établit un cadre rigoureux pour prouver la stabilité non linéaire du profil auto-similaire approximatif découvert dans l'étude compagne. La méthodologie procède à travers les étapes suivantes :

1. Représentation du Profil Approximatif : Le profil numériquement découvert via PINN est converti en une représentation par spline polynomiale par morceaux. Cette forme analytique permet une différenciation exacte et une évaluation rigoureuse des résidus et des normes via l'arithmétique d'intervalles (via la bibliothèque Arb), garantissant que les erreurs numériques sont bornées (par exemple, $O(10^{-5})$ en $L^2$).
2. Redimensionnement Dynamique et Linéarisation : Les auteurs emploient une formulation de redimensionnement dynamique où la solution est vue dans un référentiel mobile qui s'étend ou se contracte pour maintenir la singularité à une échelle fixe. Le profil approximatif devient un état stationnaire dans ce référentiel redimensionné. L'analyse de stabilité implique la linéarisation des équations d'Euler redimensionnées autour de cet état stationnaire.
3. Variables Cohérentes en Échelle : Pour gérer les comportements de redimensionnement divergents de la vitesse et de la vorticité, l'analyse est formulée en utilisant des variables de perturbation cohérentes en échelle : la perturbation de la vorticité $\delta\omega$ et le gradient de la perturbation de la vitesse $\nabla \delta u$.
4. Modulation et Normalisation : Le cadre introduit des paramètres de modulation pour fixer la translation et l'amplitude du profil, éliminant ainsi efficacement les directions neutres (modes de symétrie) de l'analyse de stabilité. Cela garantit que la question de stabilité concerne des perturbations authentiques transverses à ces symétries.
5. Estimations d'Énergie Pondérées : Le cœur de la preuve repose sur la construction d'une fonctionnelle d'énergie complète $E_k^2 = E_0^2 + \mu_k H_k^2$, combinant :
   • Énergie pondérée d'ordre bas ($E_0$) : Utilise des fonctions de poids singulières $\Phi_\omega, \Phi_r, \Phi_z$ adaptées au profil pour établir un amortissement linéaire.
   • Énergie pondérée d'ordre élevé ($H_k$) : Utilise des poids d'ordre supérieur pour contrôler les dérivées et les valeurs ponctuelles nécessaires pour fermer les estimations non linéaires.
6. Certification Assistée par Ordinateur : La preuve réduit le problème de stabilité de dimension infinie à un problème d'optimisation de dimension finie. Les auteurs dérivent des estimations analytiques explicites pour l'amortissement linéaire, les interactions non linéaires et les résidus de l'EDP. Ces estimations dépendent d'une large collection de constantes explicites (par exemple, bornes de matrices, constantes d'interpolation, normes d'opérateurs elliptiques). Le cadre nécessite que ces constantes soient rigoureusement certifiées en utilisant l'arithmétique d'intervalles et des bornes de matrices certifiées.
7. Formalisation : Le papier note un effort parallèle (LeanPDE) pour formaliser les dérivations symboliques et les étapes de preuve dans le prouveur de théorèmes Lean, en les connectant aux calculs numériques certifiés.

Contributions Clés

• Cadre de Stabilité : La principale contribution est la construction d'un cadre détaillé et modulaire pour prouver la stabilité non linéaire d'un candidat de profil de blowup auto-similaire pour les équations d'Euler 3D sur $\mathbb{R}^3$.
• Réduction à la Vérification Finie : Les auteurs démontrent que la preuve de stabilité peut être réduite à la certification rigoureuse d'un ensemble fini de constantes et d'estimations explicites. Cela déplace le fardeau de la preuve de l'analyse qualitative vers la vérification quantitative.
• Gestion des Flux Non-Sortants : Le cadre adapte avec succès les techniques de stabilité à un cadre sans propriété de sortie globale, en utilisant une condition locale plus faible pour repousser le flux loin des points fixes et en employant des estimations d'amortissement d'ordre élevé délicates.
• Certification par Splines : L'utilisation de splines polynomiales par morceaux pour représenter le profil numérique permet l'évaluation exacte des résidus de l'EDP et de ses dérivées, une étape nécessaire pour la certification rigoureuse par arithmétique d'intervalles.
• Théorème de Stabilité à Deux Rayons : Le papier fournit un théorème de stabilité généralisé (Théorème 2) qui permet des bornes séparées sur les énergies d'ordre bas et d'ordre élevé, offrant une flexibilité dans le processus de certification.

Résultats
Le papier ne prétend pas avoir achevé la certification numérique finale de toutes les constantes requises pour clore la preuve. Au lieu de cela, il établit l'architecture d'une telle preuve.

• Complétude Théorique : Les auteurs prouvent que si les constantes explicites (marges d'amortissement, bornes non linéaires, normes de résidus) peuvent être certifiées pour satisfaire des inégalités spécifiques (par exemple, $\Lambda_{stab} > 0$), alors le profil redimensionné est non linéairement stable.
• Stabilité Conditionnelle : Sous réserve de la certification rigoureuse de ces constantes, le cadre garantit que le profil redimensionné est stable. De plus, via le mécanisme de redimensionnement dynamique, cette stabilité implique l'existence d'une solution admissible dans les variables physiques originales qui développe une singularité en temps fini.
• Bornes de Résidus : Le papier rapporte que la représentation par spline du profil satisfait les équations du profil stationnaire avec des résidus bornés par $O(10^{-5})$ en $L^2$ et $O(10^{-3})$ en $L^\infty$, comparables aux résultats originaux des PINN.

Signification
Le papier affirme que les principaux obstacles restants pour prouver le blowup en temps fini pour les équations d'Euler 3D avec des données initiales lisses sont désormais computationnels et quantitatifs plutôt que conceptuels. En fournissant un cadre rigoureux qui réduit le problème à une collection finie d'estimations vérifiables, les auteurs soutiennent que le chemin vers une preuve complète est clair. Ce travail représente une étape critique dans le paradigme de la « preuve assistée par ordinateur » pour les EDP, jetant un pont entre la découverte numérique (PINNs) et la preuve mathématique rigoureuse. La signification réside dans la démonstration que la stabilité d'un profil singulier complexe, découvert numériquement, peut être soumise à une analyse systématique et vérifiable, résolvant potentiellement l'un des problèmes du prix du millénaire si les constantes restantes sont certifiées avec succès. Le papier souligne que la structure modulaire de l'argument permet des raffinements ciblés (par exemple, l'affinement d'estimations spécifiques ou l'ajustement des poids) sans altérer le mécanisme de stabilité sous-jacent.