OAI/Analysis/LpDimension/SymmetricLaws.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.averageLaw line 14
2. instance OAI.SubpolynomialLp.averageLaw_probability line 17
3. lemma OAI.SubpolynomialLp.averageLaw_integrable line 23
4. lemma OAI.SubpolynomialLp.averageLaw_integral line 31
5. lemma OAI.SubpolynomialLp.averageLaw_ae line 37
6. def OAI.SubpolynomialLp.symmetricLaw line 44
7. instance OAI.SubpolynomialLp.symmetricLaw_probability line 47
8. lemma OAI.SubpolynomialLp.symmetricLaw_symmetry line 53
9. lemma OAI.SubpolynomialLp.symmetricLaw_ae line 62
10. lemma OAI.SubpolynomialLp.symmetricLaw_even_integral line 72