Proposition 6

Tag 097F, permanent. Cite it as [Bourbaki, Tag 097F].

— Let $f$ be a numerical function $\geqslant 0$ defined on $T \times T'$ . Then

\iint^* f(t, t') d\mu(t) d\mu'(t') \geqslant \int^* d\mu(t) \int^* f(t, t') d\mu'(t').

This follows from Prop. 3 of §3, No. 2, on taking (2) into account.

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.

Cited by