OAI/NumberTheory/DirichletL/Descent/Grid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseMoment.gridCommonSupport line 14
2. theorem OAI.SevenEighths.InverseMoment.finite_triple_support_reindex line 17
3. def OAI.SevenEighths.InverseMoment.HybridColumnData.gridIndex line 47
4. theorem OAI.SevenEighths.InverseMoment.HybridColumnData.gridIndex_injective_on_square line 50
5. def OAI.SevenEighths.InverseMoment.hybridGridSupport line 65
6. theorem OAI.SevenEighths.InverseMoment.hybrid_grid_reindex line 68
7. theorem OAI.SevenEighths.InverseMoment.gridCommonSupport_origin line 83