OAI/NumberTheory/DirichletL/Inversion/InitialOverlapIdealFourier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseInitialOverlapIdealFourier.activeIndices line 15
2. theorem OAI.SevenEighths.InverseInitialOverlapIdealFourier.activeIndices_mem line 19
3. theorem OAI.SevenEighths.InverseInitialOverlapIdealFourier.indexed_mark_active line 25
4. theorem OAI.SevenEighths.InverseInitialOverlapIdealFourier.indexed_overlap_separation line 35
5. theorem OAI.SevenEighths.InverseInitialOverlapIdealFourier.indexed_overlap_integrable line 51
6. theorem OAI.SevenEighths.InverseInitialOverlapIdealFourier.tuple_gate_product line 60
7. theorem OAI.SevenEighths.InverseInitialOverlapIdealFourier.finite_ideal_overlap_separation line 80