OAI/NumberTheory/DirichletL/CubicSieve/PrincipalDensity.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassIntegration.childDensity_elementary_normalized line 79
  2. theorem OAI.SecondPassIntegration.childDensity_elementary_supported line 113
  3. def OAI.CanonicalQuadraticSieve.sourcePrincipalScale line 143
  4. def OAI.CanonicalQuadraticSieve.maskedSourceDensity line 147
  5. def OAI.CanonicalQuadraticSieve.maskedPrincipalSourceSum line 152
  6. def OAI.CanonicalQuadraticSieve.maskedSourcePrincipalTruncation line 158
  7. def OAI.CanonicalQuadraticSieve.maskedSourceErrorSum line 164
  8. theorem OAI.CanonicalQuadraticSieve.maskedSourcePrincipalTruncation_eq line 173
  9. theorem OAI.CanonicalQuadraticSieve.maskedPrincipalSourceSum_eq line 208
  10. theorem OAI.CanonicalQuadraticSieve.maskedSource_error_uniform line 238
  11. def OAI.CanonicalQuadraticSieve.sourcePrincipalMajorant line 282
  12. theorem OAI.CanonicalQuadraticSieve.masked_source_principal_difference line 297
  13. lemma OAI.CanonicalQuadraticSieve.sourcePrincipalMajorant_nonneg line 345
  14. lemma OAI.CanonicalQuadraticSieve.sourcePrincipalMajorant_mono line 359
  15. lemma OAI.CanonicalQuadraticSieve.maskedPrincipalSourceDifference_dyadic line 381
  16. theorem OAI.CanonicalQuadraticSieve.masked_source_principal_global line 396
  17. theorem OAI.CanonicalQuadraticSieve.primePoolDensity_eq_support line 458
  18. theorem OAI.CanonicalQuadraticSieve.primePoolDensity_eq_real line 464
  19. theorem OAI.CanonicalQuadraticSieve.primePoolDensity_norm_le_one line 470
  20. theorem OAI.CanonicalQuadraticSieve.primePoolDensity_star line 478
  21. theorem OAI.CanonicalQuadraticSieve.primePoolDensity_mul line 482
  22. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_generator_eq_one line 492
  23. theorem OAI.CanonicalQuadraticSieve.normalizedPairDensity_eq_primePoolDensity line 503
  24. def OAI.CanonicalQuadraticSieve.densityColumn line 518
  25. theorem OAI.CanonicalQuadraticSieve.densityColumn_norm_le line 521
  26. theorem OAI.CanonicalQuadraticSieve.densityColumn_energy_le line 527
  27. theorem OAI.CanonicalQuadraticSieve.actualPrincipalDifference_densityColumn line 534
  28. theorem OAI.CanonicalQuadraticSieve.primePoolDensity_common_conductor line 559
  29. def OAI.CanonicalQuadraticSieve.densityPairSum line 568
  30. theorem OAI.CanonicalQuadraticSieve.unrestrictedPrincipalDensity_eq line 573
  31. theorem OAI.CanonicalQuadraticSieve.unrestrictedPrincipalDensity_squarefree line 596
  32. theorem OAI.CanonicalQuadraticSieve.originalTerm_one_eq_unrestricted line 603
  33. theorem OAI.CanonicalQuadraticSieve.maskedSourceDensity_eq line 615
  34. theorem OAI.CanonicalQuadraticSieve.maskedSourceDensity_coprime_squarefree line 637