Barlet Daniel
email: barlet@iecn.u-nancy.fr

1 Introduction.

Le but de cet article est de montrer que les résultats obtenus dans [B.06] s'étendent au cas général d'un germe de fonction holomorphe à l'origine de C n+1 ayant un lieu singulier de dimension 1. On obtient dans ce cadre "général" le résultat suivant, qui généralise les points cruciaux des théorèmes 4. Les théorèmes 5.2.1, 6.2.1. et 6.4.1. de [B.06] qui sont l'essentiel des résultats de cet article se généralisent immédiatement à partir de ce théorème, puisqu'ils n'utilisent l'hypothèse (HH) faite dans [B.06] que pour obtenir ces propriétés des faisceaux de cohomologie du complexe K. Ceci complète donc le "programme" mis en place dans [B.06]. La démonstration du théorème 1.1.1 utilise l'étude de la situation suivante, qui présente un intérêt en elle-même, puisqu'elle relie l'étude d'une famille à un paramètre de fonctions à singularités isolées avec l'étude du "graphe" correspondant, qui est une fonction à lieu singulier de dimension 1. Le lemme suivant permet d'introduire cette situation pour un germe arbitraire de fonction holomorphe à l'origine de C n+1 admettant un lieu singulier de dimension 1. Proposition 1.1.4 Dans la situation de la proposition précédente, il existe un morphisme "naturel" de faisceaux ∇ : E → E vérifiant les propriétés suivantes :

1. Pour ϕ ∈ O D * et x ∈ E on a ∇(ϕ.x) = dϕ dt .b.x + ϕ.∇(x).

Soit

P := {x ∈ E / ∇(x) ∈ b.E}. Alors b -1 .∇ : P → E est une O D * -connexion qui commute à a et b.
3. On a des isomorphismes "naturels" compatibles à a et b :

Ker ∇ ≃ l * (H n ) et E b -1 .∇(P) ≃ l * (H n+1 ). 4. Il existe un sous-O D * [[b]]-module cohérent localement libre G de E vérifiant i) E/G est un O D * -module localement libre. ii) G est stable par a et b -1 .∇. iii) On a G ≃ Ker ∇ ⊗ O D * .
Le théorème 1.1.1 est alors une conséquence simple des propositions 1.1.3 et 1.1.4.

Nous compléterons ce résultat en donnant un critère suffisant permettant "d'estimer concrètement" le sous-module G dont l'existence est montrée dans la proposition 1.1.4 (mais par une méthode fort peu constructive). Nous illustrerons ce critère sur des exemples simples.

Nous conclurons cet article en décrivant le lien entre la connexion b -1 .∇ et les intégrales "à la Malgrange" .

2 La b -1 ∇-régularité.

2.1 Le théorème de b -1 ∇-régularité.

[[b]]-module Ĝ de E[b -1 ] qui est O D [[b]]-cohérent et stable par b -1 ∇.
Remarques. Il vérifie de plus les propriétés suivantes :

1. On a G = {x ∈ E / ∀ν ∈ N ∇ ν (x) ∈ b ν .E}. 2. Si x ∈ E vérifie b -1 ∇(x) ∈ G + O D [[b]].x alors x ∈ G.
En particulier on a Ker∇ ⊂ G.

Si des germes

ϕ ∈ O D \ {0} et x ∈ E sont tels que ϕ.x ∈ G alors x ∈ G. 4. Si des germes ϕ ∈ O D \ {0} et x ∈ G sont tels que ϕ.x ∈ b.G alors x ∈ b.G. Supposons maintenant que E soit b -1 ∇-régulier sur S * . Alors G est O D [[b]]
localement libre de rang fini sur S * et il est stable par a. De plus il vérifie les deux propriétés suivantes:

i) Le sous-faisceau Ker ∇ est localement constant sur S * , de fibre un (a,b)module régulier géométrique.

ii) Sur tout ouvert simplement connexe U ⊂ S * , on a un isomorphisme

Γ(U, G) ≃ Γ(U, Ker ∇) ⊗ C O S * (U ).
Remarque. Comme l'application t : S * → D * est un revêtement holomorphe fini, on pourra identifier S * et D * dans les considérations locales.

Preuve. 1. On a sur U les relations

Notons G k := {x ∈ E / ∀ν ∈ [0, k] ∇ ν (x) ∈ b ν .E}, pour k ∈ N. On a donc G = ∩ k≥0 G k . Pour montrer que G est un O D -module, il suffit de voir que c'est le cas pour chaque G k . Mais pour ϕ ∈ O D et x ∈ E on a ∇ ν (ϕ.x) = ν j=0 C j ν .ϕ (j) .b j .∇ ν-j (x) (@) ce qui montre que si x ∈ G k on aura ϕ.x ∈ G k . La somme de sous-O D [[b]]-modules stables par b -1 ∇ est encore stable par b -1 ∇. Donc il existe bien un plus grand sous-O D [[b]]-module Γ de E, stable par b -1 ∇. L'inclusion de tout sous-O D [[b]]-module stable par b -1 ∇ dans G est immédiate. Pour prouver 1), c'est à dire l'égalité G = Γ il suffit donc de montrer que G est stable par b -1 ∇. Or ∇(G k ) = {∇(x) /x ∈ G k } ⊂ {y ∈ E / ∇ ν (y) ∈ b ν+1 E ∀ν ∈ [0, k -1]} et {y ∈ E / ∇ ν (y) ∈ b ν+1 E ∀ν ∈ [0, k -1]} est contenu dans {bz / z ∈ E / ∇ ν (z) ∈ b ν .E ∀ν ∈ [0, k -1]} ⊂ b.G k-1 . On a donc bien ∇(G) ⊂ b.G. Si x ∈ E vérifie b -1 ∇(x) ∈ G + O D [[b]].x considérons G := O D [[b]].x + G. On a alors , pour y ∈ G, ∇(α.x + y) = α ′ .bx + α.∇(x) + b.G ⊂ b.(O D [[b]].x + G) où α ′ désigne la dérivée et t de α ∈ O D [[b]]. Ceci montre que G = G et donc que x ∈ G. Si maintenant on a ϕ.x ∈ G avec ϕ ∈ O D \ {0} et x ∈ E
: U → U p := t -1 (t(p)) ∩ U donnant le diagramme commutatif U f ×t Φ×t / / U p × ∆ f ×Id D × ∆ = / / D × ∆ où (Φ × t) est un homéomorphisme et U p une boule de Milnor en p pour la restriction f p de f à t = t -1 (t(p)).
dω j = (m + u) df f ∧ ω j + df f ∧ ω j-1 ∀j ∈ [1, k] avec la convention ω 0 ≡ 0.

L'espace vectoriel engendré par les classes de cohomologie induites sur

{f = ε} ∩ U par les ω j est égal au sous-espace vectoriel engendré par

e 1 , • • • , e k de H n-1 ({f = ε} ∩ U, C).
Dans ces conditions le sous-faisceau de Ker ∇ |∆ engendré par

[dω 1 ], • • • , [dω k ] est libre de rang k sur C[[b]], et il est stable par a. Sa fibre est le (a,b)-module à pôle simple de rang k de C[[b]]-base ε 1 , • • • , ε k avec a.ε j = (m + u).b.ε j + b.ε j-1 avec la convention ε 0 = 0. Le sous-faisceau de O ∆ [[b]]-module engendré par [dω 1 ], • • • , [dω k ] est

Estimation de G.

Commençons par remarquer que l'on a, localement sur S * , équivalence entre l'égalité G = E et l'appartenance de ∂f ∂t à J / (f ), l'idéal jacobien relatif de f . En effet, dès que ∂f ∂t ∈ J / (f ), on a dx ∈ P et donc, à fortiori dx ∈ G. On notera que ∂f ∂t ∈ J / (f ) n'a lieu quand la déformation de la singularité donnée par t → f t est localement triviale.

Proposition 2.2.1 Notons M k , pour k ≥ 1, l'image de M k . Ωn / dans E, où M désigne l'idéal de O X engendré par x 1 , • • • , x n . Supposons qu'il existe un entier k tel que M k . ∂f ∂t ⊂ M k+1 .J / (f ). (*) Alors le plus grand sous-O D [[b]]-module (cohérent) G de E, stable par a et b -1 ∇ contient M k .
Preuve. Nous allons montrer que sous notre hypothèse

G := M k est stable par a et b et il vérifie ∇(G) ⊂ b.G.
La stabilité par a est évidente. Pour montrer la stabilité par b, nous allons montrer que b.G est l'image dans E de M k+1 .J / (f ).Ω n / , ce qui implique en particulier la stabilité par b.

Si ω = d / ξ avec ω ∈ M k .Ω n / , on peut choisir ξ ∈ M k+1 .Ω n-1 / . On aura alors b[ω] = [d / f ∧ ξ] qui est bien dans M k+1 .J / (f ).Ω n / . Réciproquement, si η ∈ M k+1 .J / (f ).Ω n / on peut écrire η = d / f ∧ ξ avec ξ ∈ M k+1 .Ω n-1 / . Alors d / ξ ∈ M k .Ω n / et
∇(ω) = d / f ∧ ∂ξ ∂t - ∂f ∂t .ω. Comme pour [ω] ∈ G on peut choisir ξ et donc ∂ξ ∂t ∈ M k+1 .Ω n-1 / , on a, grâce à l'inclusion (*), ∇(ω) ∈ M k+1 .J / (f ).Ω n / ⊂ b.G.
Il n'est pas difficile de montrer directement que, dans la situation de la proposition précédente, G est un sous-O D [[b]]-module cohérent de E qui contient localement b N .E pour N ≫ 1. On a ainsi une preuve directe de la b -1 ∇ régularité dans ce cas.

Exemples.

