Démonstration.
Traitons d’abord le cas des intégrales sur .
On a ,
puisque . Et comme
contient le support de
, cette dernière intégrale est égale
à ;
on procède de même pour les intégrales sans valeurs absolues,
dans le cas intégrable.
Venons-en maintenant au cas de .
Soit
un atlas intégral sur adapté à ,
tel que chacun des tropicalise
également (ou ,
ce qui est pareil).
On a
,
et , et
les égalités analogues sans
valeurs absolues dans le cas intégrable.
Pour tout , le support de la forme
est contenu dans ;
d’après le paragraphe 3.9.4,
on a donc
|
|
|
ainsi que les égalités analogues sans valeurs absolues.
Quitte à remplacer
par , par et par ,
on peut donc supposer que est compact et
que et sont tropicales, définies
par un moment .
Posons , . Soit
la -forme mesurable sur telle que .
On a et .
Par définition,
|
|
|
Par ailleurs, soit un recouvrement de
par des ouverts relativement compacts, une partition
de l’unité subordonnée au recouvrement
formée de fonctions lisses à supports compacts
et, pour tout , un polytope compact de
voisinage dans du support de .
On a alors
|
|
|
En outre, on a
|
|
|
Alors, la famille
est un atlas intégral sur adapté à .
On a donc
|
|
|
d’où l’égalité .
Dans le cas intégrable, la preuve de l’égalité
est identique,
en enlevant les valeurs absolues du calcul précédent.
∎