OAI/NumberTheory/DirichletL/Detector/HighRowsSummability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbePrimePower.geometric_indicator_summable line 12
2. lemma OAI.SevenEighths.ProbePrimePower.gaussValuationTable_geometric_summable line 18
3. theorem OAI.SevenEighths.ProbePrimePower.positiveScalar_geometric_summable line 33
4. theorem OAI.SevenEighths.ProbeEuler.rowMarkedTerm_frequency_summable line 58
5. theorem OAI.SevenEighths.ProbeEuler.rowMarkedTerm_zero_lower_edge line 72
6. theorem OAI.SevenEighths.ProbeEuler.rowMarkedFamily_hasSum line 79