Exemple 1. On se propose d'étudier le cas où f (t, x) = P (x) + t.Q(x) avec P et Q deux germes de fonctions holomorphes à l'origine de C n .

Lemme 2.3.1 Supposons P à singularité isolée à l'origine et supposons que l'on ait M k+1 .J(Q) ⊂ M k+1 .J(P ) pour un entier k ≥ 0, où M désigne l'idéal maximal de l'origine dans C n . Alors on a M k+1 .J / (f ) = M k+1 .J(P ) où M désigne l'déal engendré par M dans O C n+1 . Si on a de plus Q ∈ M.J(Q), ce qui est vérifié en particulier si Q est quasi homogène, on obtiendra l'inclusion M k . ∂f ∂t ⊂ M k+1 .J / (f ) et la proposition précédente donnera que M k ⊂ G sur S = {t = 0} au voisinage de l'origine.

Preuve. L'hypothèse permet donc d'écrire chaque x α . ∂Q ∂x j pour α ∈ N n , vérifiant |α| = k + 1, comme combinaison linéaire à coefficients holomorphes des x β . ∂P ∂x i . Si γ désigne le vecteur colonne des x α . ∂P ∂x j et δ le vecteur colonne des x α . ∂Q ∂x j on aura donc δ = R.γ où R est une matrice à coefficients holomorphes dans C n . Comme les x α . ∂P ∂x j +t. ∂Q ∂x j forment un système générateur sur O C n+1 de M k+1 .J / (f ), on aura une relation matricielle Γ = (Id + t.R).γ où Γ désigne le vecteur colonne des x α . ∂P ∂x j + t. ∂Q ∂x j . Pour |t| ≪ 1 la matrice Id + t.R sera inversible et on a ainsi établi l'égalité M k+1 .J / (f ) = M k+1 .J(P ) au voisinage de l'origine dans C n+1 . Cette égalité montre que le lieu singulier de f est contenu dans S au voisinage de l'origine, et si Q(0) = 0, ce qui est imposé par l'appartenance de Q à M.J(Q), on aura égalité. On conclut immédiatement car

Q ∈ J / (f ) implique Q ∈ J(P ).
Illustrons ceci par un exemple simple "explicite".

Exemple 2. Il s'agit de calculer l'exemple suivant dans lequel on a n = 2 : P (x, y) = x 4 + y 4 , Q(x, y) = x 2 .y 2 et donc f (x, y, t) = P (x, y) + t.Q(x, y) qui est une déformation à µ-constant pour t = ±2, d'hypersurfaces à singularités isolées de C 2 dont le faisceau des modules de Brieskorn n'est pas localement constant. En effet le birapport des quatre droites de C 2 que l'on obtient pour chaque valeur de t et qui vaut 6 -t-2 4 est une fonction localement injective, ce qui montrent que ces germes de fonctions holomorphes ne sont jamais localement deux à deux analytiquement équivalentes.

6 Il s'agit de calculer le birapport des quatre racines de l'équation z 4 + t.z 2 + 1 = 0. Ce nombre est défini modulo le groupe du birapport. Par exemple 1 -(-t-2 4 ) = t+2 4 représente la même classe de birapport.

Cependant l'hypothèse M 2 .J(Q) ⊂ M 2 .J(P ) du lemme précédent est satisfaite, où ici, on a simplement M := (x, y). On vérifie aussi immédiatement que Q ∈ J(P ). On aura donc G = M.

Explicitons le calcul de ∇. On a

∂f ∂x = 4x 3 + 2t.xy 2 ∂f ∂y = 4y 3 + 2t.x 2 y. et donc 8.x 3 y = 2y ∂f ∂x -tx.( ∂f ∂y -2t.x 2 y) = 2t 2 .x 3 y + 2y ∂f ∂x -tx. ∂f ∂y . On obtient ainsi 2(4 -t 2 ).x 3 y = 2y ∂f ∂x -tx. ∂f ∂y ∈ J / (f ) et (1) 2(4 -t 2 ).xy 3 = 2x ∂f ∂y -ty. ∂f ∂x ∈ J / (f ) par symetrie. (2)
On en déduit que

4.x 5 = x 2 . ∂f ∂x -2t.x 3 y 2 ∈∈ J / (f ) et (3) 4.y 5 = y 2 . ∂f ∂y -2t.x 2 y 3 ∈ J / (f ) par symetrie. (4)
Grâce aux relations

4.x 4 = -2t.x 2 y 2 + x. ∂f ∂x (5) 4.y 4 = -2t.x 2 y 2 + y. ∂f ∂y (6) une O D [[b]]-base de E est donc donnée par
(1, x, y, x 2 , y 2 , xy, x 2 y, xy 2 , x 2 y 2 ).dx ∧ dy.

Soit ω := x.dy -y.dx. Pour un monôme m homogène de degré δ(m) on a

d / (m.ω) = δ(m) + 2 4 . d / f f ∧ m.ω (7)
ce qui donne

a(m) = δ(m) + 2 4 .b(m). (8)
On a également

∇(d(m.ω)) = d / f ∧ ∂(m.ω) ∂t -x 2 y 2 .d(m.ω) (9) et donc ∇(m) = -x 2 y 2 .m. (10) Comme x 2 y 2 .M ⊂ J / (f ), on voit que b -1 ∇ opère sur G = M. Par exemple, comme 2(4 -t 2 ).x 3 y 2 = 2y 2 ∂f ∂x -txy. ∂f ∂y (11) = d / f ∧ (2y 2 dy + t.xydx) (12) on aura b -1 ∇(x) = t.x 2(4 -t 2 )
.

Donc (4 t 2 ) 1 4 .x sera (localement) dans Ker ∇ pour |t| < 2. Comme ∇(1) = -x 2 y 2 / ∈ b.E, pour tester directement la b -1 ∇-régularité de E, posons E 1 := E ⊕ O D .ε, où l'on définit ε := b -1 (x 2 y 2 ). Alors on obtient, puisque a(x 2 y 2 ) = 3 2 b(x 2 y 2 ) les relations suivantes : aε = 1 2 .bε et ∇ε = b -1 ∇(x 2 y 2 ) = b -1 (-x 4 y 4 ).
Explicitons b -1 (-x 4 y 4 ). On a d'après (1) 2(4 -t 2 ).x 4 y 4 = d / f ∧ (2xy 4 dy + t.x 2 y 3 dx) (13) ce qui donne 2(4 -t 2 ).x 4 y 4 = b(2y 4 -3t.x 2 y 2 ) et donc d'après ( 6)

2(4 -t 2 ).x 4 y 4 = b(-4t.x 2 y 2 + d / f ∧ (- 1 2 y.dx)) = b(-4t.x 2 y 2 + 1 2 .b(1)). On a donc b -1 ∇(ε) = 2t 4 -t 2 .ε - 1 4(4 -t 2 )
.1.

Ceci permet de conclure que

E 1 est stable par b -1 ∇. On obtient ainsi directement la b -1 ∇-régularité pour E dans cet exemple. Le O D [[b]]-module O D [[b]].1⊕O D [[b]].ε est stable par a et b -1 ∇, via les formules: a.ε = 1 2 .bε, a.1 = 1 2 .b.1 b -1 ∇(1) = -ε, b -1 ∇(ε) = 2t 4 -t 2 .ε - 1 4(4 -t 2 )
.1.

Exemple 3. Soient p, q, r trois entiers ≥ 3 tels que 1 p + 1 q + 1 r < 1 et posons f (x, y, z, t) = x p + y q + z r + txyz.

Remarquons que l'on a f ∈ M 3 et donc J / (f ) ⊂ M 2 . Montrons que, sur l'ouvert S * := {t = 0} de C, les hypothèses de la proposition 2.2.1 sont vérifiées avec k = 1. D'abord on a J / (f ) = (p.x p-1 + t.yz, q.y q-1 + t.xz, r.z r-1 + t.xy).

Les relations ∂f ∂x = p.x p-1 + t.yz ∂f ∂y = q.y q-1 + t.xz ∂f ∂z = r.z r-1 + t.xy donnent pq.x p-1 .y q-1 = t 2 .xyz 2 + M 2 .J / (f ) ainsi que t.x p-1 .y q-1 = -r.z r-1 .x p-2 y q-2 + M 2 .J / (f ) puisque x p-2 y q-2 ∈ M 2 . On a donc t 3 .xyz 2 + pqr.z r-1 .x p-2 y q-2 + M 2 .J / (f ) ou encore, puisque p, q, r, sont au moins égaux à 3 et t = 0,

t 3 .xyz 2 (1 + pqr t 3 .z r-3 x p-3 y q-3 ) ∈ M 2 .J / (f ). (@)
On aura aussi t.x p y = -r.x p-1 z r-1 + x p-1 . ∂f ∂z t 2 .x p y = -r.t.x p-1 z r-1 + M 2 .J / (f ) = rq.y q-1 .x p-2 .z r-2 + M 2 .J / (f ) = rq.y 2 .x.z.(y q-3 .x p-3 .z r-3 ) + M 2 .J / (f ) ∈ M 2 .J / (f ) d'après (*). On a donc, en utilisant encore le fait que x, y, z jouent le même rôle, que

M. ∂f ∂t ⊂ M 2 .J / (f ) ainsi que M.f ⊂ M 2 .J / (f ).
Il nous reste seulement à voir que ∂f ∂t .h ∈ J / (f ) implique h ∈ M; ceci résulte du fait que ∂f ∂t ∈ J / (f ) . Preuve. Comme on a p.x p = q.y q = r.z r = -t.α modulo M.J / (f ),

on aura f -(1 -ρ).tα ∈ M.J / (f ) avec ρ = 1 p + 1 q + 1 r . ( 14
)
On en déduit en particulier que a.α ∈ M 2 .J / (f ) et donc que ab -1 α est bien dans Γ. La stabilité par b -1 a en découle alors puisque la relation

