OAI/NumberTheory/CubicGauss/GramPoisson.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Cubic Gram expansions and their residue-Poisson transforms.

  1. lemma OAI.CubicFirstMoment.dvd_common_of_coprime line 16
  2. lemma OAI.CubicFirstMoment.primary_common_split_unique line 25
  3. abbrev OAI.CubicFirstMoment.CommonIndex line 37
  4. def OAI.CubicFirstMoment.commonTriples line 39
  5. lemma OAI.CubicFirstMoment.mem_commonTriples line 44
  6. theorem OAI.CubicFirstMoment.sum_commonTriples line 59
  7. lemma OAI.CubicFirstMoment.cubic_common_gram line 92
  8. theorem OAI.CubicFirstMoment.cubic_row_common_gram line 111
  9. lemma OAI.CubicFirstMoment.bounded_gaussian_summable line 141
  10. lemma OAI.CubicFirstMoment.cubicCorrelation_norm_le line 152
  11. lemma OAI.CubicFirstMoment.dvdIndicator_norm_le line 158
  12. lemma OAI.CubicFirstMoment.tsum_dvd_indicator line 161
  13. lemma OAI.CubicFirstMoment.cubic_dvd_correlation_theta line 172
  14. theorem OAI.CubicFirstMoment.cubic_common_correlation_poisson line 193