OAI/NumberTheory/DirichletL/QuadraticSieve/TruncatedSecondTransfer.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.squarefreeIdealRange line 78
  2. theorem OAI.CanonicalQuadraticSieve.mem_squarefreeIdealRange line 80
  3. theorem OAI.CanonicalQuadraticSieve.tsum_squarefree_norm_cutoff line 95
  4. theorem OAI.CanonicalQuadraticSieve.dualSquarefreeLow_principal_finite line 119
  5. theorem OAI.CanonicalQuadraticSieve.canonical_nonprincipal_dual_finite_truncated line 131
  6. def OAI.SecondPassArithmetic.secondDiagonalMass line 177
  7. theorem OAI.SecondPassArithmetic.truncatedSecondZero_eq_density line 184
  8. theorem OAI.SecondPassArithmetic.secondDiagonalMass_nonneg_le line 218
  9. theorem OAI.SecondPassArithmetic.truncatedSecondZero_norm_le line 233
  10. def OAI.SecondPassArithmetic.secondDyadicSector line 251
  11. theorem OAI.SecondPassArithmetic.secondDyadicSector_subset line 256
  12. theorem OAI.SecondPassArithmetic.sum_secondDyadicSector line 262
  13. theorem OAI.SecondPassArithmetic.truncatedSecondSource_eq_zero_add_dyadic line 279
  14. theorem OAI.SecondPassArithmetic.truncatedSecondSource_norm_le_zero_add_dyadic line 299
  15. theorem OAI.SecondPassArithmetic.normalized_truncated_second_transfer line 334
  16. theorem OAI.SecondPassArithmetic.postCommonSmoothPair_twisted_fixed_tests line 436
  17. theorem OAI.SecondPassIntegration.tupleSource_twisted_uniform_transfer line 476
  18. theorem OAI.SecondPassIntegration.exists_fixed_twisted_normalized_child_tests line 525
  19. theorem OAI.SecondPassArithmetic.actual_second_variable_sector_twisted_transfer line 611