OAI/NumberTheory/DirichletL/QuadraticSieve/SquareParts.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.supported_mul_iff line 80
  2. theorem OAI.CanonicalQuadraticSieve.supported_sq_iff line 102
  3. theorem OAI.CanonicalQuadraticSieve.supported_square_parts line 105
  4. def OAI.CanonicalQuadraticSieve.supportedSquarefreeEquiv line 117
  5. theorem OAI.CanonicalQuadraticSieve.supported_tsum_squarefree_decomposition line 129
  6. theorem OAI.CanonicalQuadraticSieve.canonical_quadraticRow_argument_mul line 142
  7. theorem OAI.CanonicalQuadraticSieve.canonical_quadraticRow_square_argument line 152
  8. theorem OAI.CanonicalQuadraticSieve.canonical_quadraticRow_primary_squarefree line 156
  9. theorem OAI.CanonicalQuadraticSieve.canonical_high_pair_squarefree_decomposition line 164
  10. theorem OAI.CanonicalQuadraticSieve.supported_generator_injective line 203
  11. theorem OAI.CanonicalQuadraticSieve.supported_radial_norm_summable line 212
  12. def OAI.CanonicalQuadraticSieve.originalPairSource line 227
  13. def OAI.CanonicalQuadraticSieve.originalPairLow line 231
  14. def OAI.CanonicalQuadraticSieve.originalPairHigh line 234
  15. theorem OAI.CanonicalQuadraticSieve.originalPairSource_summable line 237
  16. theorem OAI.CanonicalQuadraticSieve.originalPairLow_summable line 252
  17. theorem OAI.CanonicalQuadraticSieve.originalPairHigh_summable line 256
  18. theorem OAI.CanonicalQuadraticSieve.originalPairHigh_eq_source_sub_low line 260
  19. theorem OAI.CanonicalQuadraticSieve.canonical_gcd_masked_pair_poisson line 280
  20. theorem OAI.CanonicalQuadraticSieve.canonical_pair_divisor_mask line 322
  21. theorem OAI.CanonicalQuadraticSieve.canonical_original_pair_poisson line 334
  22. theorem OAI.CanonicalQuadraticSieve.residual_pair_nontrivial line 364
  23. theorem OAI.CanonicalQuadraticSieve.original_pair_dual_remove_zero line 375
  24. def OAI.CanonicalQuadraticSieve.rayPairCoefficient line 388
  25. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_eq_pair_high line 392
  26. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_eq_source_sub_low line 441
  27. def OAI.CanonicalQuadraticSieve.originalPairDualKernel line 460
  28. theorem OAI.CanonicalQuadraticSieve.originalPairSource_poisson line 474
  29. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_poisson line 480
  30. theorem OAI.SecondPassIntegration.columnLog_extract_common line 504
  31. theorem OAI.SecondPassIntegration.normalizedColumn_extract_fixed_profile line 514
  32. theorem OAI.SecondPassIntegration.normalizedColumn_pair_extract_fixed_profiles line 527
  33. def OAI.SecondPassArithmetic.actualSecondVariableSectorSource line 559
  34. theorem OAI.SecondPassArithmetic.actual_second_variable_sector_uniform_transfer line 571