OAI/NumberTheory/Ostmann/QuadraticCenter/IncidenceFactorial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.descFactorial_le_pow_mul line 8
2. theorem OAI.Ostmann.QuadraticCenter.card_incident_tuples line 16
3. theorem OAI.Ostmann.QuadraticCenter.small_rows_moment_bound line 21
4. theorem OAI.Ostmann.QuadraticCenter.high_rows_moment_lower line 39
5. theorem OAI.Ostmann.QuadraticCenter.moment_le_pow_mul_total line 54
6. theorem OAI.Ostmann.QuadraticCenter.exists_large_row line 72