Recherche démonstration : exp solution de y'=y

[invite7553e94d]

Bonjour à tous. En Terminale, notre prof a introduit la fonction exponentielle comme unique solution de


Puis il nous a balancé que cette fonction était une fonction puissance (x-> e^x) sans nous donner :
- la preuve de l'existence d'une fonction vérifiant (E)
- la preuve de l'unicité de exp
- la preuve de la continuité de exp
- la définition d'une fonction puissance (que signifie e^x pour e et x réels, sans passer par a^b=e^{b ln a} ?)
- la preuve que e^x=exp(x)

Par la suite, mes profs m'ont introduit la fonction exponentielle comme suit :

Et là tout est bon sur R.

Mais est-il possible de démontrer les cinq points précédent sans passer par une série, mais bien par exp unique solution de (E) ?
Si oui, pouvez-vous m'aider à y parvenir ? Merci.
-----

[GrisBleu]

Salut

- pour l'existence et l'unicite de l'exponentielle, tu as le theoreme de Cauchy Lipschitz qui prouve tout ca d'un coup.
- En terminal, on m'avait explique l'exponentielle sur R comme fonction invere du logarithme:
1) ln va de R+ sur R
2) ln est croissante strictement
il existe donc une fonction inverse, notons la exp(x), telle que ln(exp)=exp(ln)=Id
3) par ln(ab)=ln(a)+ln(b), tu as assez vite exp(a+b)=exp(a)exp(b)
4) par ln(exp)'=ln'(exp) exp'=1, et par ln(exp(0)=0 tu as bien tes deux conditions

avec tout ca tu as toutes les proprietes de exp. Pour finir exp(n)=exp(1+...+1)=exp(1)...e xp(1)=(exp(1))^n=e^n. Tu continu sur Z,Q puis R et je penses que ca doit rouler

++

[invite7553e94d]

- pour l'existence et l'unicite de l'exponentielle, tu as le theoreme de Cauchy Lipschitz qui prouve tout ca d'un coup.

Ok merci

- En terminal, on m'avait explique l'exponentielle sur R comme fonction invere du logarithme:
1) ln va de R+ sur R
2) ln est croissante strictement
il existe donc une fonction inverse, notons la exp(x), telle que ln(exp)=exp(ln)=Id
3) par ln(ab)=ln(a)+ln(b), tu as assez vite exp(a+b)=exp(a)exp(b)
4) par ln(exp)'=ln'(exp) exp'=1, et par ln(exp(0)=0 tu as bien tes deux conditions

avec tout ca tu as toutes les proprietes de exp. Pour finir exp(n)=exp(1+...+1)=exp(1)...e xp(1)=(exp(1))^n=e^n. Tu continu sur Z,Q puis R et je penses que ca doit rouler

