Il faut que je mette plus en avant en calcul intégral le résultat concernant le fait qu'une intégrale indétérminée est dérivable presque partout (classiquement) avec comme dérivée son intégrande (donc sans doute le virer de l'annexe, montrer pourquoi ça a du sens dans les cas simples (tels que : C^0 + C^1 par morceaux), et peut-être inclure la preuve en annexe). C'est un résultat qui n'est pas dur à comprendre (même si sa démo est dure), qu'on peut appliquer directement et qui repointe très souvent le bout de son nez (proba, calcul intégral, dans les preuves + ou - profondes, etc.) ensuite, plus que ce que j'avais anticipé.
Je pense qu'il faut accepter en proba des densités positives presque partout uniquement. C'est particulièrement flagrant quand on (re)définit tardivement les densités comme les dérivées faibles de fonctions de répartition (les valeurs de la dérivée faible sur un ens. négligeable n'ont pas de raison a priori d'être positives dans ce contexte).
Je pense qu'il est possible d'améliorer la remarque en proba concernant la non-unicité de la densité (le warning reste tout à fait approprié) en fournissant une manière de rendre canonique la fonction f (qui est instructive en soi) plutôt qu'un exemple arbitraire pour en générer d'autres. On fait comma ça : soit la valeur moyenne de $f$ sur [x-h, x+h] tend vers une valeur finie quand $h$ tend vers $0$ (c'est ce qu'on appelle un point de Lebesgue, ça doit arriver presque partout d'après les résultats sur la dérivée d'une intégrale indéterminée -- cf supra -- et la valeur limite est pp f(x)) et on prend ça comme "nouvelle valeur nettoyée" de f, soit la limite est infinie ou indéfinie et on prend 0 (par exemple). Ce procédé rend en particulier les fonctions f continues (quand une telle densité continue existe) ; c'est un "filtrage" régularisant. La construction pourrait apparaître en remarque, les éléments de preuve en exo (par exemple).
P.S. : la "canonicalisation", c'est aussi une façon d'éviter de se prendre la tête à ce stade avec la manipulation de classes d'équivalence de fonctions égales presque partout tout.
Plusieurs considérations liées :
Il faut que je mette plus en avant en calcul intégral le résultat concernant le fait qu'une intégrale indétérminée est dérivable presque partout (classiquement) avec comme dérivée son intégrande (donc sans doute le virer de l'annexe, montrer pourquoi ça a du sens dans les cas simples (tels que : C^0 + C^1 par morceaux), et peut-être inclure la preuve en annexe). C'est un résultat qui n'est pas dur à comprendre (même si sa démo est dure), qu'on peut appliquer directement et qui repointe très souvent le bout de son nez (proba, calcul intégral, dans les preuves + ou - profondes, etc.) ensuite, plus que ce que j'avais anticipé.
Je pense qu'il faut accepter en proba des densités positives presque partout uniquement. C'est particulièrement flagrant quand on (re)définit tardivement les densités comme les dérivées faibles de fonctions de répartition (les valeurs de la dérivée faible sur un ens. négligeable n'ont pas de raison a priori d'être positives dans ce contexte).
Je pense qu'il est possible d'améliorer la remarque en proba concernant la non-unicité de la densité (le warning reste tout à fait approprié) en fournissant une manière de rendre canonique la fonction f (qui est instructive en soi) plutôt qu'un exemple arbitraire pour en générer d'autres. On fait comma ça : soit la valeur moyenne de $f$ sur [x-h, x+h] tend vers une valeur finie quand $h$ tend vers $0$ (c'est ce qu'on appelle un point de Lebesgue, ça doit arriver presque partout d'après les résultats sur la dérivée d'une intégrale indéterminée -- cf supra -- et la valeur limite est pp f(x)) et on prend ça comme "nouvelle valeur nettoyée" de f, soit la limite est infinie ou indéfinie et on prend 0 (par exemple). Ce procédé rend en particulier les fonctions f continues (quand une telle densité continue existe) ; c'est un "filtrage" régularisant. La construction pourrait apparaître en remarque, les éléments de preuve en exo (par exemple).
P.S. : la "canonicalisation", c'est aussi une façon d'éviter de se prendre la tête à ce stade avec la manipulation de classes d'équivalence de fonctions égales presque partout tout.