OAI/NumberTheory/DirichletL/Descent/FirstMarkedColumns.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.cube_whole_column_norm line 15
2. def OAI.SevenEighths.InverseMoment.wholeMarkedTest line 32
3. theorem OAI.SevenEighths.InverseMoment.whole_marked_test_uniform line 36
4. theorem OAI.SevenEighths.InverseMoment.canonical_residual_norm line 61
5. theorem OAI.SevenEighths.InverseMoment.canonical_residual_test_nonzero line 68
6. theorem OAI.SevenEighths.InverseMoment.canonical_marked_residual_support line 75