OAI/NumberTheory/DirichletL/Detector/HighRowsLocal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.rowHighPrimeTerm line 12
2. def OAI.SevenEighths.ProbePhysical.idealRowHighLocalFactor line 16
3. lemma OAI.SevenEighths.ProbePhysical.rowHighPrimeTerm_summable_norm line 20
4. lemma OAI.SevenEighths.ProbePhysical.rowHighPrimeTerm_zero_of_two_le line 27
5. theorem OAI.SevenEighths.ProbePhysical.rowHighPrimeTerm_tsum_eq_localFactor line 35
6. theorem OAI.SevenEighths.ProbePhysical.bareIdealHighSeries_row_hasProd_localFactor line 52
7. theorem OAI.SevenEighths.ProbePhysical.excludedRowHighLocalFactor line 60
8. theorem OAI.SevenEighths.ProbePhysical.excludedIdealHighSeries_row_hasProd_outside line 80