OAI/NumberTheory/DirichletL/CubicSieve/PrincipalNormalization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.globalSecondLabel line 88
  2. theorem OAI.SecondPassArithmetic.globalSecondLabel_span line 93
  3. def OAI.SecondPassArithmetic.globalSecondLabelUnit line 98
  4. theorem OAI.SecondPassArithmetic.globalSecondLabelUnit_spec line 103
  5. theorem OAI.SecondPassArithmetic.global_second_energy_pushforward line 108
  6. def OAI.SecondPassArithmetic.globalSecondMode line 160
  7. theorem OAI.SecondPassArithmetic.global_second_mode_transfer line 166
  8. theorem OAI.SecondPassArithmetic.rowCoprimeMask_congr_span line 226
  9. theorem OAI.SecondPassArithmetic.fixedChildRow_congr_mask_span line 233
  10. theorem OAI.SecondPassArithmetic.secondChildColumn_zero_of_mask_label_mem line 238
  11. theorem OAI.SecondPassArithmetic.fixedChildRow_restore_killed_pool line 251
  12. def OAI.SecondPassArithmetic.globalSecondMask line 267
  13. def OAI.SecondPassArithmetic.fixedTripleMask line 273
  14. theorem OAI.SecondPassArithmetic.globalSecondMask_span line 277
  15. theorem OAI.SecondPassArithmetic.globalSecondMask_kills_cube_common line 285
  16. theorem OAI.SecondPassArithmetic.globalSecondRawRow_fixed_pool line 316
  17. def OAI.CanonicalQuadraticSieve.signedProductDivisorSum line 346
  18. def OAI.CanonicalQuadraticSieve.correctionRectangleMajorant line 354
  19. theorem OAI.CanonicalQuadraticSieve.signedProductDivisorSum_le_rectangles line 363
  20. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.small_principal_window line 426
  21. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.small_principal_divisor_sum line 480
  22. lemma OAI.CanonicalQuadraticSieve.source_large_cut_lower line 521
  23. lemma OAI.CanonicalQuadraticSieve.dual_large_cut_lower line 532
  24. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.source_large_principal_sum line 552
  25. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_large_principal_sum line 572
  26. theorem OAI.CanonicalQuadraticSieve.dual_large_principal_normalization line 593