je suis en train de revoir la construction de l'intégrale de Riemann. On prouve le théorème du changement de variable à travers le théorème fondamental de l'analyse (intégrale = différence de primitive). Est-ce qu'on peut démontrer le changement de variable à partir seulement de la définition de l'intégrale et de la dérivée??

Je sais pas trop si une autre démonstration aurait un intérêt car justement le théorème de changement de variable est une utilisation pratique du théorème fondamental de l'analyse, les sens mathématiques des 2 notions sont directement liées.

Au passage, tu me dois toujours une démo toi, décidément

liés* .... décidément

ben l'intérêt serait qu'on pourrait généraliser la formule de changement de variable là où le théorème fondamental ne s'applique plus.

Le théorème fondamental ne s'applique qu'avec une fonction continue et donc fait que la propriété de changement de variable ne s'applique que chez les fonctions de classe C1 alors qu'elle marcherait aussi pour de nombreuses fonctions qui sont pas C1.

Ce qui est sûr c'est que le théorème marche encore quand f est intégrable (et pas forcément continue) si phi est un C1-difféo

(FoPhi)' = Phi' * foPhi
int(a->b)((FoPhi)') = int(a->b)(Phi' * foPhi)
=> int(a->b)(Phi' * foPhi) = FoPhi(b) - FoPhi(a)
=> int(a->b)(Phi' * foPhi) = int(Phi(a)->Phi(b))

On utilise uniquement le fait que f est C° et Phi C1-difféo.
(je me trompe peut-être, j'ai pas trop compris ton 2ème poste )

(Ah oui, F est une primitive de f au cas où)

J'ai oublié une partie de la dernière ligne.
=> int(a->b)(Phi' * foPhi) = int(Phi(a)->Phi(b))(f)

Azk En faisant ça tu as justement utilisé le théorème qu'Amandin cherche à éviter, précisément à ta première implication.

Ouais, c'est ce qui m'a semblé aussi en relisant ses postes.
Ca aurait été trop facile.
(je bossais l'algèbre en même temps, difficile de passer de l'un à l'autre comme ça)

L'intégrale de Riemann de f sur un segment est la limite d'une certaine somme de f(ai)dxi où les (xi) forment une subdivision du segment et xi < ai < x(i+1)

Si on peut écrire les (xi) comme des g(ti), alors on se retrouver à sommer des f(ai)dg(ti)

Or le théorème des accroissements finis permet d'écrire dg(ti) comme un certain g'(ci)dti. En choisissant ai=g(ci), on obtient que l'intégrale de f s'écrit aussi comme limite d'une somme de f(g(ci))g'(ci)dti qui n'est autre que l'intégrale de (fog)*g'

Il reste à écrire ça plus proprement et à trouver les bonnes hypothèses sur f et g.

Klaus ça a l'air tellement simple comme démo, pourquoi ne la voit-on nulle part?? Elle est fausse??

fausse? Non avec les bonnes hypothèses elle est tout à fait correcte. En particulier on a besoin d'une hypothèse de monotonie sur f pour assurer le choix de ai=g(ci).

Si on veut généraliser à f non monotone il va falloir s'assurer qu'elle est quand même assez régulièrement monotone et au final on va se retrouver avec les même hypothèses que ceux du changement de variable classique.

En outre la démo utilise essentiellement le TAF qui est aussi essentiellement le seul nécessaire pour démontrer le théorème fondamental de l'analyse, donc autant démontrer ce dernier puis le changement de variable par ce dernier.

Mais ce n'est pas inintéressant d'avoir une preuve uniquement constructiviste. On pourrait de même démontrer par la définition la formule d'intégration par partie.

C'est inspiré de Riemann-Stieltjes Klaus ?

Pas vraiment ça y ressemble mais ce n'est pas la même idée.