OAI/NumberTheory/DirichletL/QuadraticSieve/ProductColumns.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.productColumnCoefficient line 77
  2. theorem OAI.CanonicalQuadraticSieve.product_fiber_card line 80
  3. theorem OAI.CanonicalQuadraticSieve.productColumnCoefficient_norm line 95
  4. theorem OAI.CanonicalQuadraticSieve.productColumnCoefficient_row_sum line 109
  5. theorem OAI.CanonicalQuadraticSieve.product_quadratic_norm line 123
  6. def OAI.CompletedGauss.shortCompletedSum line 175
  7. def OAI.CompletedGauss.shortCubeRange line 180
  8. theorem OAI.CompletedGauss.mem_shortCubeRange line 183
  9. theorem OAI.CompletedGauss.shortCompletedSum_eq line 196
  10. theorem OAI.CompletedGauss.cube_inverse_weight_norm line 209
  11. theorem OAI.CompletedGauss.short_completed_energy line 227
  12. theorem OAI.CompletedGauss.short_cube_scale_algebra line 275
  13. theorem OAI.CompletedGauss.short_cube_scales line 308
  14. theorem OAI.CompletedGauss.short_completed_branch line 328
  15. theorem OAI.CompletedGauss.short_completed_average line 349
  16. theorem OAI.CompletedGauss.short_completed_normalized_small_power line 389
  17. theorem OAI.CanonicalQuadraticSieve.squarefree_all_column_energy line 432
  18. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_nonzero_bounds line 509
  19. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_nonzero_card line 527
  20. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_all_energy line 546
  21. theorem OAI.CanonicalQuadraticSieve.columnSquareParts_nonzero_bounds line 590
  22. theorem OAI.CanonicalQuadraticSieve.bounded_nonzero_quadratic_norm line 608