OAI/NumberTheory/DirichletL/CubicSieve/GlobalEncoding.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.primeIdealProduct_emultiplicity line 82
  2. theorem OAI.SecondPassArithmetic.primeIdealProduct_exponents_eq line 100
  3. theorem OAI.SecondPassArithmetic.primeProduct_span_exponents_eq line 116
  4. theorem OAI.CanonicalQuadraticSieve.divisor_dyadic_sum_le line 136
  5. def OAI.CanonicalQuadraticSieve.largePrincipalWindow line 159
  6. lemma OAI.CanonicalQuadraticSieve.largePrincipalWindow_le line 169
  7. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.large_principal_window line 188
  8. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.large_principal_pool line 234
  9. theorem OAI.CanonicalQuadraticSieve.finite_principal_triangle line 270
  10. def OAI.CanonicalQuadraticSieve.principalDivisorCorrection line 294
  11. def OAI.CanonicalQuadraticSieve.largePrincipalProductAt line 302
  12. lemma OAI.CanonicalQuadraticSieve.largePrincipalProductAt_le_window line 311
  13. lemma OAI.CanonicalQuadraticSieve.principalDivisorCorrection_le_product line 343
  14. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.principal_divisor_correction line 385
  15. structure OAI.SecondPassArithmetic.CubeCoordinates line 430
  16. def OAI.SecondPassArithmetic.CubeCoordinates.support line 439
  17. def OAI.SecondPassArithmetic.CubeCoordinates.leftBit line 442
  18. def OAI.SecondPassArithmetic.CubeCoordinates.rightBit line 443
  19. def OAI.SecondPassArithmetic.CubeCoordinates.Admissible line 445
  20. theorem OAI.SecondPassArithmetic.CubeCoordinates.support_pos line 448
  21. theorem OAI.SecondPassArithmetic.CubeCoordinates.left_off line 453
  22. theorem OAI.SecondPassArithmetic.CubeCoordinates.right_off line 458
  23. theorem OAI.SecondPassArithmetic.CubeCoordinates.aLabel_left line 463
  24. theorem OAI.SecondPassArithmetic.CubeCoordinates.aLabel_right line 474
  25. structure OAI.SecondPassArithmetic.GlobalSecondData line 487
  26. def OAI.SecondPassArithmetic.globalSecondTuple line 497
  27. def OAI.SecondPassArithmetic.globalSecondFixedTriple line 501
  28. def OAI.SecondPassArithmetic.GlobalSecondAdmissible line 507
  29. theorem OAI.SecondPassArithmetic.globalSecondTuple_valid line 512
  30. theorem OAI.SecondPassArithmetic.globalSecondFixedTriple_nonzero line 521
  31. theorem OAI.SecondPassArithmetic.globalSecondFixedTriple_norm_bounds line 529
  32. theorem OAI.SecondPassArithmetic.globalSecondFixedTriple_count line 554
  33. theorem OAI.SecondPassArithmetic.sum_globalSecondFixedTriple line 576
  34. theorem OAI.SecondPassArithmetic.globalSecondTuple_cube_eq line 593
  35. theorem OAI.SecondPassArithmetic.globalSecondEncoding_injective line 622
  36. theorem OAI.SecondPassArithmetic.globalSecond_fiber_card line 649