OAI/NumberTheory/DirichletL/QuadraticSieve/CommonMasks.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.maskedPairDualTail line 83
  2. def OAI.CanonicalQuadraticSieve.retainedDualPair line 90
  3. theorem OAI.CanonicalQuadraticSieve.maskedPairIdealDualKernel_retained line 96
  4. theorem OAI.CanonicalQuadraticSieve.retainedDualPrincipalSum_pair_expansion line 149
  5. theorem OAI.CanonicalQuadraticSieve.retainedDualPrincipalSum_twist_expansion line 168
  6. def OAI.CanonicalQuadraticSieve.maskedDualFamily line 186
  7. def OAI.CanonicalQuadraticSieve.maskedDualTailFamily line 191
  8. theorem OAI.CanonicalQuadraticSieve.maskedDualFamily_retained line 196
  9. theorem OAI.CanonicalQuadraticSieve.normalizedFactors_commonMaskIdeal line 238
  10. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_commonMaskIdeal line 246
  11. lemma OAI.CanonicalQuadraticSieve.idealZeroMask_idempotent line 253
  12. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_generator_eq_indicator line 259
  13. theorem OAI.CanonicalQuadraticSieve.idealZeroMask_primary_eq_indicator line 280
  14. theorem OAI.CanonicalQuadraticSieve.commonMask_primary_indicator line 286
  15. theorem OAI.CanonicalQuadraticSieve.residual_joint_mask line 292
  16. theorem OAI.CanonicalQuadraticSieve.lowPrincipalLattice_residual line 317
  17. theorem OAI.CanonicalQuadraticSieve.idealRange_filter_coprime line 331
  18. theorem OAI.CanonicalQuadraticSieve.sum_idealRange_coprime line 345
  19. def OAI.CanonicalQuadraticSieve.pairMaskedSquareSource line 354
  20. theorem OAI.CanonicalQuadraticSieve.originalPairLow_residual_finite line 359
  21. theorem OAI.CanonicalQuadraticSieve.originalLow_gcd_aggregate line 383
  22. theorem OAI.CanonicalQuadraticSieve.originalDual_gcd_aggregate line 423
  23. theorem OAI.CanonicalQuadraticSieve.originalHigh_gcd_principal_assembly line 447
  24. theorem OAI.CanonicalQuadraticSieve.residual_commonMask_coprime line 495
  25. theorem OAI.CanonicalQuadraticSieve.idealQuotient_norm_eq line 517
  26. theorem OAI.CanonicalQuadraticSieve.idealQuotient_shell line 524
  27. def OAI.CanonicalQuadraticSieve.gcdRaySupport line 542
  28. theorem OAI.CanonicalQuadraticSieve.mem_gcdRaySupport line 546
  29. theorem OAI.CanonicalQuadraticSieve.gcd_ray_pair_sum_restrict line 551
  30. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_energy line 601
  31. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_quotient_properties line 607
  32. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_proper line 637