Exponentielle pour mémo

L’existence est faite par la construction $x\mapsto \lim_{\infty} (1+\frac{x}{n})^n$, non ?

Je pense au fait que la méthode « de la limite » fonctionne car on utilise le caractère complet de $\mathbb R$ (ou encore « suite croissante majorée converge »).

Et sinon, c’est de l’artillerie lourde mais le Théorème de Cauchy-Lipschitz est une théorème d’existence (puis d’unicité).
Ça utilise encore un espace complet (et le théorème du point fixe de Picard).
Mais j’en conviens, ça sort du cadre…

Exact !

La différence entre "non constructive" et "constructive" n'est elle pas un peu ambigue?
Considère t-on que faire la limite d'une suite comme $(1+x/n)^n$ c'est constructif?
Considére t-on que le résumé de construction donné par cc est constructif? Le fait que $10^\pi$ est la limite de la suite $10^3, 10^{31/10}, 10^{314/100}$ où par ex $10^{314/100}$ est l'unique solution de $x^{100}=10^{314}$, c'est constructif?
Considére t-on que Cauchy-Lipshtitz c'est constructif? (la solution est donné comme limite d'une suite définie par une récurrence explicite)

Relisant le message de Christophe, comme d’habitude je n'ai rien compris à ses blabla et je ne vois absolument pas comment traiter son « Étape 1», et je suspecte une erreur dans son blabla, qui me semble supposer ce qu'il demande de prouver plus loin, que $f$ ne s'annule pas. Bref, encore des
« leçons de ténèbres ».

De toutes manières comme l'a écrit Cyrano, ceci ne prouve pas l'existence de la fonction $f$. L'unicité se prouve en effet plus simplement, on peut dire que c'est « facile » mais encore faut-il y penser. Moi je poserais $g(x)=f(x)f(-x)$, et en dérivant on voit que $g$ est constante, d'où $f(x)f(-x)=1$ pour tout $x$ réel, et $f$ ne s'annule pas. Alors si $f_1$ est une autre fonction satisfaisant à : $\forall x \in \mathbb R, f_1'(x)=f_1(x)$ et $f_1(0)=1$, la fonction $x\mapsto \frac {f_1(x)}{f(x)}$ est constante, égale à $1$.

Avec les mêmes idées, on peut prouver l'équation fonctionnelle de l'exponentielle. Pour chaque $a \in \mathbb R$, la fonction $x\mapsto \frac {f(x+a)}{f(x)}$ est constante, d'où $f(x+a)=f(x)g(a)$, et puis $g=f$. On retrouve les considérations de Christophe, mais moyennant le fait que $f$ ne s'annule pas. On peut aussi considérer $x \mapsto f(x)f(a-x)$, qui n'exige pas cette propriété de non- annulation.

Pour l'existence je vois deux possibilités.

Avec ce que j'ai dit il est clair que si $f$ existe, alors ce sera une fonction strictement croissante, de dérivée $>0$ avec les limites connues en $+ \infty$ et $-\infty$. Elle aura donc une fonction réciproque, qui sera la primitive de $ x\mapsto \frac 1x$, et celle-ci, elle existe.

Autre méthode. Développement en série sans le dire, qu'on peut présenter de plusieurs façons.
On peut exécuter une suite d'intégrations par parties pour prouver la formule de Taylor avec reste intégral, juste dans ce cas particulier.
On peut aussi faire une suite d'intégrations avec encadrement. Je pose $f(x)=e^x$.
Si $x>0$, alors d'abord : $\displaystyle 0\leq \int_{0}^{x}e^{t}dt\leq \int_{0}^{x}e^{x}dt$, soit : $0\leq e^{x}-1\leq xe^{x}$.
$~~~$Intégration encor : $ \displaystyle 0\leq \int_{0}^{x}(e^{t}-1)dt\leq \int_{0}^{x}te^{t}dt\le \int_{0}^{x}te^{x}dt$, soit : $0\leq e^{x}-1-x\leq \frac{x^{2}}{2}e^{x}$.
Et ainsi de suite jusqu'à : $\displaystyle 0\leq e^{x}-\underset{k=0}{\overset{n}{\sum }}\frac{x^{k}}{k!}\leq \frac{x^{n+1}}{(n+1)!}e^{x}$. D'où : $\displaystyle e^x = \lim_{n \rightarrow +\infty } \underset{k=0}{\overset{n}{\sum }}\frac{x^{k}}{k!}$, qu'on ne notera pas $\displaystyle e^x = \underset{k=0}{\overset{+\infty}{\sum }}\frac{x^{k}}{k!}$ si ça défrise.

Bonne journée estivale, enfin.
Fr. Ch.

La construction des fonctions puissances à partir des puissances d'exposants rationnels est traitée en détail dans N.Bourbaki: Topologie générale (où dans fonctions d'une variable réelle? je n'ai pas ces livres sous la main présentement).

Je traduis l'étape 1 de CC si ça peut intéresser quelqu'un... Chaurien peut-être.

Il faut montrer que la fonction $(x,y)\mapsto \frac{f(x+y)}{f(y)}$ ne dépend pas de $y$. Donc on calcule la dérivée partielle de cette fonction par rapport à $y$ et on trouve :
$$
\frac{f'(x+y)f(y)- f(x+y)f'(y)}{f^2(y)}=\frac{f(x+y)f(y)- f(x+y)f(y)}{f^2(y)}=0.

