OAI/NumberTheory/DirichletL/QuadraticSieve/DualMiddleExpansion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.scaled_middleTruncation_eq_ideal_frequencies line 78
  2. theorem OAI.CanonicalQuadraticSieve.dual_normalized_middle_expansion line 100
  3. def OAI.CanonicalQuadraticSieve.dualTruncatedMiddle line 119
  4. theorem OAI.CanonicalQuadraticSieve.dual_truncated_pair_expansion line 129
  5. theorem OAI.CanonicalQuadraticSieve.dualTruncatedMiddle_le_product_divisors line 176
  6. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_truncated_middle line 226
  7. theorem OAI.SecondPassArithmetic.primeSpanProduct_squarefree line 281
  8. theorem OAI.SecondPassArithmetic.row_nonzero_notMem line 290
  9. theorem OAI.SecondPassArithmetic.primeSpanProduct_isCoprime_of_row_nonzero line 299
  10. def OAI.SecondPassArithmetic.firstRetainedSupport line 314
  11. theorem OAI.SecondPassArithmetic.jLabel_eq_retainedProduct line 318
  12. theorem OAI.SecondPassArithmetic.firstBaseLabel_squarefree line 327
  13. def OAI.SecondPassArithmetic.secondArithmeticWeight line 348
  14. theorem OAI.SecondPassArithmetic.secondArithmeticWeight_coprime line 354
  15. theorem OAI.SecondPassArithmetic.secondArithmeticWeight_squarefree line 387
  16. theorem OAI.SecondPassArithmetic.actualSecondLabel_squarefree_of_weight line 398
  17. theorem OAI.SecondPassArithmetic.secondExpansionSource_eq_squarefree line 412
  18. def OAI.SecondPassArithmetic.secondLogNormalizedEnergy line 459
  19. lemma OAI.SecondPassArithmetic.secondLogNormalizedEnergy_nonneg line 467
  20. lemma OAI.SecondPassArithmetic.secondLogNormalizedEnergy_empty line 484
  21. theorem OAI.SecondPassArithmetic.secondLog_normalized_cost line 493
  22. theorem OAI.SecondPassArithmetic.first_second_normalized_child_cost line 514
  23. theorem OAI.SecondPassArithmetic.secondBinnedIndex_mass line 534
  24. lemma OAI.FirstPassCubeLabels.firstLogDensity_pair_moment line 563
  25. lemma OAI.FirstPassCubeLabels.firstLogDensity_le_zero line 568
  26. lemma OAI.FirstPassCubeLabels.integral_pair_moment_bound line 572
  27. theorem OAI.SecondPassArithmetic.firstCoreInputRow_binned_integrated_transfer line 609