OAI/Analysis/TriangularHilbert/CyclicMaxMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularHilbert.aemeasurable_cyclicMax line 11
2. def OAI.TriangularHilbert.rationalMoment line 17
3. lemma OAI.TriangularHilbert.rationalMoment_mono line 21
4. lemma OAI.TriangularHilbert.cyclicMax_rpow_eq line 29
5. lemma OAI.TriangularHilbert.aemeasurable_rationalMoment line 49
6. lemma OAI.TriangularHilbert.lintegral_cyclicMax_moment_le line 58