Soit A un anneau et B un sous anneau de A, vérifiant la propriété (P):
"Pour tout x de A, si x^k est dans B pour tout k assez grand, alors x est dans B"
Alors l'anneau B[[X]] des séries formelles a coeff dans B, vu en tant que sous anneau de A[[X]], vérifie la même propriété (P).
Ce lemme est un exercice en soi, et il n'y a pas besoin de connaitre quoi que ce soit sur les séries formelles si ce n'est la def d'un produit. La démo c'est juste des récurrences et des bidouilles.
Son utilisation est la suivante : Posant U l'ouvert ou on a montré que f est C infinie, à une fonction g C infinie de U on associe la série formelle
(dont les coeff sont donc des fonctions)
On vérifie par du Leibnitz que S est multiplicative et donc que pour tout k S(f^k)=S(f)^k. Or on sait que pour k assez grand, f^k est C infinie, ce qui entraine donc une certaine régularité sur les coeffs de S(f)^k, qui grace au lemme va entrainer une certaine régularité pour les coeffs de S(f), ce qui pourra permettre ensuite de conclure. Plus précisément, on peut appliquer le lemme avec par exemple
- A={fonctions C infinies sur U} ( ou bien juste l'ensemble des fonctions définies sur U..l'anneau A qu'on choisit n'est pas bien important )
- B={fonctions de A bornées sur [-1,1]}, mon [-1,1] étant évidemment arbitraire..
Ainsi, le lemme entraine que les coeffs de S(f) sont dans B, ie que les dérivées de f sur U inter [-1,1] sont bornées, ce qui entraine quelques accroissements finis plus loin que f est C infinie sur [-1,1].
Voilà tu comprend maintenant pourquoi je trouvais ça un peu rude de poser l'exo sans indics^^