OAI/NumberTheory/DirichletL/QuadraticSieve/LogarithmicSectors.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.lowPrincipalErrorSum line 83
  2. theorem OAI.CanonicalQuadraticSieve.lowPrincipal_actual_error_sum_bound line 91
  3. theorem OAI.CanonicalQuadraticSieve.sqrt_product_column_shell line 138
  4. theorem OAI.CanonicalQuadraticSieve.dual_truncation_reference_bounds line 151
  5. theorem OAI.CanonicalQuadraticSieve.dual_truncation_prefactor_bound line 169
  6. def OAI.CanonicalQuadraticSieve.dualPrincipalErrorSum line 181
  7. theorem OAI.CanonicalQuadraticSieve.dualPrincipal_actual_error_sum_bound line 191
  8. def OAI.SecondPassArithmetic.secondSquarefreeLogSector line 258
  9. lemma OAI.SecondPassArithmetic.secondSquarefreeLogSector_subset line 265
  10. def OAI.SecondPassArithmetic.secondSquarefreeLogTargets line 270
  11. lemma OAI.SecondPassArithmetic.secondSquarefreeLogTargets_subset line 278
  12. lemma OAI.SecondPassArithmetic.secondSquarefreeLogTargets_mem line 285
  13. lemma OAI.SecondPassArithmetic.secondSquarefreeLogTargets_squarefree line 294
  14. lemma OAI.SecondPassArithmetic.secondSquarefreeLogTargets_bounds line 302
  15. lemma OAI.SecondPassArithmetic.secondSquarefreeLogSector_coordinates line 311
  16. theorem OAI.SecondPassArithmetic.secondExpansionSource_log_eq_squarefree line 332
  17. theorem OAI.SecondPassArithmetic.normalized_squarefree_binned_second_density_transfer line 356
  18. theorem OAI.SecondPassArithmetic.firstCoreInputRow_squarefree_binned_finite_transfer line 451
  19. theorem OAI.SecondPassArithmetic.firstCoreInputRow_squarefree_binned_integrated_transfer line 563