OAI/NumberTheory/CubicGram/GlobalRecurrence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Summed dual norms and full smoothed sieve recurrences.

  1. def OAI.CubicFirstMoment.dualDyadicNorm line 15
  2. lemma OAI.CubicFirstMoment.summable_dualDyadicNorm line 18
  3. lemma OAI.CubicFirstMoment.dualDyadicNorm_nonneg line 38
  4. theorem OAI.CubicFirstMoment.coprimeGramForm_norm_recurrence line 42
  5. lemma OAI.CubicFirstMoment.residualRows_norm line 79
  6. lemma OAI.CubicFirstMoment.residualRows_nonunit line 92
  7. lemma OAI.CubicFirstMoment.residualRows_subset_one line 100
  8. lemma OAI.CubicFirstMoment.coprimeGramForm_subset_singleton line 132
  9. def OAI.CubicFirstMoment.commonBlockEnergy line 146
  10. lemma OAI.CubicFirstMoment.commonBlockEnergy_nonneg line 149
  11. lemma OAI.CubicFirstMoment.commonBlockCoefficient_energy_le line 152
  12. lemma OAI.CubicFirstMoment.commonBlockCoefficient_unweighted_energy_le line 163
  13. def OAI.CubicFirstMoment.commonBlockCost line 172
  14. lemma OAI.CubicFirstMoment.commonBlockCost_nonneg line 179
  15. theorem OAI.CubicFirstMoment.primarySmoothedSieveMass_norm_recurrence line 190