Oui mais dans ce cas, toutes les propriétés de ln ne sont pas démontrées, et on revient aux mêmes questions.
Peux-tu démontrer 1) (pourquoi ln n'est-elle pas définie sur R_-) ? et 3) ?

[invite986312212]

pourquoi ln n'est-elle pas définie sur R_-) ?

si tu définis la fonction log comme primitive de 1/x, tu vois que si tu essaies de le définir à la fois pour des réels positifs et négatifs, tu vas avoir une singularité en zéro, puisque l'intégrale de 1/x diverge autour de zéro.

[A voir en vidéo sur Futura]

[invite7553e94d]

Certes, mais la courbe de la fonction inverse est symétrique, ainsi si on définit ln comme


et sachant que
on pourrait avoir (et non on a, attention aux conclusions attives)



Je sais bien que ln n'est pas définie sur R_-, mais je n'en ai pas la preuve. Sauf si on la définie comme fonction réciproque de la fonction exp, et là on tourne en rond ...

edit : avec l'intégrale de Riemann, une singularité en un point, ou même en un nombre infini dénombrable de point n'a (n'ont) pas d'influence.

[invite986312212]

tu vas avoir une singularité en zéro

que cela est mal dit... en fait c'est plus qu'une singularité. On devrait avoir or cette intégrale diverge (encore que là on pourrait dire que c'est zéro par symétrie, mais si on remplace 1 par 0.5 rien ne va plus).

[invite7553e94d]

Tu as parfaitement raison, mais ça ne donne qu'une vague idée de preuve, pas une preuve

[invite5f448492]

En fait, on peut définir exp(x) comme la limite de (1 + x/n)^n (si je ne me trompe pas).
Et toutes les propriétés se trouvent en encadrant sauvagement (avec l'inégalité de Bernoulli et choses du même genre).

(oui c'est assez vague, mais ça marche).

[invite7553e94d]

Ca revient sensiblement au même que ça

Par la suite, mes profs m'ont introduit la fonction exponentielle comme suit :

Et là tout est bon sur R.

au passage, est-ce que pour z complexe e^z = lim (1+z/n)ⁿ ?

[invite986312212]

Tu as parfaitement raison, mais ça ne donne qu'une vague idée de preuve, pas une preuve

mais une preuve de quoi au juste? on pourrait très bien définir une fonction pour x strictement négatif. Le fait est qu'on doit choisir son côté. C'est naturel de choisir le côté positif.

[invite7553e94d]

De deux choses l'une : soit je suis incompris, soit je comprends mal

[leg]

De deux choses l'une : soit je suis incompris, soit je comprends mal

bonjour prgasp77

et si tu étais y' = y
où y' = incompris
y=comprends mal

je plaisante, mes tes remarques sont interressantes
amicalement leg

[invite4ef352d8]

"puis R et je penses que ca doit rouler" >>> pas exactement.


on vérifie que pour tous x dans Q, exp(x) =e^x.

puis on définit : e^x= exp(x) pour x réel quelconque.


Pour x rationel, on peut le prouver (mais on pourrait aussi le prendre comme définition) pour x réel, il s'agit à priori de l'unique facon simple de définir a^b quand b est réel.

[invite7553e94d]

"puis R et je penses que ca doit rouler" >>> pas exactement.


on vérifie que pour tous x dans Q, exp(x) =e^x.

puis on définit : e^x= exp(x) pour x réel quelconque.


Pour x rationel, on peut le prouver (mais on pourrait aussi le prendre comme définition) pour x réel, il s'agit à priori de l'unique facon simple de définir a^b quand b est réel.

Tiens, je ne m'attendais pas à ça, mais ça me rassure. Selon toi, définir la fonction exp comme solution de (E) ou réciproque de ln définie elle-même comme primitive de 1/x s'annulant en 1, nous amène à un "manque" qui doit être couvert par une définition arbitraire.
Je ne suis donc pas fou ?

que cela est mal dit... en fait c'est plus qu'une singularité. On devrait avoir or cette intégrale diverge (encore que là on pourrait dire que c'est zéro par symétrie, mais si on remplace 1 par 0.5 rien ne va plus).

Et en applicant Challes,

[GrisBleu]

Salut

on vérifie que pour tous x dans Q, exp(x) =e^x.
puis on définit : e^x= exp(x) pour x réel quelconque.

En fait je pensais - c est intuitif - a quelque chose du genre
- exp est continue et e^x aussi (?)
- exp(x)=e^x sur Q
- Q est dense dans R
- donc on prolonge sur R et l egalite est toujours vraie

Pour prgasp77, je croyais que le ln etait deja defini pour toi.
- Si tu admets les proprietes du ln, les proprietes de exp suivent et comme c est une solution sur R de l equation differenteille et que cette solution est unique, tu as bien ta solution.
- Si tu veux redefinir le ln, je crois avoir oublie comment faire ca simplemement

++

[invitefc60305c]

Un truc... c'est quoi la différence entre exp(x) et e^x ???

[invitedef78796]

Bonjour à tous. En Terminale, notre prof a introduit la fonction exponentielle comme unique solution de


Puis il nous a balancé que cette fonction était une fonction puissance (x-> e^x) sans nous donner :
- la preuve de l'existence d'une fonction vérifiant (E)
- la preuve de l'unicité de exp
- la preuve de la continuité de exp
- la définition d'une fonction puissance (que signifie e^x pour e et x réels, sans passer par a^b=e^{b ln a} ?)
- la preuve que e^x=exp(x)

Par la suite, mes profs m'ont introduit la fonction exponentielle comme suit :

Et là tout est bon sur R.

Mais est-il possible de démontrer les cinq points précédent sans passer par une série, mais bien par exp unique solution de (E) ?
Si oui, pouvez-vous m'aider à y parvenir ? Merci.

Bonjour,

Si tu cherches une preuve parfaitement rigoureuse de tout ça sans passer par les séries entières, je te suggère (comme cela a déjà été fait dans ce sujet) de passer par les intégrales :

On définit pour tout x strictement positif :



ce qui nous définit naturellement une fonction dérivable sur vérifiant

Etape 1 : Equation fonctionnelle

On fixe un réel strictement positif y et pour tout x strictement positif elle aussi dérivable sur ayant pour dérivée qui est constante et s'annule en 0. Bilan : est nulle et



S'en déduisent toutes les autres relations fonctionelles et notamment :




Etape 2 : bijection de sur

ln est dérivable sur à dérivée strictement positive, elle est donc strictement croissante sur .

Ainsi, elle possède une limite finie ou en .

Supposons que ce soit une limite finie , alors avec la relation on aboutit à une absurdité en passant à la limite.

Donc la limite de ln en est . Avec la relation sur l'inverse, la limite en 0 de est .

Continue, réalise une bijection de sur ce qui définit rigoureusement une fonction exp(x) comme sa bijection réciproque.

Bon je vais couper dans un autre message, sinon ça va faire gros...

[invite35452583]

Bonjour à tous. En Terminale, notre prof a introduit la fonction exponentielle comme unique solution de


Puis il nous a balancé que cette fonction était une fonction puissance (x-> e^x) sans nous donner :
- la preuve de l'existence d'une fonction vérifiant (E)
- la preuve de l'unicité de exp
- la preuve de la continuité de exp
- la définition d'une fonction puissance (que signifie e^x pour e et x réels, sans passer par a^b=e^{b ln a} ?)
- la preuve que e^x=exp(x)
[...]

Mais est-il possible de démontrer les cinq points précédent sans passer par une série, mais bien par exp unique solution de (E) ?
Si oui, pouvez-vous m'aider à y parvenir ? Merci.

Bonjour,
1er point : peut-on le montrer rigoureusement en Terminale ? Non comme tout théorème utilisant la complétude de IR (valeurs intermédiaires, Rolle, convergence de suites adjacentes, monotones bornées...).
Peut-on définir (avec une preuve relativement élémentaire) exp comme unique solution de (E) :
wlad_von_tokyo propose le théorème de Cauchy-Lipschitz. Je suis d’accord sur le fait que l’équation différentielle définissant exp vérifie hypothèse et conclusion de ce théorème, mais il me semble que l’on ne peut pas dire que l’on applique ce théorème pour montrer l’existence et l’unicité de exp par ce biais. Le hic est, si mes souvenirs sont bons, est que la preuve de ce théorème utilise l'exponentielle elle-même. Les démos que je connais à quelques changements près définissent des e-solutions (ly'-f(x,y)l<e sur un intervalle) puis montre la méthode d'Euler définit des e-solutions (e dépendant du pas en tendant vers 0 avec celui-ci) puis majore les e-solutions s'annulant en un point (en appliquant, via passage à la limte de e, à deux solutions exactes on en déduit l'unicité, en appliquant à une suite de fonctions définies précédement on montre l'existence de solutions). La 1ère majoration peut très bien se passer de l'exponentielle, la seconde utilise celle-ci et je ne sais pas si on peut s'en passer (à moins de compliquer inutilement).
Peut-on néanmoins le montrer sans marteau-pilon ? Oui
unicité : y1 et 2 deux solutions z=y1-y2 est solution de z'=z et z(0)=0.
z continue z'=z donc continue donc z uniformément continue sur un intervalle [0,a]
e>0 d tel que lx-x'l<d=lz'(x')-z'(x)l<e on majore par le théorème des accroissements finis
z(d)<de (lz'(d)l<de)
lz(2d)-z(d)l< (de+e) d=e(d+d²)
... on prend d <1 et a/d=N entier
lz(d)l<lz(2d)l<...<lz(Nd)l=lz( a)l<e(d+d²+...+d^N)<e/(1-d)
On fait tendre e et d vers 0 on aboutit à z=0 sur [0,a]
Existence : le théorème général utilisant l’exponentielle il faut construire celle-ci de manière autre. La série susnommée est un exemple de preuve d’existence.
Sinon la méthode d’Euler donne : yN(0)=1 yN(1/N)=1+1/N yN((k+1)/N)=yN(k/N)+1/Ny’(k/N)=(1+1/N)y(k/N)=(1+1/N)^(k+1), yN est affine sur les intervalles [k/N (k+1)/N]
YN est strictement croissante
N=2^n Y(2^(n+1))>y(2^n)
Les fonctions yN sont bornées sur Q par une même fonction 3^x définie ainsi 3^(p/q)=racine q-ème de 3^p pour tout p/q rationnel (sans ambiguïté p/q=p’/q’=>3^(p/q)=3^(p’/q’))
(1+1/N)^(k/N)=((1+1/N)^N)^k
(1+1/N)^N=1+N.1/N+(N(N-1)/2)(1/N²)+(N(N-1)(N-2)/6)(1/N²)+…+(N(N-1)…(N-k+1)/k !)(1/N^k)+…+N(N-1)…1/N !(1^N^N)<1+1+1/2+1/3 !+…+1/k !+…+1/N !<1+1+1/2+1/2²+1/2^3+…+1/2^(k-1)+…+1/(2^(N-1))<1+1+1/2+1/4+1/8+1/16+….=3
Pour x de la forme p/2^h, ce qui précède montre que y(2^n)(x) converge. Les (y(2^n)(x)) pour les autre réels sont alors aussi majorées donc ça converge.
Ensuite par argument diagonal : calcul de la pente (y(x’)-y(x))/(x’-x) en décomposant y(x’)-y(x)=[y(x’)-y(2^n)(x’)] + [y(2^n)(x’)-y(2^n)(x)] + [y(2^n)(x)-y(x)], on montre que y’=y.
Autres voies lim (1+x/n)^n comme évoquée avant, ….
En fait la méthode qui me paraît la plus simple et la plus propre est de montrer l’existence de l’exp en utilisant comme définition l’équation (E) montrer que la fonction réciproque de ln est une solution (cf post d'Ice DL)et en utilisant ce qui précède (uniquement partie « unicité ») pour montrer que exp est bien l’unique solution de (E).

Le 3ème point exp continue car exp dérivable (ce point au moins est simple)

4ème et 5ème point
Une puissance peut être définie comme un a^x ce qui ne fait pas grandement avancer les choses ici. Une propriété de ces fonctions est celle-ci : elle transforme les sommes en produits f(a+b)=f(a)f(b) (autrement dit c’est un morphisme du groupe additif dans le groupe multiplicatif). On a f(0)=1 ou f est nulle partout car f(0)=f(0+0)=f(0)f(0)=f(0)² donc f(0)=0 ou 1 ; or si f(0)=0 on a f(x)=f(x+0)=f(x)f(0)=f(x)0=0 pour tout x ce qui n’est guère intéressant.
Est-ce une bonne « modification » de la « définition ». Les fonctions a^x sont aussi des morphismes, les morphismes non nuls sont-ils tous de cette forme a^x ?
Sur Q : oui on pose g=ln(f) alors g est un morphisme du groupe additif (f >0 car f(a)=f(a/2+a/2)=f(a/2)² f(a)=0=>f=0 car f(b)=f(a+(b-a)=…) (cf fonction additive de R dans R dans contre-exemples) g=ax et f=exp(a)^x
Sur R, g est additive d’où deux possibilités : soient f ou g ont un minimum de régularité ou alors f et g sont deux fonctions à haute teneur en exotisme (cf fonction additive "classiques""classiques parmi les classiques")
Résultat : toute fonction puissance non exotique est de la forme a^x (a>0), c’est à dire coïncide avec a^r sur Q et est égal sur R à l’unique extension agréable de cette dernière fonction définie sur Q.
Exp (définie comme précédemment) est-elle une puissance : oui z=exp(a+x)/exp(a) vérifie l’équation (E) donc z=exp et exp(a+x)=exp(a)exp(x).
On peut aussi assez facilement le montrer si on définit exp comme fonction réciproque de ln, nettement plus délicat si on la définit à partir de la série (le plus simple est de passer par l’équa diff).
Exp est donc une fonction puissance donc de la forme e^x pour un certain e. (Ca se mord un peu la queue à ce niveau mais on peut reprendre et éviter le recours à l’exp et ln pour montrer le résultat précédent mais c’est plus fastidieux)

En espérant ne pas avoir été trop confus

[invite986312212]

allez, juste pour faire le cacou:

les morphismes non nuls (...)

... morphismes non identiquement égaux à 1

[invite4ef352d8]

"et e^x aussi " >>> ba c'est continu parcequ'on le définit comme etant égal a exp(x)... mais avant de faire ca ce n'est pas définit aux point irationel donc on peut pas parler de continuité !


apres c'est vrai, on doit pouvoir dire qu'on prolonge e^x a R par continuité : comme c'est déja définit sur Q le prolongement est unique, mais à mon avi il va etre assez difficile de prouver l'existence d'un tel prolongement sans passer par la fonction exponentielle avant ^^


"Un truc... c'est quoi la différence entre exp(x) et e^x ???"
>>> une fois que tous est définit absoluement aucune. mais au départ on définit deux objet différent : la fonction exponentielle de C dans C (qu'on définit par exemple avec la seri entiere, ou comme solution d'equation différentielle, ou comme réciproque de ln etc...) et la notation e^n, qui signifie e*e*e...*e n fois, qu'on prolonge pour n rationelle, en considerant les racines n-iemme.

[invite7553e94d]

Merci à IceDL et homotopie
J'ai eu plus de mal avec la démo de homotopie, mais les deux répondent à ma question, d'une certaine façon.

[invite52d2f307]

Je suis aussi en Terminale, et je peux t'apporter des réponses qui ne dépassent pas ce niveau.

L'existence de cette fonction est admise en terminale. La vraie démonstration se fait par la méthode d'Euler.

Son unicité se fait en terminale. Voici l'activité qu'on a fait dessus en cours :
Ici

Continue parceque dérivable, sinon, ça c'est immédiat.

En Terminale, on ne donne aucun sens à a^x, avec a et x réels. On connaissait lorsque x entier, mais sinon ça ne veut toujours rien dire en terminale, et faut passer par la la notation avec e et ln.

Enfin, e^x n'est qu'une contation de exp(x) en terminale. Rien d'autre.

Mais comme tu dis que "tes profs" t'ont introduit d'autres trucs, je suppose que t'es plus en terminale, mais quelque part en prépa, non ? Donc, j'espère que tu trouveras des réponses plus avancés ailleurs, mais au moins là tu connais les bases de ce qu'il faut acquérir en Terminale.

[invite7553e94d]

Merci Error, c'est bien gentil.

Mais au final, je n'ai aucun moyen de démontrer l'existance d'une solution de (E) même en définissant la fonction ln ?

[invitedef78796]

Merci Error, c'est bien gentil.

Mais au final, je n'ai aucun moyen de démontrer l'existance d'une solution de (E) même en définissant la fonction ln ?

Si !

Si tu pars de la définition de ln (j'aime bien la preuve d'homotopie ceci dit ), tu peux prouver (exercice) que exp est dérivable et que sa dérivée est égale à elle même (dériver ln(exp(x))=x).

Tu peux même démontrer l'unicité de la solution de (E) à partir de là.

[invite7553e94d]

Oui pardon, je me suis un peu mélangé ... Mais sans te fâcher, je vais rester sur la démo de homotopie qui correspond à ce que je recherchais.

À partir de là, je vais construire proprement exp, puis ln comme sa réciproque et démontrer qu'elle est une primitive de 1/x.

Et si l'envie me viens, je démontrerai que la définition de exp sur C par la limite d'une série est valable. Je posterai tout ça ici même un de ces jours.

Merci à vous deux.