OAI/NumberTheory/DirichletL/Fourier/LogDensity.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.JointLogSeparation.tripleLogDensity line 80
  2. lemma OAI.JointLogSeparation.tripleLogDensity_integrable line 83
  3. lemma OAI.JointLogSeparation.tripleLogDensity_nonneg line 87
  4. lemma OAI.JointLogSeparation.tripleLogDensity_bounded_integrable line 91
  5. lemma OAI.JointLogSeparation.tripleLogDensity_slice_integrable line 97
  6. theorem OAI.JointLogSeparation.triple_coefficient_density_bound line 107
  7. def OAI.SecondPassIntegration.densityChildEnergy line 134
  8. theorem OAI.SecondPassIntegration.child_coefficient_density_bound line 144
  9. lemma OAI.JointLogSeparation.one_add_norm_sub_le line 179
  10. theorem OAI.JointLogSeparation.difference_height_weight_le line 185
  11. theorem OAI.JointLogSeparation.triple_density_polynomial_bound line 203
  12. theorem OAI.CanonicalQuadraticSieve.ideals_coprime_of_relprime line 246
  13. theorem OAI.CanonicalQuadraticSieve.squarefree_quotient_gcd_coprime line 250
  14. theorem OAI.CanonicalQuadraticSieve.gcd_mul_of_coprime_divisor line 265
  15. def OAI.CanonicalQuadraticSieve.squarefreeGcdEquiv line 273
  16. theorem OAI.CanonicalQuadraticSieve.squarefree_gcd_tsum line 297
  17. def OAI.CanonicalQuadraticSieve.coprimeSquarefreeRange line 303
  18. theorem OAI.CanonicalQuadraticSieve.squarefree_cutoff_summable line 306
  19. theorem OAI.CanonicalQuadraticSieve.norm_le_mul_of_ne_zero line 319
  20. theorem OAI.CanonicalQuadraticSieve.coprime_squarefree_cutoff line 325
  21. theorem OAI.CanonicalQuadraticSieve.squarefree_gcd_finite_sum line 350
  22. theorem OAI.CanonicalQuadraticSieve.canonical_quadraticRow_one line 379
  23. theorem OAI.CanonicalQuadraticSieve.unrestrictedPairCharacter_one line 383
  24. def OAI.CanonicalQuadraticSieve.normalizedIdealPair line 389
  25. theorem OAI.CanonicalQuadraticSieve.normalizedIdealPair_mul line 392
  26. def OAI.CanonicalQuadraticSieve.normalizedIdealPairHom line 398
  27. theorem OAI.CanonicalQuadraticSieve.normalizedIdealPair_square line 406
  28. theorem OAI.CanonicalQuadraticSieve.squarefree_divisor_sum_eq_support line 420
  29. theorem OAI.CanonicalQuadraticSieve.normalizedIdealPair_double_divisor line 431
  30. def OAI.CanonicalQuadraticSieve.idealNormCutoff line 473
  31. def OAI.CanonicalQuadraticSieve.normalizedPairPartial line 475
  32. def OAI.CanonicalQuadraticSieve.normalizedPairCoprimePartial line 478
  33. def OAI.CanonicalQuadraticSieve.normalizedPairDivisors line 481
  34. def OAI.CanonicalQuadraticSieve.normalizedPairDensity line 484
  35. theorem OAI.CanonicalQuadraticSieve.normalizedPairPartial_split line 489
  36. theorem OAI.CanonicalQuadraticSieve.normalizedPair_main_difference line 507
  37. def OAI.CanonicalQuadraticSieve.commonMaskIdeal line 548
  38. theorem OAI.CanonicalQuadraticSieve.commonMaskIdeal_squarefree line 550
  39. theorem OAI.CanonicalQuadraticSieve.fixedBadPrimes_dvd_commonMaskIdeal line 562
  40. theorem OAI.CanonicalQuadraticSieve.admissible_of_squarefree_coprime_bad line 567
  41. theorem OAI.CanonicalQuadraticSieve.coprimeSquarefreeRange_subset_idealRange line 578
  42. theorem OAI.CanonicalQuadraticSieve.commonMask_coprimeSquarefreeRange_subset line 586
  43. theorem OAI.CanonicalQuadraticSieve.commonMaskIdeal_eq_fixed_mul line 590
  44. theorem OAI.CanonicalQuadraticSieve.commonMaskIdeal_norm line 602