Postée il y a 22 heures
--- Description ---
Comment calculer de manière exacte et fiable avec des fonctions spéciales dans les systèmes de calcul formel ? Une stratégie consiste à adopter une approche locale et à représenter systématiquement ces fonctions à l'aide de séries formelles autour d'un point non singulier. Par exemple, la fonction f(z) ≔ exp (sin (z)) est l'unique solution en série du système d'équations f'(z) = c(z) f(z), c'(z) =-s(z), s'(z) = c(z), avec les conditions initiales f(0) = 1, c(0) = 1, s(0) = 0. En supposant ce type de représentation, comment vérifier des égalités telles que s(z)^2 + c(z)^2 = 1 ?
Il est clair qu'il suffit d'avoir un algorithme pour vérifier si une expression donnée représente la fonction nulle. Lorsque toutes les séries formelles sont données comme solutions d'équations différentielles explicites avec des conditions initiales explicites, plusieurs algorithmes ont été proposés pour ce problème de test de nullité. Un premier défi consiste à mettre en œuvre un ou plusieurs de ces algorithmes et à étudier les améliorations possibles.
Un deuxième défi concerne le calcul de la solution générique en série formelle d'un système d'équations différentielles ordinaires si les conditions initiales ne sont pas ou seulement partiellement spécifiées. Cela nécessite une extension de la théorie au cas où les coefficients de la série dépendent de paramètres. Par exemple, en posant δ ≔ z ∂/∂ z, la solution générale de l'équation (δ f)^2 - f δ^2 f = 0 est f = c z^n, où c est une constante arbitraire et n ∈ ℕ un entier non négatif arbitraire.
L'objectif principal de la thèse est de généraliser davantage cette théorie en passant des solutions sous forme de séries formelles ordinaires aux solutions en transséries. Une transsérie est une série formelle généralisée qui peut contenir de manière récursive des exponentielles et des logarithmes. Par exemple, integrale (e^(e^x)) = e^(e^x-x) + e^(e^x-2 x) + 2 e^(e^x-3 x) +⋯ et W(x) ≔ inverse (x*e^x) = log x - log log x + (log log x) / (log x) + ⋯ sont des séries transséries à l'infini x→∞. Les transséries apparaissent naturellement lors de l'étude du comportement asymptotique des solutions aux équations différentielles ordinaires. En fin de compte, nous aimerions avoir des tests de nullité efficaces pour les transséries et des algorithmes pour résoudre des équations différentielles dans le corps des transséries.
--- Méthodologie ---
La thèse débutera par une étude de la littérature existante. Ensuite, des cas de plus en plus difficiles de tests de nullité et de résolution d'équations différentielles seront considérés. En fonction de son profil, le ou la doctorant(e) peut choisir de mettre davantage l'accent sur les aspects théoriques ou pratiques du problème. Les implémentations logicielles pourront être réalisées en C++, Julia, Mathemagix ou un mélange de ces langages et distribuées sous forme de logiciel libre.
Contexte de travail
La thèse sera effectuée au laboratoire LIX (Laboratoire d'Informatique de l'École polytechnique), qui se situe dans le bâtiment Alan Turing, 1, rue Honoré d'Estienne d'Orves, Palaiseau. La thèse sera effectuée dans l'équipe MAX de calcul formel et financée par le project ERC ODELIX. La candidate ou le candidat disposera d'un poste de travail et de moyens pour assister à quelques conférences par an.
Contraintes et risques
Néant.