$$ Bon lui il a préféré "$a$" et "$x$" au lieu de "$x$" et "$y$". Donc le $blabla$ c'était $f^2(y)$ cool.

PS. Si vous en avez marre des exo traditionnels essayez de traduire CC, il y a plusieurs bénéfices à en tirer : ça vous fait passer le temps, vous contribuez à rendre CC plus ou moins compréhensible et ce dernier point lui permettra de se sentir un membre à part entière du forum. Bref vous aurez accompli une œuvre de bien qui vous fera sentir mieux. B-)-

Il faut cependant prouver dans un premier temps que f ne s'annule pas pour faire fonctionner cet argument

@ Raoul.S
Sauf qu'il faut prouver que $f$ ne s'annule pas, comme je l'ai lourdement signalé. Ce n'est pas un détail...

Précisions sur la présentation en Terminale des fonctions $\exp$ et $\ln$.
Je n'ai pas compris pourquoi on a voulu opter pour cette présentation d'une fonction $f$ telle que $f'=f$ et $f(0)=1$. Je présume que pour l'existence, il était prescrit de recourir à une méthode approchée (Euler) qui donne une idée de cette existence, sans rien prouver.
Bon, ce n'est pas un scandale d'admettre certaines choses, pourvu que ce ne soit pas trop souvent. Mais pourquoi avoir renoncé à commencer par le log, avec la définition classique : $\ln x= \int_1^x \frac{dt}t$ ?
Si l'on veut « motiver », on peut adopter une approche fonctionnelle, et annoncer qu'on cherche une fonction qui transforme les multiplications en additions, ce qui était du plus haut intérêt avant l'apparition des calculatrices. C'est ainsi que procédait André Delachet dans son « Que Sais-Je ? », qui reste toujours intéressant.
On cherche donc une fonction $f:\mathbb R_+^* \rightarrow \mathbb R$ telle que : $\forall x\in \mathbb R_+^*, \forall y \in \mathbb R_+^*, f(xy)=f(x)+f(y)$.
C'est une des quatre équations fonctionnelles de Cauchy.
On peut supposer $f$ dérivable, et on obtient tout de suite $f(x)= \int_1^x K\frac{dt}t$, où $K$ est une constante.
Avec des élèves avancés, on peut prolonger la question : chercher à définir $f$ sur $\mathbb R$, sur $\mathbb R^*$ ; supposer seulement $f$ continue, ou continue en un point, etc.
Bonne journée.
Fr. Ch.

[Un document] qui reprend quelques points de vue exprimés dans ce fil.

@Foys : C'est là qu'on se rend compte à quel point il est difficile d'avoir une approche rigoureuse et "self-contained" en secondaire, même avec ceux qui ont le plus grand nombre d'heures de maths par semaine. (Chez nous, ça peut aller jusqu'à 8).

Que ce soit ton approche pour introduire le logarithme en premier, ou bien celle avec des suites adjacentes (que ce soit la série ou bien $(1+x/n)^n$), tôt ou tard, il faut faire intervenir la notion de borne supérieure, ... qui n'est pas au programme.
Quand j'y pense, c'est hallucinant. Comment faire de l'analyse (c'est à dire étudier $\R$ et donc intrinsèquement la propriété de la borne supérieure) si on ne peut même pas parler de la notion.

EDIT : Quand j'y pense, on pourrait juste dire que la proposition "toute suite croissante et majorée admet une limite" est un axiome. De toute façon, il faut bien un axiome quelque part, sauf à construire explicitement $\R$ en secondaire, ce qui est pour le coup franchement inenvisageable.

@Magnéthorax : On vient de penser à la même chose en même temps. :-D

@Cyrano: la borne sup, c'est la première notion pour laquelle on ne peut plus faire semblant avec les quantifications.
Pour les limites à la rigueur on peut "programmer" l'élève à coups de hacks pour lui faire faire des rédactions calculatoires justes sans comprendre ("x est non nul donc je peux écrire ceci-cela") mais pour les sups/infs ça ne marche plus même si la notion est moins complexe in fine.

Si on a vraiment que les suites croissantes majorées, passer par la suite des $(1+x/n)^n$ ou les polynômes de Taylor semble effectivement être la solution la plus raisonnable, bien que ces suites semblent sorties du chapeau à ce stade.

Oui, c'est in fine la méthode la plus simple.
On admet l'axiome des suites croissantes majorées, on démontre la propriété des suites adjacentes, on démontre en lemme l'inégalité de Bernoulli par récurrence (bonne idée d'ailleurs puisqu'on est censé exercer les élèves à la récurrence en terminale). On montre que les suites $(1+x/n)^n$ et $(1-x/n)^{-n}$ sont adjacentes en montrant que le quotient tend vers $1$ et puis on continue comme dans le document de gai requin.

@Foys : Théoriquement, on est aussi censé faire du $\epsilon, \eta$ rigoureux lorsqu'on introduit les limites. Par exemple il faut démontrer avec la définition que $1/x \to 0$ lorsque $x \to +\infty.$ Il suffit bien sur de poser $\eta = 1/\epsilon$ mais je ne sais pas combien de profs le font réellement.

Cette suite fait le job niveau TS et on a même [la formule d'Euler] en corollaire sans trop forcer.

Effectivement tout ça est probablement trop théorique pour les Terminales. Cependant ça peut être intéressant pour l'enseignement L1 qui tout en étant supérieur a suffisamment faibli pour qu'un cours "Terminale+" soit adapté, au moins au premier semestre.