OAI/NumberTheory/CubicGram/DyadicRecurrence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Frequency dyads and summable base Gram recurrences.

  1. lemma OAI.CubicFirstMoment.normNat_ne_zero_of_ne_zero line 17
  2. def OAI.CubicFirstMoment.frequencyDyad line 23
  3. lemma OAI.CubicFirstMoment.mem_frequencyDyad line 26
  4. lemma OAI.CubicFirstMoment.frequencyDyad_norm line 35
  5. lemma OAI.CubicFirstMoment.summable_gramDualTerm line 47
  6. lemma OAI.CubicFirstMoment.hasSum_frequencyDyad line 71
  7. lemma OAI.CubicFirstMoment.finiteCubicBound_le_card_mul line 99
  8. lemma OAI.CubicFirstMoment.dyadic_decay_step line 119
  9. lemma OAI.CubicFirstMoment.dyadic_decay_partial_sum line 135
  10. lemma OAI.CubicFirstMoment.dyadic_decay_summable line 151
  11. lemma OAI.CubicFirstMoment.dyadic_decay_tsum line 155
  12. def OAI.CubicFirstMoment.coprimeGramForm line 163
  13. lemma OAI.CubicFirstMoment.hasSum_coprimePoissonDyad line 168
  14. lemma OAI.CubicFirstMoment.frequencyDyad_card_le line 195
  15. theorem OAI.CubicFirstMoment.coprimeGramForm_base_bound line 202