OAI/NumberTheory/DirichletL/Descent/Poisson.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.ideal_divisibility_local_zeroMark line 22
2. theorem OAI.SevenEighths.InverseMoment.actual_marked_active_eq line 35
3. theorem OAI.SevenEighths.InverseMoment.actual_marked_active_norm line 45
4. theorem OAI.SevenEighths.InverseMoment.actual_marked_active_formula line 57
5. theorem OAI.SevenEighths.InverseMoment.actual_marked_gauss_phase_norm line 74
6. theorem OAI.SevenEighths.InverseMoment.row_slot_cross_phase line 93
7. theorem OAI.SevenEighths.InverseMoment.row_slot_product_phase line 116
8. theorem OAI.SevenEighths.InverseMoment.canonicalSourceCoefficient_mark_priority line 128
9. theorem OAI.SevenEighths.InverseMoment.marked_disjoint_source_poisson line 143