M.f ⊂ M 2 .J / (f ) donne a.G ⊂ M 2 .J / (f ) ⊂ b.G.
Remarques.

1. Le cas p = q = r = 3 relève du premier exemple traité plus haut. 3 Intégration "à la Malgrange".

Les cas

3.1

Lemme 3.1.1 Soit n un entier au moins égal à 2. On a un morphisme de complexes

• • • / / ( Ker df ) n-1 d / / ( Ker df ) n d / / α ( Ker df ) n+1 / / β 0 • • • / / 0 / / P b -1 ∇ / / E / / 0
où α est induite par la projection "évidente" de Ωn sur Ωn / et où β est l'inverse de l'isomorphisme ∧dt : Ωn / → Ωn+1 . Il induit des isomorphismes (a,b)-linéaires sur les faisceaux de cohomologie, si on remplace ( Ker df ) 0 par ( Ker df ) 1 ∩ Ker d en degré 0 dans le premier complexe (avec l'inclusion évidente).

Preuve. Vérifions déjà les égalités

α • d = 0 et β • d = b -1 ∇ • α. Si u + dt ∧ v est dans ( Ker df ) n-1 avec u ∈ Ωn-1 / et v ∈ Ωn-2 / , on aura d / f ∧ u = 0 et (α • d)(u + dt ∧ v) = d / u. On trouve donc bien zéro dans P ⊂ E. Pour d / ξ + dt ∧ η ∈ ( Ker df ) n on aura (β • d)(d / ξ + dt ∧ η) = β(dt ∧ ( ∂d / ξ ∂t -d / η)) = ∂d / ξ ∂t -d / η = d / ( ∂ξ ∂t -η). La condition df ∧ (d / ξ + dt ∧ η) = 0 donne ∂f ∂t .d / ξ = d / f ∧ η et on a donc ∇(α(d / ξ + dt ∧ η)) = ∇(d / ξ) = d / f ∧ ( ∂ξ ∂t -η)
ce qui donne bien l'égalité désirée. La fin de la preuve consiste alors à vérifier que les morphismes induits en cohomologie coïncident avec ceux des propositions 4.

  3.1 et 4.3.2 de [B.06]. Théorème 1.1.1 Soit f un germe de fonction holomorphe à l'origine de C n+1 et notons par K := ( Ker df • , d • ) le complexe obtenu par complétion formelle le long de Y := {f = 0} à partir du sous-complexe du complexe de de Rham des formes holomorphes sur C n+1 annulées par ∧df . Les faisceaux de cohomologie du complexe K vérifient les propriétés suivantes : 1. Le faisceau H 1 est de support Y et isomorphe à C Y ⊗E 1 où le (a,b)-module E 1 est défini par E 1 := C[[b]].e 1 et a.e 1 = b.e 1 1 2. Le faisceau H n est à support dans S. C'est un système local sur S * := S\{0} de (a,b)-modules réguliers géométriques 2 . De plus ce faisceau n'a pas de section non nulle supportée par l'origine et n'a pas de b-torsion. Sa fibre à l'origine est donc également un (a,b)-module régulier géométrique. 3. Le faisceau H n+1 est à support dans S. Il vérifie la propriété du prolongement analytique 3 sur S * . L'espace vectoriel H 0 {0} (S, H n+1 ) est, modulo un sous-module de b-torsion de dimension finie sur C, un (a,b)-module régulier géométrique. 4. Les autres faisceaux de cohomologie du complexe K sont nuls. 1 Il s'identifie à C[[z]] avec a := ×z et b := z 0 .

  Lemme 1.1.2 Soit f un germe de fonction holomorphe à l'origine de C n+1 dont le lieu singulier S est de dimension 1. Pour l ∈ (C n+1 ) * générique, le lieu critique Σ du germe d'application (f, l) : (C n+1 , 0) → (C 2 , 0) est de dimension 1 et contient S; on a donc l'égalité Σ = S au voisinage de S * . De plus la restriction de l à Σ est propre et finie avec un unique point de ramification à l'origine. La famille (f t ) t∈D où f t := f |{l=t} et où D est un disque ouvert centré à l'origine dans C assez petit, est sur D * une famille à µ-constant le long de S * . Dans la situation du lemme précédent, on fixera un voisinage ouvert V de S * dans C n+1 de sorte que Σ ∩ V = S * et on notera par E le complexe image directe par la restriction de l à V du complexe ( Ω• / , d • / ) où Ω• / désigne le complété formel "en f " du faisceau des formes l-relatives sur C n+1 et où d • / est la différentielle l-relative correspondante. On a alors les résultats suivants. Proposition 1.1.3 Dans la situation précisée ci-dessus le seul faisceau de cohomologie non nul en degré = 1 du complexe E est celui de degré n que l'on notera E. C'est un faisceau cohérent localement libre sur le faisceau (cohérent) de C-algèbres O D * [[b]]. Il est naturellement muni d'un morphisme de faisceau O D * -linéaire a vérifiant a.b -b.a = b 2 et continu pour la topologie b-adique. Chaque fibre de E est ainsi munie d'une structure de (a,b)-module régulier géométrique. Le faisceau de cohomologie en degré 1 est le O D * [[b]]-module libre de rang 1 engendré par la classe e 1 := [d / f ] qui vérifie a.e 1 = b.e 1 .

1.

  Comme b est injective sur E, il s'injecte dans E[b -1 ]. 2. Comme Ĝ est cohérent sur O D [[b]] il existe N ∈ N tel que Ĝ soit contenu dans b -N .E. On en déduit alors l'existence localement sur D * d'un sous-O D [[b]]-module cohérent G := b N . Ĝ de E, stable par b -1 ∇ et contenant b N .E. Il est facile de voir que, réciproquement l'existence d'un tel G donne la b -1 ∇-régularité. Proposition 2.1.2 Il existe sur D un plus grand sous-O D [[b]]-module G de E, stable par b -1 ∇.

  montrons par récurrence sur ν ∈ N que l'on a ∇ ν (x) ∈ b ν .E. La propriété étant claire pour ν = 0 supposons-la vraie pour ν -1 et montrons-la pour ν. Comme on a la relation (@) on déduit de l'hypothèse ϕ.x ∈ G et de l'hypothèse de récurrence que ϕ.∇ ν (x) ∈ b ν .E. Mais sur D * le faisceau E/b ν .E est localement O D -libre 4 on en déduit que ∇ ν (x) ∈ b ν .E. On en conclut que x ∈ G, ce qui achève la preuve du point 3). Le point 4) se montre de la même façon en utilisant l'égalité (essentiellement établie plus haut) b.G = {x ∈ E / ∀ν ∈ N ∇ ν (x) ∈ b ν+1 .E}. Supposons maintenant que E est b -1 ∇-régulier. Alors le faisceau G est O D [[b]]-cohérent : en effet si G désigne le plus grand sous-faisceau O D [[b]]-cohérent stable par b -1 ∇ (un tel G existe et il est cohérent car toute suite croissante de sous-O D [[b]]-modules cohérents de E est localement stationnaire) on a G ⊂ G.

4

  car c'est le cas pour ν = 1 et donc pour tout ν en raisonnant par récurrence sur la suite exacte 0 → b k .E b k+1 .E → E b k+1 .E → E b k .E → 0. puisque b k : E b.E → b k .E b k+1 .E est un isomorphisme de faisceaux de O D -modules. De plus, s'il existe x ∈ G \ G, la considération de O D [[b]].x + G contredit la maximalité de G. On a donc G = G. Mais l'absence de O D -torsion de G b.G prouvée au 4) précédent, montre que le faisceau G est O D -localement libre de rang fini sur D * . Les assertions i) et ii) sont alors des conséquences simples du théorème de Cauchy, en utilisant le fait que l'on sait à priori que Ker ∇ ≃ Ĥn a des fibres qui sont des (a,b)-modules réguliers géométriques, en tant que sous-(a,b)-modules de (a,b)modules réguliers géométriques (voir [B.06]).

  Proposition 2.1.4 Dans la situation ci-dessus considérons une base de Jordan e 1 , • • • , e k d'un bloc de Jordan de la monodromie de f pour la valeur propre exp(2iπ.u) où u ∈ [0, 1[, agissant sur H n-1 ({f = ε} ∩ U, C). Alors il existe un entier m ≥ 0 et des (n -1)-formes holomorphes ω 1 , • • • , ω k sur U vérifiant les propriétés suivantes:

  stable par a et libre de rang k sur O ∆ [[b]]. Il est contenu dans G. De plus, pour deux blocs de Jordan distincts, les sous-faisceaux de O ∆ [[b]]-modules ainsi obtenus sont en somme directe dans G.On remarquera que grâce à notre trivialisation locale, pour chaque p ′ ∈ ∆, les restrictions de la base e 1 , • • • , e k à {f p ′ = ε} induiront une base de Jordan d'un bloc de Jordan de taille k pour la monodromie de f p ′ agissant sur H n-1 ({f p ′ = ε}, C).Preuve. L'existence de l'entier m et des (n -1)-formes holomorphes vérifiant les propriétés 1) et 2) résultede [B.84]. Les sections sur l'ouvert ∆ du faisceau Ĥn induites par les formes dω j vérifient les relations :a.[dω j ] = (m + u).b.[dω j ] + b.[dω j-1 ] ∀j ∈ [1, k]qui ne sont qu'une réécriture des relations du 1). Montrons l'indépendance sur C[[b]]. Si on a une relation sur un ouvert connexe ∆ ′ ⊂ ∆ k j=1 s j .[dω j ] ∈ d(Γ(∆ ′ , Ker df )) où s j ∈ C[[b]], on obtient une relation sur C[[f ]] des classes correspondantes, ce qui donne la nullité des coefficients, puisque que ces classes sont indépendantes dans le système de Gauss-Manin localisé en f et donc aussi dans le réseau holomorphe puisqu'il est sans torsion 5 . On en déduit la même propriété pour son complété formel en f par platitude de C[[f ]] sur C{f }. L'indépendance sur O ∆ [[b]] s'en déduit en raisonnant pour chaque t ∈ ∆ fixé, grâce à la remarque qui suit l'énoncé de cette proposition. L'inclusion dans G est immédiate puisque les [dω j ] sont dans Ker ∇. L'indépendance pour des bases de blocs de Jordan distincts (et aussi pour une base de Jordan complète) s'obtient de façon analogue. Démonstration du théorème. Compte tenu de la proposition précédente, il nous suffit de montrer qu'il existe localement sur S * un entier N tel que le O ∆ [[b]]-module G ⊂ G construit à partir d'une base de Jordan de la monodromie de f agissant sur l'espace vectoriel H n-1 ({f = ε} ∩ U, C) tel que l'on ait b N .E ⊂ G. Ceci résulte immédiatement du fait que le réseau du système de Gauss-Manin engendré par les formes holomorphes construites à partir de la base de Jordan considérée est méromorphiquement équivalent au réseau engendré par les formes méromorphes de la forme dω/df avec dω ∈ Ker df ∩ Ker d, où ω est holomorphe. Ceci fournit (localement) l'entier N cherché. D'où la b -1 ∇-régularité de E.

  donne un élement [d / ξ] ∈ G dont l'image par b est [η]. Ceci prouve notre assertion. On a alors, pour ω = d / ξ,

  Notons par G := M.Ω n / d / f ∧ d / Ω n-2 / . Comme le fibré vectoriel sur S * défini par E b.E est trivial, on constate facilement que le O S [[b]]-module Γ := G + O S [[b]].b -1 α de E[b -1 ] où α := xyz, est stable par a, b, b -1 ∇ et b -1 a sur S * .

<

  Preuve. Soit ∆ ⊂ H × C un polydisque. L'hypothèse de trivialité topologique permet de trouver ψ ∈ C ∞,n-1 c/f (f -1 (∆)) une (n -1)-forme d-fermée induisant pour chaque (s, t) ∈ ∆ la classe définie par γ s,t dansH n-1 c (f -1 t (s), C) ≃ H n-1 (f -1 t (s), C). Pour ξ ∈ Ω nt) ∈ ∆.Commençons par prouver l'holomorphie de F sur ∆. Comme F est manifestement une fonction continue, il suffit de prouver que son ∂ au sens des distributions est nul. Considérons alors une forme test θ ∈ C ∂F, θ >= -< F, ∂θ >= -f -1 (∆) ξ ∧ ψ ∧ d(f * (θ))puisque ∂θ = dθ et puisque loin du lieu critique de f le théorème de Fubini banal s'applique à des fonction continues. Comme on ad(ξ ∧ ψ ∧ f * (θ)) = ξ ∧ ψ ∧ d(f * (θ)))puisque dψ = 0 et que dξ ∧ f * (θ) est de type (n + 2, 1) donc nulle, la formule de Stokes permet de conclure à l'holomorphie de F . Pour calculer ∂F ∂s au sens des distributions, considérons maintenant une forme testζ dt ∧ ζ >= -< F, d(dt ∧ ζ) >=f -1 (∆) ξ ∧ ψ ∧ d(f * (dt ∧ ζ)).Comme on a dξ = d / ξ + dt ∧ ∂ξ ∂t la formule de Stokes donne< ∂F ∂s .ds, dt ∧ ζ >= f -1 (∆) d / ξ ∧ ψ ∧ f * (dt ∧ ζ).Le théorème de Fubini donne alors ∧ ψ .ds ∧ dt ∧ ζ ce qui donne bien notre formule de dérivation "en s". Soit ζ une forme-test choisie comme plus haut. On a< ∂F ∂t .dt, ds ∧ ζ >= -< F, d(ds ∧ ζ) >=f -1 (∆) ξ ∧ ψ ∧ d(f * (ds ∧ ζ)).La formule de Stokes donne alors< ∂F ∂t .dt, ds ∧ ζ >= f -1 (∆) ∂ξ ∂t ∧ dt ∧ ψ ∧ d / f ∧ f * (ζ) + d / ξ ∧ ψ ∧ ∂f ∂t .dt ∧ f * (ζ) puisque f * (ds) = df = d / f + ∂f ∂t .dt. On trouve alors, puisque∇(d / ξ) = d / f ∧ / ξ) ∧ ψ ∧ dt ∧ f * (ζ).On a donc bien, à nouveau grâce au théorème de Fubini, la formule annoncée, pour d / ξ ∈ E : Remarquons que si I : E → O H×C est le morphisme de faisceau localement défini par [d / ξ] → γs,t d / ξ d / f , on a établi les égalités suivantes : (∂ s ) • I • b = I et (∂ t ) • I = I • (b -1 ∇) de morphismes de faisceaux respectivement de E à valeurs dans O H×C et de P à valeurs dans O H×C .

  ∇ contenant b N .E pour N assez grand (localement sur D * ). Ceci équivaut à l'existence localement sur D * d'un entier N tel que l'on ait ∇ j E ⊂ b j-N .E pour tout j ≥ 0. On dira que E est b -1 ∇-régulier si E est localement sur D * contenu dans un sous-O D

	Soit n ≥ 2 un entier. On se place sous l'hypothèse (H 0) de [B.06], c'est à dire que f : (C n+1 , 0) → (C, 0) est un germe non constant de fonction holomorphe à lieu singulier de dimension 1. On considère un représentant de Milnor f : X → D de ce germe dont le lieu singulier, S := {x ∈ X / df x = 0}, est une courbe de X dont chaque composante irréductible passe par l'origine et telle que S * := S \ {0} soit lisse et réunion disjointe de disques topologiques épointés. On suppose donnée une fonction non singulière t : X → D telle que sa restriction à S fasse de S un revêtement ramifié seulement à l'origine du disque D et telle que l'on ait S * = {dt ∧ df = 0} au voisinage de S * . On a montré dans [B.06] que sous l'hypothèse (H 0) il existe toujours de telles fonctions t au voisinage de l'origine. On a défini ∇ : E → E dans [B.06] et on a montré que b -1 ∇ est une O D -connexion sur E[b -1 ] qui commute à a et b. La notion de régularité qui est introduite ci-dessous signifie qu'il existe localement sur D * un O D [[b]]-réseau cohérent stable par b -1 Définition 2.1.1

  Théorème 2.1.3 Sous l'hypothèse (H 0) de [B.06] E est b -1 ∇-régulier sur S * . Démonstration. Comme près du point p ∈ S * la famille des fonctions à singularités isolées donnée par t → f t est à µ-constant elle est topologiquement triviale au voisinage de p. En identifiant S * et D

