OAI/NumberTheory/DirichletL/Descent/ActualSecondEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseMoment.actualSecondChild line 16
2. def OAI.SevenEighths.InverseMoment.actualSecondTriples line 19
3. theorem OAI.SevenEighths.InverseMoment.actualSecondChild_nonzero line 23
4. structure OAI.SevenEighths.InverseMoment.ActualSecondSourceConditions line 40
5. theorem OAI.SevenEighths.InverseMoment.actual_second_fiber_weight line 51
6. theorem OAI.SevenEighths.InverseMoment.actual_second_energy_projection line 80
7. theorem OAI.SevenEighths.InverseMoment.actual_second_weighted_count line 111