OAI/NumberTheory/DirichletL/Descent/SecondSupportedEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.ActualSecondSourceConditions.mono line 16
2. def OAI.SevenEighths.InverseMoment.actualSecondSurvivingSource line 27
3. theorem OAI.SevenEighths.InverseMoment.assignedSecondSource_mono line 31
4. theorem OAI.SevenEighths.InverseMoment.actualSecondTriples_mono line 39
5. theorem OAI.SevenEighths.InverseMoment.actual_second_supported_marked_energy line 44