OAI/NumberTheory/DirichletL/Detector/GramFrequencySummation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeGramFrequencySummation.frequencyNorm line 12
2. lemma OAI.SevenEighths.ProbeGramFrequencySummation.frequencyNorm_nonneg line 14
3. lemma OAI.SevenEighths.ProbeGramFrequencySummation.frequencyNorm_one_le line 16
4. theorem OAI.SevenEighths.ProbeGramFrequencySummation.finite_weighted_of_count line 21
5. theorem OAI.SevenEighths.ProbeGramFrequencySummation.nonzero_frequency_count line 76
6. theorem OAI.SevenEighths.ProbeGramFrequencySummation.frequency_weighted_sum line 92
7. theorem OAI.SevenEighths.ProbeGramFrequencySummation.exceptional_frequency_weighted_sum line 106