OAI/NumberTheory/DirichletL/Detector/RowReflectedAllocation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.prod_rpow_nonneg line 19
2. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.selected_exponent_allocation line 30
3. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.allocation_of_deficit line 37
4. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.prime_norm_ge_one line 65
5. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.original_row_conductor_le line 68
6. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.original_row_deletion_radical_le line 75
7. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.row_same_primitive_allocation line 90
8. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.actual_multiplicity_divisor line 111
9. lemma OAI.SevenEighths.ProbeRowReflectedAllocation.actual_ideal_multiplicity line 118
10. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.buffered_reflected_right_bound line 126
11. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.central_deletion_bound line 160
12. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.buffered_same_primitive_reflected line 192
13. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.source_calibrated_reflected_allocation line 229
14. theorem OAI.SevenEighths.ProbeRowReflectedAllocation.source_actual_valuation_reflection line 308