OAI/NumberTheory/DirichletL/QuadraticSieve/DivisorBlocks.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.quotientBlock line 78
  2. theorem OAI.CanonicalQuadraticSieve.canonical_divisor_block_bound line 84
  3. theorem OAI.CanonicalQuadraticSieve.quadraticRow_norm_le_one line 147
  4. theorem OAI.CanonicalQuadraticSieve.quadraticRow_mul line 154
  5. theorem OAI.CanonicalQuadraticSieve.quadraticRow_divisor_factor line 187
  6. def OAI.CanonicalQuadraticSieve.originalBlock line 196
  7. theorem OAI.CanonicalQuadraticSieve.original_entry_factor line 202
  8. theorem OAI.CanonicalQuadraticSieve.originalBlock_le_quotientBlock line 213
  9. theorem OAI.CanonicalQuadraticSieve.original_rectangular_bound line 249
  10. theorem OAI.CanonicalQuadraticSieve.canonical_original_divisor_block_bound line 265
  11. theorem OAI.FiniteSieveRestriction.squared_norm_row_partition line 292
  12. def OAI.CanonicalQuadraticSieve.Supported line 309
  13. def OAI.CanonicalQuadraticSieve.fullRange line 313
  14. theorem OAI.CanonicalQuadraticSieve.mem_fullRange line 315
  15. theorem OAI.CanonicalQuadraticSieve.admissible_supported line 330
  16. theorem OAI.CanonicalQuadraticSieve.squarefreePart_eq_self line 333
  17. def OAI.CanonicalQuadraticSieve.highKernelRange line 337
  18. theorem OAI.CanonicalQuadraticSieve.mem_highKernelRange line 340
  19. def OAI.CanonicalQuadraticSieve.highKernelMatrix line 345
  20. def OAI.CanonicalQuadraticSieve.highKernelNorm line 348
  21. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_nonneg line 350
  22. theorem OAI.CanonicalQuadraticSieve.sieveNorm_le_low_add_high line 352
  23. theorem OAI.QuadraticKernelTransfer.sum_norm_integral_bound line 392
  24. theorem OAI.QuadraticKernelTransfer.radial_two_variable_window line 410
  25. theorem OAI.QuadraticKernelTransfer.radial_phase_integrable line 445
  26. theorem OAI.QuadraticKernelTransfer.radial_matrix_kernel_transfer line 455
  27. def OAI.CanonicalQuadraticSieve.quotientTerm line 505
  28. def OAI.CanonicalQuadraticSieve.divisorBlockCost line 511
  29. theorem OAI.CanonicalQuadraticSieve.quotientTerm_phase line 517
  30. theorem OAI.CanonicalQuadraticSieve.canonical_divisor_block_phase_bound line 529
  31. theorem OAI.CanonicalQuadraticSieve.canonical_radial_divisor_block_bound line 560
  32. def OAI.CanonicalQuadraticSieve.originalTerm line 616
  33. theorem OAI.CanonicalQuadraticSieve.originalTerm_phase line 623
  34. theorem OAI.CanonicalQuadraticSieve.canonical_original_divisor_block_phase_bound line 635
  35. theorem OAI.CanonicalQuadraticSieve.canonical_original_radial_divisor_block_bound line 666