OAI/NumberTheory/DirichletL/Detector/Row.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeRow.targetMonoid line 15
2. theorem OAI.SevenEighths.ProbeRow.targetMonoid_norm_le_one line 20
3. def OAI.SevenEighths.ProbeRow.rowCoefficient line 26
4. theorem OAI.SevenEighths.ProbeRow.rowCoefficient_apply line 31
5. theorem OAI.SevenEighths.ProbeRow.rowCoefficient_apply_unit line 36
6. theorem OAI.SevenEighths.ProbeRow.rowCoefficient_norm_le_one line 46
7. def OAI.SevenEighths.ProbeRow.spectralSummand line 55
8. def OAI.SevenEighths.ProbeRow.spectralRow line 61
9. theorem OAI.SevenEighths.ProbeRow.spectralSummand_norm_le line 64
10. theorem OAI.SevenEighths.ProbeRow.spectralRow_summable line 85