OAI/NumberTheory/CubicGauss/InitialBounds.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Initial large-sieve bounds, positivity and divisor counts.

  1. lemma OAI.CubicFirstMoment.nonzero_gaussian_finite_mass line 15
  2. lemma OAI.CubicFirstMoment.cubicSymbol_at_zero line 35
  3. lemma OAI.CubicFirstMoment.cubic_zero_row_bound line 44
  4. lemma OAI.CubicFirstMoment.cubic_row_card_bound line 59
  5. theorem OAI.CubicFirstMoment.cubic_gaussian_initial_bound line 78
  6. lemma OAI.CubicFirstMoment.norm_idealMoebius_le line 121
  7. def OAI.CubicFirstMoment.CubicGaussianBound line 131
  8. lemma OAI.CubicFirstMoment.initial_cubicGaussianBound line 138
  9. lemma OAI.CubicFirstMoment.cubic_coprime_dual_norm_bound line 144
  10. lemma OAI.CubicFirstMoment.cubic_coprime_dual_gaussian_bound line 158
  11. lemma OAI.CubicFirstMoment.sieveFiber_subset_quotient line 180
  12. theorem OAI.CubicFirstMoment.cubic_gaussian_positive_bound line 193
  13. abbrev OAI.CubicFirstMoment.SieveFour line 275
  14. def OAI.CubicFirstMoment.sieveFourIndices line 277
  15. def OAI.CubicFirstMoment.divisorFourIndices line 281
  16. def OAI.CubicFirstMoment.sieveFourMap line 285
  17. lemma OAI.CubicFirstMoment.mem_sieveFourIndices line 288
  18. lemma OAI.CubicFirstMoment.mem_divisorFourIndices line 294
  19. lemma OAI.CubicFirstMoment.sieveFourMap_mem line 299
  20. lemma OAI.CubicFirstMoment.sieveFourMap_inj line 317
  21. theorem OAI.CubicFirstMoment.sieve_divisor_multiplicity_bound line 332
  22. lemma OAI.CubicFirstMoment.squarefree_divisor_cube_bound line 354
  23. theorem OAI.CubicFirstMoment.sieve_divisor_power_bound line 374