OAI/NumberTheory/DirichletL/Descent/ReopenedBins.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.marked_column_zero_of_subunit line 12
2. theorem OAI.SevenEighths.InverseMoment.markedReopenedCubeBin_eq_active line 34
3. theorem OAI.SevenEighths.InverseMoment.markedReopenedCubeBin_log_bins line 53
4. def OAI.SevenEighths.InverseMoment.markedShortCompletedSum line 61
5. theorem OAI.SevenEighths.InverseMoment.original_marked_reopened_binned line 66
6. theorem OAI.SevenEighths.InverseMoment.original_marked_binned_energy line 78