* via la fonction t au voisinage de p, on a donc l'existence d'un voisinage U de p dans X et une application continue Φ

  = f et ne s'annule pas sur {t = 0}. 3. La relation M.f ⊂ M 2 .J / (f ) implique que le plus grand sous-(a,b)-module à pôle simple de f t pour chaque t = 0 est la fibre en t de M.

	1 p + 1 q + 1 r < 1 résulte de l'étude de [B.06] puisque l'on a
	W :=	1 p	.x.	∂ ∂x	+	1 q	.y.	∂ ∂y	+	1 r	.z.	∂ ∂z	+ (1 -ρ).t.	∂ ∂t
	qui vérifie W.f

On a donc G = M = M.E dans ce cas.

  2.6. et 4.2.8. de [B.06]. C'est à dire une section locale sur un ouvert de H×C, où exp : H → D * est le revêtement universel du disque pointé, du système local dont les fibres sont les espaces vectoriels H n-1 (f -1 t (s), C), où nous avons posé f t (x) = f (x, t).

	∂ ∂s γs,t	ξ =	γs,t	d / ξ d / f
	qu'il faut lire sous la forme
	primitive "en s" de		γs,t		d / ξ d / f		=	γs,t	d / f ∧ ξ d / f	.
	Pour tout d / ξ ∈ E on a la formule de dérivation "en t"
	∂ ∂t γs,t	ξ =	γs,t	∇(d / ξ) d / f
	que l'on peut lire sous la forme
	∂ ∂t γs,t	d / ξ d / f	=	γs,t	b -1 ∇(d / ξ) d / f
	pour d / ξ ∈ P.

Pour (s, t) ∈ C×C voisin de (0, t 0 ) considérons une famille horizontale multiforme (en s) de (n -1)-cycles compacts 7 γ s,t ⊂ {f (x, t) = s}. Nous utilisons ici la trivialité topologique locale de l'application (f, t) : C n+1 → C 2 dont le lieu critique est {x = 0} × C au voisinage de S * × {0}, grâce à la locale constance de µ sur S * . Il s'envoie sur {s = 0} ⊂ C 2 . Proposition 3.1.2 Pour tout d / ξ ∈ E on a la formule de dérivation "en s" 7

Voir [B.05] ou [B.06].

C'est à dire que toute section sur un ouvert connexe V de S * qui est nulle sur un ouvert non vide de V est nulle.

La a-torsion coïncide avec la b-torsion et cette dernière est nulle (voir [B.06]).


Cyril Cohen
email: cyril.cohen@inria.fr

Boris Djalal
email: boris.djalal@inria.fr

Formalization of a Newton Series Representation of Polynomials

