Tu y écris
Par $\sigma$-additivité de la mesure $\mu$, on a donc
$$
\lim_{n \to + \infty} \mu\left(f^{-1}\left([2^{-n}, +\infty]\right)\right)
\mu\left(f^{-1}\left(\left]0, +\infty\right]\right)\right).
$$
L'ellipse peut paraître un peu violente. Tu pourrais ajouter que
$f^{-1}\left([2^{-n}, +\infty]\right) = \bigcup_{i=1}^n f^{-1}\left(\left[2^{-n},2^{-(n-1)}\right[\right) f^{-1}\left(\bigcup [1,+\infty]\right)$
est une décomposition en ensembles disjoints ?
Sinon en proba 1, on a un résultat similaire que l'on appelle la continuité croissante que tu pourrais intercaler (dans une version adaptée) si besoin.
OK. J'ai externalisé ce que tu suggérais en annexe (localement ça casse le flot de la démo, c'est trop long) et puis c'est effectivement un résultat en soi.
Tu y écris Par $\sigma$-additivité de la mesure $\mu$, on a donc $$ \lim_{n \to + \infty} \mu\left(f^{-1}\left([2^{-n}, +\infty]\right)\right)
\mu\left(f^{-1}\left(\left]0, +\infty\right]\right)\right). $$ L'ellipse peut paraître un peu violente. Tu pourrais ajouter que $f^{-1}\left([2^{-n}, +\infty]\right) = \bigcup_{i=1}^n f^{-1}\left(\left[2^{-n},2^{-(n-1)}\right[\right) f^{-1}\left(\bigcup [1,+\infty]\right)$ est une décomposition en ensembles disjoints ? Sinon en proba 1, on a un résultat similaire que l'on appelle la continuité croissante que tu pourrais intercaler (dans une version adaptée) si besoin.