Keywords: D.2.4 [SOFTWARE ENGI-NEERING]: Software/Program Verification -Correctness proofs, Formal methods, F.2.1 [ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY]: Numerical Algorithms and Problems-Computations on polynomials, I.1.2 [SYMBOLIC AND ALGE-BRAIC MANIPULATION]: Algorithms-Algebraic algorithms, I.1.1 [SYMBOLIC AND ALGEBRAIC MANIPULATION]: Expressions and Their Representation-Representations (general and polynomial) formalization of mathematics, algebraic numbers, fractions, polynomials, Newton power series

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Real algebraic geometry studies points and sets defined by polynomial equations and inequations. Algorithms in real algebraic geometry handle these points and sets in an implicit way and use the defining polynomials as a basis for computations. For example, a real algebraic number is represented by a nonzero polynomial with rational coefficients and a way to select a root (e.g. real approximation, rational interval (Cohen 2012b), Thom encoding). In order to compute basic arithmetic operations on algebraic numbers (sum, product, comparison), we perform operations on these polynomials and need to find a polynomial whose roots are the result of the given operation.

Given two polynomials in K[X], P = aiX i with roots α1, . . . , αm and Q = bj X j with roots β1, . . . , βn, we wish to compute a polynomial whose roots are αi + βj for (i, j) ∈ {1, . . . , m}×{1, . . . , n}, which we write P ⊕Q and which we call composed sum. Similarly we define the composed product P ⊗ Q, whose roots are αiβj for (i, j) ∈ {1, . . . , m} × {1, . . . , n}.

If the base field K is algebraically closed (i.e. in which every non constant polynomial has a root), we can split the polynomials P = an i (Xαi) and Q = bm j (Xβj ), and compute the results

P ⊕ Q = ambn (i,j) (X -(αi + βj)). P ⊗ Q = ambn (i,j) (X -(αi • βj )).
Given an arbitrary field K, folklore mathematics textbooks usually take an algebraic closure or splitting fields and performs the construction above. However, in order to take the algebraic closure, one needs to already have a way to perform the composed sums and products, so this does not solve the problem. In fact, these operations may rely on purely algebraic computations on the coefficients, and thus do not require a preexisting algebraic closure to perform the computation.

In prior work by the first author (Cohen 2012b), we provide a way to perform these operations and build the algebraic closure. However the underlying algorithms for composed sums and products use resultants, which is not an efficient implementation and would not allow for a practical implementation of algebraic numbers. An efficient way relies on a morphism between polynomials and Newton power series, as described by A. Bostan in [START_REF] Bostan | Algorithmique efficace pour des opérations de base en Calcul formel[END_REF], which is a main reference for the computer algebra community. Composed sums and products on polynomials are mapped to low-cost operations on Newton power series. In the case of zero characteristic, the new algorithm improves the complexity by a linear factor [START_REF] Bostan | Algorithmique efficace pour des opérations de base en Calcul formel[END_REF]. If n denotes the degree of two input polynomials and M (n) the costs to multiply two polynomials of degree n, then the traditional algorithm based on bivariate resultant has asymptotic complexity O(nM (n) log(n)) while the new algorithm has complexity O(M (n 2 )) [START_REF] Bostan | Algorithmique efficace pour des opérations de base en Calcul formel[END_REF]. In this work we use our prior knowledge of the existence of an algebraic closure (even though it is not efficient) as a reference implementation to certify our new results. Indeed, all the algorithms we describe use the coefficients in the base field, but all the proofs are made by supposing one can split the polynomials in a field extension. The existence of the algebraic closure provides grounding for this assumption and thus serves as a bootstrap.

In this paper, we describe a COQ formalization of an isomorphism between monic polynomials of a bounded degree and a truncated version of formal power series.

In order to explain and formalize this isomorphism we first introduce the general mathematical notions we had to formalize (Section 2). The truncated formal power series (Section 2.1) is an approximation of traditional power series, better suited for use in COQ with the MATHEMATICAL COMPONENTS library. We also need to build the fraction field of the domain of polynomials in order to compute the isomorphism, and instead we first give an abstract interface for poles and evaluation of fraction (Section 2.2) which we implement twice.

Throughout Section 3, we describe some algorithms on polynomials on a field and prove them correct with regard to another, more concise definition in an algebraic closure. We explain how to compute the Newton power series in the context of algebraically closed fields (Section 3.1). Then we describe an algorithm to compute the Newton power series without making operations inside an algebraic closure and we prove it computes the same result as in the previous section (Section 3.2). We also provide an explicit inverse, which computes a polynomial from a Newton power series. Finally, we explain how to compute the composed sum and product using a translation to a Newton power series, a simple computation on the formal power series and then a backward translation.

The results described in this paper are entirely formalized in COQ, unless explicitly stated. The formal development is available on the first author webpage: http://www.cyrilcohen.fr/work/newtonsums/ 2. Mathematical background 2.1 Formal power series and truncated formal power series In this paper, we make statements indirectly involving formal power series (FPS), the common mathematical object noted K

[[X]].
FPS is a generalization of polynomials: it is an infinite sequence of coefficients (ai) i∈N . Unlike polynomials, the set of non-zero coefficients is not necessarily finite. For example, 1 + X 2 is a polynomial (thus a FPS) and S = 1 + X + X 2 + X 3 + . . . is the FPS with general term X i . In the general case, coefficients are taken in a commutative ring.

The set of formal series R[[X]] over a commutative ring R has a structure of commutative ring. In this work, we study formal series K[[X]] over a field K of characteristic zero, which means that for any natural number n:

n i=1 1 K = 0.
In COQ we could implement FPS by functions from nat to the given ring, as it is done by A. Chaieb in [START_REF] Chaieb | Formal power series[END_REF]. In this case, comparing two FPS amounts to proving that two given functions are equal. This approach has two drawbacks: equality becomes undecidable (more precisely, disequality is semi-decidable) and without the functional extensionally axiom two FPS with equal terms are not provably equal. While we would not mind being in a context where the second axiom is validated (e.g. Homotopy Type Theory (Univalent Foundations Program 2013)) the algebraic library we use extensively in our work requires a decidable equality.

Instead of FPS, we consider an approximation we call truncated formal power series up to X m (TFPSm or TFPS if there is no ambiguity), noted Km[X]. In this case, we deliberately provide only m + 1 coefficients. The set of TFPSm is isomorphic to the set of polynomials quotiented by X m+1 . Consequently, we can implement a TFPS by a polynomial whose degree is less than m, i.e. by a polynomial together with a proof that its degree is less than m. We use polynomials from the MATHEMATICAL COMPONENTS library, already used for many results (algebraic numbers, Galois theory, Cayley Hamilton theorem, odd order theorem [START_REF] Gonthier | A machine-checked proof of the odd order theorem[END_REF], . . .).

Record tfps := TFPS { truncation_tfps :> {poly K}; _ : size truncation_tfps <= n.+1 }.

We write {tfps K n} for the formal power series over K truncated up to precision X n (included).

We can use the following fact to turn any polynomial into a TFPSm for any m, and build a smart constructor Tfpsp which turns any polynomial to a TFPSm. We also provide a construction to define a TFPSm from its coefficients:

Notation "[tfps s => E]" := Tfpsp m (\poly_(i < m.+1) E)

Arithmetic properties

The decision procedure for equality consists in comparing the underlying polynomial representations. The addition of two polynomials whose degrees are less than m produces a polynomial whose degree is less than m. Thus, we define addition of two TFPS as the addition of the underlying polynomials.

In order to multiply two TFPSm, we multiply the underlying polynomials, we can get a polynomial with degree more than m+1. We then take the remainder modulo X m+1 to guarantee that the degree of the obtained polynomial is less than m. This makes sense since the coefficients from m + 1 are only partially known (we are missing the information from the rest of the series).

Our definition of multiplication of two TFPS in COQ is as follows:

Definition mul_tfps (f1 f2 : {tfps K m}) : {tfps K m} := Tfpsp (f1 * f2).

For example in K2[X], we have:

(1 + X 2 ) × X = X.
Additionally, the Hadamard product of two FPS is the term-wise product of the FPS. Formally we write:

Definition hmul_tfps (f1 f2 : {tfps K m}) : {tfps K m} := [tfps s => f1'_s * f2'_s] For example in K2[X], we have:

(1 + X 2 ) ⊙ (1 + X + 2X 2 ) = 1 + 2X 2 .
FPS over an integral domain forms an integral domain. This is not true with TFPS as we defined them. Indeed, in TFPS3

X 2 • X 2 = 0 mod X 4
This is due to the fixed precision of our representation. We could opt for a "floating truncation" FPSm, where m would actually refer to the number of meaningful terms, i.e. the representation of these series would be of the form

X M 0≤s≤m asX s
with a0 nonzero. Moreover, allowing M to be negative would lead to a representation of Laurent formal series instead.

Derivative

We can translate any statement about FPS into a statement about TFPS. Let's consider the additivity of formal derivation as an example. In terms of FPS, it expresses as:

∀f, g ∈ K[[X]] (f + g) ′ = f ′ + g ′ . In terms of TFPS, it expresses as: ∀m ∈ N, ∀f, g ∈ Km[X] (f + g) ′ = f ′ + g ′ .
Here, we just have replaced occurrences of FPS by TFPS. However, the translation of a statement dealing with FPS into a statement dealing with TFPS can be trickier. This is the case for the definition of the derivative of a TFPS (see 2.1.1). We formally prove that Km[X] is a ring. The relationships between FPS and TFPS is summarized by the following diagram: where n ≤ m, ։ denotes a surjective ring morphism, and ⌊.⌋ m denotes the function which sends a FPS (or a polynomial) to its truncation in Km[X]. Please note that in our COQ development we chose only to deal with TFPS, not FPS. One can mathematically define the derivative, primitive, exponential and logarithm of FPS. All these operations are required to formalize the algorithm which changes the representation of a polynomial to a Newton TFPS. We are going to define such operations on TFPS by adapting their equivalent definitions on FPS.

K[[X]] Km[X] Kn[X]
The derivative of a polynomial is defined as follows. For P ∈ K[X],

P ′ = m i=1 i • ai X i-1 = m-1 i=0 (i + 1) • ai+1 X i .
The notion of derivative on polynomials is easily extended to FPS.

For P ∈ K[[X]], P ′ = ∞ i=1 i • ai X i-1 = ∞ i=0 (i + 1) • ai+1 X i .
In COQ we write:

Definition deriv_tfps : {tfps K n} -> {tfps K n.-1} := fun f => [tfps s => f'_s.+1 *+ s.+1]
Note that derivation must be a map from Km[X] to Km-1[X], not a map from Km[X] to Km[X]. Indeed, when we take derivative, we lose precision. Otherwise, the following commutative diagram would be broken:

K[[X]] K[[X]] Km[X] Km.-1[X].

⌊.⌋ m-1

Primitive

We define the canonical primitive of a polynomial as the only primitive such that the constant term is zero.

P = m i=0 ai X i = m i=0 ai i + 1 X i+1 .
Definition prim (p : {poly K}) := \poly_(i < (size p).+1) (p'_i.-1 *+ (i != 0) / (i%:R)).

From the canonical primitive, we can derive the family of primitive functions for each possible constant term in the ring by adding the constant a, as in (a + prim p).

Like for the derivative, these definitions naturally extend to a FPS.

∞ s=0 as X s = ∞ s=0 as s + 1 X s+1 .
We formally define primitive for polynomial and for TFPS.

Definition prim_tfps : {tfps K n} -> {tfps K n.+1} := fun f => [tfps s => f'_s.-1 *+ (s != 0) / s%:R]. Note that the primitive must be a map from Km[X] to Km+1[X], not a map from Km[X] to Km[X], for exactly the same reason as for derivation.

We prove basic theorems linking derivative with primitive:

P ′ = P P ′ = P -a0
Our corresponding COQ pieces of code of these two statements are:

Lemma prim_tfpsK (n : nat) : cancel (@prim_tfps n) (@deriv_tfps K n.+1).

Lemma deriv_tfpsK n (f : {tfps K n.+1}) : {in @coef0_is_0 K n.+1, cancel (@deriv_tfps _ _) (@prim_tfps _)}.

Composition

The composition of FPS is not always well defined: given two

P = ∞ i=0 ai X i and Q = ∞ j=0
bj X j , for the composition to be well-defined it is sufficient that b0 = 0 (cf (Wikipedia)). We can then write the composition of P et Q in the following way

P • Q = ∞ i=0 ai ( ∞ j=0 bjX j ) i .
We could also define the composition with explicit coefficients:

P • Q = ∞ k=0 c k X k with c k = i∈N, s∈N i j∈I i s j =k   ai j∈I i bs j  
where Ii = {1, . . . , i}.

The coefficient c k is well-defined whenever b0 = 0, since the sum and each product is finite. Indeed, for any k, if there is a j such that sj = 0 then j∈I i bj = 0, so we can sum over only the sequences s ∈ (N * ) i .

Since j∈I i sj = k and ∀j ∈ Ii, sj > 0, we have i ≤ k. Hence the sum indexed by i ∈ N and s ∈ N i such that j∈I i sj = k is indeed finite. This proves that c k is a finite sum and is welldefined.

The formula above works also for k = 0. In this case the only possible i is 0. It leads to:

c0 = a0 j∈∅ bs j = a0 × 1 = a0
which is the expected result. Formally proving the general formula for the coefficient of the composition of two TFPS is the subject of an ongoing work.

Composition for polynomials is already defined in the MATH-EMATICAL COMPONENTS library. We formally define this notion when formal power series are truncated, by directly defining the composition in terms of polynomials. We use this opportunity in our COQ code:

Definition comp_tfps m (q p : {tfps K m}) := if q \in (coef0_is_0 K m) then Tfpsp m (comp_poly q p) else 0.

Notation "p \So q" := (comp_tfps q p).

We did not yet prove in COQ the formula with explicit coefficients, nor did we prove the existence of the compositional inverse when the coefficient of X 0 is 0 and the coefficient of X 1 is 1. Indeed, this could have eased the definition of exponential and logarithm, but it is not used in our developments yet (it is not required to define Newton Power Series).

Exponential

There are two main ways to define the exponential of a FPS.

We can see the exponential as the element of K

[[X]] defined by exp = ∞ i=0 X i i! .
Note that here we use the hypothesis that K has zero characteristic to guarantee i! = 0. This is commonly expressed in MATHEMATI-CAL COMPONENTS by the following hypothesis.

Hypothesis char_K_is_zero : [char K] =i pred0.

We can also view this exponential as a function from FPS with zero constant to FPS with constant 1, defined by:

fexp(P ) = ∞ i=0 P i i! .
This definition is related to the first one by: fexp(P ) = exp •P.

In our development, we use the former definition adapted to TFPS: Definition exp (p : {tfps K n}) : {tfps K n} := if p \notin coef0_is_0 then 0 else Tfpsp (\sum_(i < n.+1) ((i'!%:R)^-1) *: (p ^+ i))).

We formally prove that the formal exponential is a morphism: for all P and Q such that P (0) = Q(0) = 0, exp(P + Q) = exp(P ) exp(Q). The corresponding COQ code statement is:

Lemma exp_is_morphism :
{in (@coef0_is_0 K m) &, {morph (@exp _ _) : p q / p + q >-> p * q}}.

We formally prove the formula linking the exponential and its derivative, which states, for any formal power series P :

(exp P ) ′ = P ′ exp(P ).

In our COQ code, this formula is expressed as:

Lemma deriv_exp (m : nat) (p : tfps K m) : (exp p)^' () = (p^' ()) * (Tfpsp m.-1 (exp p)).

It would be simplier if exp were defined as a TFPS, as we could write exp ′ = exp and prove the previous theorem as a trivial application of the derivation of composition theorem. Moreover, injectivity could be obtained by the existence of compositional inverses under the right conditions.

Logarithm

As for exponential, logarithm can be defined both as a function or as a FPS. For any P such that P0 = 1:

log P = - ∞ i=1 (1 -P ) i i .
This series is well-defined whenever P0 = 1 for the same reason as for the composition. In our development, we use the latter definition adapted to TFPS:

Definition log (p : {tfps K n}) := if p \notin coef0_is_1 then 0 else Tfpsp n (-\sum_(1 <= i < n.+1) ((i %:R) ^-1) *: ((1 -val p) ^+i)).

We formally prove:

(log P ) ′ = P ′ P .
We expressed the lemma about the derivative of the formal logarithm on TFPS with:

Lemma deriv_log (m : nat) (p : tfps K m) :

p \in (coef0_is_1 K m) -> (log p) ^' () = (p )^' () / (Tfpsp m.-1 p).

We prove that log(exp P ) = P on TFPS formally by derivating the expression and using the lemma about the derivative of log. It is possible to obtain this results from logarithm injectivity. But in our development, we use the derivative of the logarithm formula to prove the injectivity of the logarithm function. The injectivity of the formal logarithm on TFPS expresses as:

Lemma log_inj : {in coef0_is_1 K n &, injective (@log K n)}.
We prove the injectivity of the logarithm as follows. First, we notice that the derivative formula of a division holds for TFPS. For any TFPS P and Q such that Q = 0, we have:

P Q ′ = P ′ Q -QP ′ Q 2 .
Let be TFPS P et Q such that P (0) = 1 and Q(0) = 1, and let's suppose that we have log(P ) = log(Q). Since Q(0) = 1, we have Q = 0. We are going to prove that P = Q and thus the injectivity of the logarithm. By derivating the hypothesis, we get:

P ′ P = Q ′ Q which rewrites as P ′ Q -QP ′ = 0 then P ′ Q-QP ′ Q 2 = 0 (since Q = 0)
. Using our first remark, we thus get

P Q ′ = 0. It implies that P Q is a constant.
In other words, the underlying polynomials of P and Q are associate polynomials. Since P (0) = Q(0), we finally get P = Q. This achieves the proof of the injectivity of the formal logarithm on TFPS.

We could simplify some proof by getting the logarithm of a series as a composition for series. Indeed we could define log(1 -X) as a series:

L = - ∞ i=1 X i i .
So that log P = L•(1-P ), which would be well-defined whenever the constant coefficient of P is 1. Moreover, injectivity could be obtained by the existence of compositional inverses under the right conditions.

Fractions

The main theorem about Newton power series requires polynomial fractions. We use a more general result about the field of fractions of an integral domain and K(X) is constructed as the field of fractions of K[X]. The construction of polynomial is correct because K[X] is an integral domain whenever K is a field. Let R be an integral domain and ι : R ֒→ F(R) the (canonical) injection to its field of fractions.

We not only want to manipulate fractions, we also want to define functions from F(R) to another ring without having to go back to the implementation of F(R) as R×R quotiented by an equivalence relation.

In this section we show an interface for an abstract notion of poles of fraction. We first show two use-cases of this interface. We then establish the relationship between this interface and the universal property of the field of fractions.

Here we present the first use-case, which is the evaluation of polynomial fractions. Let's consider the following examples:

• the evaluation of X 2 -2 X + 5 in 3 is 7 8 , • the evaluation of X 2 -2 X -3 in 3 is not defined because 3 is a pole, • the evaluation of X 2 -3X X 2 -X -6 = X X + 2 in 3 is 3 5 .
An evaluation algorithm proceeds by first deciding whether there is a good representation for our fraction. Then, there are two mutually exclusive possibilities:

• evaluation is not defined

• it boils down to evaluating two polynomials and performing a division.

A unifying interface via abstract poles of fractions

Let R be an integral domain and ι : R ֒→ F(R) the canonical injection to its field of fractions. Let K be a field and f : R → K a morphism. For any a in K, we say x has a regular representation in a if x can be written as u v with f (v) = a. We use this definition of regular representation for a = 0.

We define

κ(x) = f (u) f (v)
if there is a regular representation u v of x in 0 undefined otherwise (we return 0 in COQ) .

where we say x has a regular representation in 0 if x can be written as

Our κ is mathematically well-defined, but not always computable.

The computability of κ is guaranted when these three points are satisfied: f is computable, for all x, it is decidable whether there is a regular representation of x and we can compute it when it exists.

Application to the evaluation of polynomial fractions. Let K be a field.

• R is the ring of polynomials K[X]

• K(X) is the field of fractions of R, noted F(R)

• f : R -→ K is the evaluation of polynomials in a

The evaluation of polynomial fractions in a is the map:

κ : F(R) -→ K κ(x) = f (u) f (v)
if x can be written as u v with f (v) = 0 undef ined otherwise.

Note that f is parameterized by an element a ∈ K.

Application to the lifting of a the field of coefficients. Let F and L denote fields and L/F be a field extension, where ι : F ֒→ L is the canonical injection. We assume that we know how to lift from F[X] to L(X). We want to lift any element of F ∈ F(X) to L(X).

We reuse or interface where

• F[X] is the integral domain R • F(X) is the field of fractions of R, noted F(R) • L(X) is a field K • f : R -→ K is the lifting from F[X] to L(X)
• our lifting function from F(X) to L(X) is the map: κ :

F(R) -→ K κ(x) = f (u) f (v)
if x can be written as u v with v = 0 undef ined otherwise.

Note that since here f is injective, v = 0 implies f (v) = 0. Thus, κ is always defined.

Relation to the universal property of fractions

When f is injective, it is basically the universal property of the field of fractions of an integral domain. This universal property states: for any field K and injective ring morphism f from R to K, there is a unique ring morphism κ from the field of fractions F(R) to K such that our diagram (1) commutes. However the function κ is defined even when f is not injective -we call this broader definition of κ an abstract evaluation. When f is not injective, κ fails to be a ring morphism. We develop abstract evaluation theory in the general case i.e. even when f is not injective. We define the notion of abstract pole by:

x ∈ F(R) has a f -pole if: ∀u v ∈ R such that x = ι(u) ι(v) , f (v) = 0.
The presence of an abstract pole, or f -pole, in x means that there is no regular representation of x. It is expressed as follows in our COQ code: Definition has_pole x := forall y : R * R, x = y.1%:F / y.2%:F -> f y.2 = 0.

We then suppose that any x ∈ F(R) either has a f -pole or can be written x = ι(u) ι(v) for some u v ∈ R such that f (v) = 0. We derive formally the following results:

• κ(0) = 0 • κ(1) = 1 • ∀x ∈ F(R), κ(-x) = -κ(x) • ∀x, y ∈ F(R), κ(y) = 0 =⇒ κ( x y ) = κ(x) κ(y)
The latter result is expressed as:

Lemma kappa_div (y z : {fraction R}) : kappa z != 0 -> kappa (y / z) = (kappa y) / (kappa z).

Extra results are provided in the interface when ι is injective. When ι is injective, the main and summarizing result is that abstract evaluation is a ring morphism. We use the universal property of fractions -lifting from F(X) to L(X) -in the particular situation where F = L(Y ) for a second formal variable Y . We use it to define lifting from F(X) to (F(Y ))(X). Here, R is F[X], K is F(X) and f is the lifting function from F[X] to (F(Y )) [X]. Then, we derive lifting of polynomial fractions automatically : this implementation helps defining composition of fractions of polynomials. Let U and V ∈ F(X). The composition of U and V is defined by: U

• V = (κ(U ))(V ).
That is, we lift U . Then we swap variables X and Y and evaluate the resulting polynomial in V .

Taylor series of polynomial fractions

In Section 3.2 we use the concept of Taylor series of polynomial rational, which is well defined for the set of elements of K(X) such that the denominator of an irreducible representation has got a nonzero constant. For example, 1 X has no Taylor series and 1

1-X has the following Taylor series

∞ i=0 X i = 1 + X + X 2 + X 3 + . . . .
Note that X 2 X-X 2 has a Taylor series despite the fact that the constant term of X -X 2 is zero. If 0 is a pole of the fraction, we know there is no Taylor series. Otherwise, there is a representation U V of the fraction where the constant coefficient of the denominator V is nonzero. Then we find the Taylor series S of U V by solving the system deriving from the equation S • V = U (in this equation U and V cast to FPS). Sum and product of fractions preserve the existence of a Taylor series, hence fractions which have a Taylor series form a sub-ring of the field of polynomial fractions. We use the very same concept of Taylor series, adapted to TFPS. Instead, we output a TFPS with the desired precision.

We could also reuse the generalized universal property of the field of fractions, in two possible different ways. The first way would require a generalization of the interface for the generalized universal property of the field of fractions with a morphism which target is in an integral domain instead of a field. Then we consider the morphism that casts a polynomial inside the integral domain of "floating truncation" FPS. A second way would be to reuse our interface with a morphism which target is truncated Laurent formal series, and show that when the source fraction has no pole, the Laurent formal series has a nonnegative order:

X M 0≤s≤m asX s with M ≥ 0.

Newton Power Series

The mathematical theory of this section is entirely based on [START_REF] Bostan | Algorithmique efficace pour des opérations de base en Calcul formel[END_REF]. A Newton power series is a FPS which represents a monic polynomial (polynomial with leading coefficient equal to one) without loss of information. In pratice, it is enought to use truncated Newton power series, because only n coefficients of the formal series are used to recover the n coefficients of a monic polynomial of degree n.

Throughout this section, we take the running example of two polynomials P = X 2 -2 and Q = X + 3 we compute the composed sum and product of.

Newton series in an algebraic closed field

Let K be a field and L an algebraically closed extension of K, where ι : K ֒→ L is the injective morphism from K to L. Let P = i≤m aiX i be a polynomial of K[X]. We write abusively ι(P ) = i≤m ι(ai)X i the lifting of P to L[X] and we write p ^iota in COQ.

Since L is algebraically closed, ι(P ) has roots αi ∈ L for i ∈ {1, . . . , m}, such that ι(P ) = ι(am) i (Xαi). Note that, in common mathematical practice, we would simply write P = am i (Xαi), the injection ι being implicit.

With our example, we have X 2 -2 = (X -√ 2)(X + √ 2) and X + 3 = X -(-3). And the results of the composed sum and products should be

(X 2 -2) ⊕ (X + 3) = X + 3 - √ 2 X + 3 + √ 2 = X 2 + 6X + 7 (X 2 -2) ⊗ (X + 3) = X + 3 √ 2 (X -3 √ 2 = X 2 -18
We can define

Ns(P ) = i≤m α s i (2)
By convention, the sum is zero if P has no root. This can be formalized using the library bigop [START_REF] Bertot | Canonical big operators[END_REF]) of Mathematical Components libraries, which provides a theory of finite iterations of an operation on a monoid.

With our example, we have:

Ns(X 2 -2) = √ 2 s + - √ 2 s = 2 k+1 if s = 2k 0 otherwise
and Ns(X + 3) = (-3) s

The Newton power series of P is the following FPS :

N (P ) = ∞ s=0 Ns(P ) X s (3)
We call forward transformation the process to obtain N (P ) from P . With our example, we have:

N (X 2 -2) = 2 + 4X 2 + 8X 4 + k>2 2 k+1 X 2k N (X + 3) = 1 -3X + 9X 2 + k>2 (-3) k X k
The Newton power series N (P ) and the Newton sums Ns(P ) are respectively in L[[X]] and L. However, each Ns(P ) is a symmetric function of the roots of P : each Ns(P ) remains unchanged when we apply a permutation to the roots of P . Thus, by the fundamental theorem of symmetric polynomials, Ns(P ) can be expressed as a polynomial expression of elementary symmetric functions of the roots of P , which are the coefficients of P (up to a sign). This means Ns(P ) can be expressed as a polynomial in the coefficients of P and is hence in K instead of L. Hence N (P ) can be written as a formal power series over K. Whereas common mathematical practice does not observe the distinction, in COQ we have to be specific and we cannot write the definition of Newton sums as in (2) and Newton power series as in (3). There are two options: using the theory of symmetric polynomials we could have proved that the Newton series are in the sub-field K of L and extracted the corresponding elements, or we can provide an alternative definition of Newton series that makes it obvious they belong to K. Since this alternative definition is also the one used for efficient computation, we chose to define Newton sums using the latter.

The remainder of this section gives a concrete direct representation of Newton sums as a value in K and hence the truncated power series newton_tfps representing the series N (P ), but in K

[[X]] instead of L[[X]].
With the definition in Section 3.2, we eventually prove that forall (p : {poly K}) (n : nat), (newton_tfps n p) ^iota = [tfps j => \sum_(r <-roots (p ^iota)) r ^+ j].

Note that in fact, L need not be algebraically closed, but a splitting field of P . However, it is sufficient for our development to consider an algebraically closed extension, because we can actually provide the algebraic closure of the fields we consider (Cohen 2012b).

We now explain how to define newton_tfps as a series with coefficients in K.

Newton power series in a general setting

We now show how to compute N (P ) directly from the coefficients of P , without the need for factoring P . Then, we will present a procedure to recover P from N (P ), where P is monic (i.e. with a leading coefficient equal to 1, which implies P = 0). For any polynomial P , the forward transformation theorem holds:

N (P ) = rev(P ′ ) rev(P ) (4)
where rev is the reverse operator on polynomials, which outputs a polynomial by reversing the list of coefficients of the input polynomial. For instance: rev(1 + 2X + 3X 2 ) = 3 + 2X + X 2 , rev(X 3 -X 5 ) = -1 + X 2 , rev(X 2 -2) = 1 -2X 2 , rev(2X) = 2, rev(X + 3) = 1 + 3X and rev(1) = 1.

In the equation above P is in K[X] and N (P ) is in K(X). The constant coefficient of rev(P ) is nonzero because P = 0, thus rev(P ′ ) rev(P ) has a Taylor series, which is a FPS in K[[X]].

With our example we have

rev(2X) rev(X 2 -2) = 2 1 -2X 2 = 2 s≥0 (2X 2 ) s = s≥0 2 s+1 X 2s rev(1) rev(X + 3) = 1 1 + 3X = s≥0 (-3X) s = s≥0 (-3) s X s
Hence we define newton as a rational fraction in K(X) and newton_tfps as a TFPS with coefficients in K.

Fact

  leq_modpXn m p : size (p %% 'X^m) <= m. Definition Tfpsp m : {poly K} -> {tfps K m} := fun p => TFPS (leq_modpXn m.+1 p).

.

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . .. . . . . ..

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	⌊.⌋ m	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . derivative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . derivative . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ⌊.⌋ m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Acknowledgments

Pretty COQ code listing was done thanks to Assia Mahboubi's file (Mahboubi). Commutative diagrams where drawn thanks to Pedro Quaresma's package (Quaresma). We thank our colleagues for their input on this work: Enrico Tassi, José Grimm, Laurence Rideau, Laurent Théry and Yves Bertot.

The proof of the equivalence of the definitions (3) and (4) relies on the following lemma about the reverse function.

Proof.

We now prove the equivalence of the definitions (3) and (4).

Proof. The polynomial P factorizes in L[X] because L is an algebraic closed field:

The definition (3) gives

The definition (4) uses

and rev(P ′ ) = P ′ 1 X X m-1 .

Then:

The formal proof follows the same reasoning steps. In the reference [START_REF] Bostan | Algorithmique efficace pour des opérations de base en Calcul formel[END_REF], ( 3) is a definition and (4) is a theorem, whereas in our COQ formalization, we exchange definition and theorem of Newton representation. The formal proof relies on TFPS, on fractions and on the development of a fraction of polynomials into a TFPS.

In section 3.3, we use this transformation to compute the Newton power series associated with two polynomials P and Q, on which we perform the operation corresponding to the composed sums and products. In order to get the result, we need to transform back a power series into a polynomial.

We prove the backward transformation theorem

First, remark that the constant term of N (P ) is

(the number of roots of P , which is the degree of P ). So, X divides m -N (P ). It is then possible to define m-N (P )

Whenever we encounter an imprecise equality between a polynomial and an infinite FPS, we explicitly truncate the FPS to the right precision. This formula (5) establishes a relation between rev(P ) and N (P ). It is possible to recover rev(P ) from N (P ). Besides, it is possible to recover P , except the multiplicity of 0 in P , from rev(P ). Thus, it is possible to recover P , except the multiplicity of 0 in P , from N (P ).

When P (0) = 0, which is a decidable property, rev(rev(P )) = P holds and thus our backward conversion formula rewrites as:

If P (0) = 0, we can recover the multiplicity of X by making the difference between the degree of the result and m.

We write the inverse of newton_tfps:

Definition newton_inv (p : {tfps K m}) : {poly K} := revp (exp (prim_tfps (divfX ((p'_0)%:S -p)))).

We now prove (5). First we check that for any polynomials U , V such that U0 = 1:

Proof.

We proved (6). So, by applying (6) to the desired theorem, it is sufficient to prove:

We prove ( 7) by considering both sides as FPS. On one side:

On the other side:

We proved:

The result follows by applying ( 6) to (7). In our COQ code, the backward transformation theorem is expressed as: Lemma newton_tfpsK (p : {poly K}) :

size p <= m.+1 -> ~~(root p 0) -> p \is monic -> newton_inv (newton_tfps m p) = p. As one could see in the proof, we use a result about formal geometric series. We use this version:

In our COQ code, it is expressed as:

Composed sums and products

Given two monic polynomials in K[X], P = aiX i with roots α1, . . . , αm in L and Q = bj X j with roots β1, . . . , βn in L, we wish to compute a polynomial whose roots are αi + βj for (i, j) ∈ {1, . . . , m}×{1, . . . , n}, which we write P ⊕Q and which we call composed sum. Similarly we define the composed product P ⊗Q, whose roots are αiβj for (i, j) ∈ {1, . . . , m}×{1, . . . , n}.

Since P and Q are supposed monic, am and bn are equal to 1, and we can split the polynomials in L[X]. We write abusively P = i (Xαi) and Q = j (Xβj ), and we want to compute the results

Since, both P ⊕ Q and P ⊗ Q are symmetric in the αi and βi, the fundamental theorem of symmetric polynomials concludes that their coefficients are polynomials in the coefficients of P and Q. We can compute P ⊕ Q and P ⊗ Q without the need for factoring P or Q. One solution is to use the resultant (which is already implemented for the construction of algebraic numbers (Cohen 2012b)) thanks to the relations:

where m is the degree of P . Note that P (

The Newton power series enables us to compute (P ⊕ Q)(X) and (P ⊗ Q)(X) faster for any characteristic of K. The Newton representation of a polynomial is a FPS. If this FPS is truncated far enough, there is no loss of information about the input polynomial. Then, the composed sum and composed product are done in the space of TFPS.

We formally prove the following equation for the composed product

where ⊙ denotes the Hadamard product, i.e. the term-wise product of TFPS.

In COQ:

Definition cmul (p q : {poly K}) := if (p == 0) || (q == 0) then 0 else \prod_(r <-[seq s * t | s <-roots p ^iota, t <-roots q ^iota]) ('X -r%:P) Lemma newton_cmul m p q : newton_tfps m (cmul iota p q) = (hmul_tfps (newton_tfps m p) (newton_tfps m q)) ^iota.

The proof of (8) boils down to proving the equality of the coefficients of two FPS.

Proof.

With our example we have

We then compute

which we truncate at precision 2. Hence P ⊗ Q = X 2 -18, which is the expected result.

We formally prove the similar equation for the composed sum

where

In COQ:

Definition cadd_poly (p q : {poly K}) := if (p == 0) || (q == 0) then 0 else \prod_(r <-[seq s + t | s <-iroots p, t <-iroots q]) ('X -r%:P).

Lemma cadd_newton m p q : hmul_tfps (newton_tfps m (cadd_poly iota p q)) E = (hmul_tfps (newton_tfps m p) E * hmul_tfps (newton_tfps m q) E) ^iota.

The proof of ( 9) is also almost immediate.

Proof. First we have:

Thus (9) can be rewritten as:

which can be re-expressed in the following way:

The latter is a direct consequence of the morphism property of the exponential. This completes the proof of (9).

With our example we have

We then compute the backward transformation.

which we truncate at precision 2. Hence P ⊕ Q = X 2 + 6X + 7, which is the expected result.

Related Work

This work is mostly based on Alin Bostan's PhD thesis [START_REF] Bostan | Algorithmique efficace pour des opérations de base en Calcul formel[END_REF] for the mathematical results, that he develops with care in order to provide algorithms for computer algebra. In our paper we only study the theory for characteristic zero, while he does it for arbitrary characteristic.

In [START_REF] Chaieb | Formal power series[END_REF], the author describes a formalization of formal power series in ISABELLE/HOL as functions from natural numbers. He already provides formal derivative, division, composition, inverse, logarithm. He provides additional constructions such as arbitrary nth roots, compositional inverse, binomial FPS, trigonometric FPS. These constructions are done for arbitrary domain. Contrary to our work, [START_REF] Chaieb | Formal power series[END_REF] does not require polynomials and defines them as FPS. We define TFPS by exploiting an existing library about polynomials. In (Alasdair Armstrong 2014), the authors generalizes FPS by implementing them as functions from free monoids into dioids.

We rely on the code of P.-Y. Strub (Strub 2014) for the theory of polynomials on a decidable field, in order to get the list of roots of a polynomial in an algebraically closed field.

For the fractions, we follow up on a work by the first author [START_REF] Gonthier | A machine-checked proof of the odd order theorem[END_REF], where he describes a construction of the fraction field of an integral domain using a quotient construction. We expand this work in a slightly different way than (Strub 2014) does, by generalizing the notion of pole and evaluation to an arbitrary integral domain.

We also use the existence of the algebraic closure to conclude that the resulting polynomial has the desired properties (Cohen 2012b,a).

Conclusion and future work

In this paper, we describe a formalization of truncated formal power series. We equip them with a commutative ring structure and define some common operations: Hadamard product, derivative, primitive, composition, exponential, logarithm and prove formulas linking these operations. The theory of truncated power series is both an artifice to avoid handling FPS as infinite objects and a feature as it explicits the precision that the operations have. We hope that the theory of TFPS can be reused for a theory of Taylor series.

We also develop a theory of abstract poles of fractions to factorize code and improve readability, which generalizes the universal property of the field of fractions. The theory of abstract poles is used to develop the theory of evaluation of polynomial fractions in a modular way. It is used twice: once for the evaluation of polynomials, once for lifting of injective morphisms from polynomials to a field, to a morphism from polynomial fractions to a field.

We then use these components to define the Newton power series and prove the main results: forward transformation theorem, backward transformation, theorem linking composed product with the Hadamard product, formula linking the composed sum with the product.

Whatever implementation of algebraic numbers we pick, in order to implement the sum and product on algebraic numbers, one step is to compute the composed sum and product of two polynomials. In this paper we describe an efficient way to do so. We should now investigate efficient ways to select a root of the composed sum and products. Once we have more efficient pieces than in (Cohen 2012b) we may use the COQEAL library to provide computable versions of the algorithms we describe and formalized here and perform computations on algebraic numbers inside COQ.