OAI/NumberTheory/DirichletL/QuadraticSieve/CoefficientCancellation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MixedCrossSeparation.norm_localCoefficient line 77
  2. theorem OAI.MixedCrossSeparation.local_coefficient_cancel line 83
  3. theorem OAI.MixedCrossSeparation.canonicalProductG_crt line 118
  4. theorem OAI.MixedCrossSeparation.convertedColumnBlock_univ line 138
  5. theorem OAI.MixedCrossSeparation.coefficient_cancel_univ_false line 152
  6. theorem OAI.MixedCrossSeparation.coefficient_cancel_univ_true line 172
  7. theorem OAI.MixedCrossSeparation.columnPrimeCoprime line 209
  8. def OAI.MixedCrossSeparation.columnCoefficient line 216
  9. def OAI.MixedCrossSeparation.columnG line 223
  10. theorem OAI.MixedCrossSeparation.convertedColumnBlock_subtype line 230
  11. theorem OAI.MixedCrossSeparation.columnCoefficient_cancel_false line 240
  12. theorem OAI.MixedCrossSeparation.columnCoefficient_cancel_true line 253
  13. def OAI.FirstCauchyArithmetic.firstPassColumnMinus line 280
  14. def OAI.FirstCauchyArithmetic.firstPassColumnPlus line 287
  15. theorem OAI.FirstCauchyArithmetic.norm_columnG line 293
  16. theorem OAI.FirstCauchyArithmetic.norm_firstPassColumnMinus_le line 304
  17. theorem OAI.FirstCauchyArithmetic.norm_firstPassColumnPlus_le line 320
  18. theorem OAI.FirstCauchyArithmetic.a_weighted_converted_pair line 332
  19. theorem OAI.FirstCauchyArithmetic.active_productGauss_eq_mobius_converted line 370
  20. def OAI.FirstCauchyArithmetic.activeGaussRowFactor line 411
  21. theorem OAI.FirstCauchyArithmetic.disjoint_pair_poisson_arithmetic line 423
  22. theorem OAI.FirstCauchyArithmetic.a_weighted_activeGaussRowFactor line 476
  23. theorem OAI.FirstCauchyArithmetic.a_weighted_pair_sum_to_second_poisson_rows line 499
  24. abbrev OAI.QuadraticInitialBound.O line 544
  25. def OAI.QuadraticInitialBound.pvSeminorms line 547
  26. def OAI.QuadraticInitialBound.pvConstant line 550
  27. theorem OAI.QuadraticInitialBound.pvConstant_pos line 553
  28. def OAI.QuadraticInitialBound.pvControl line 557
  29. theorem OAI.QuadraticInitialBound.pvControl_nonneg line 560
  30. theorem OAI.QuadraticInitialBound.pv_lattice_bound line 563
  31. theorem OAI.QuadraticInitialBound.norm_finite_character_le_one line 569
  32. theorem OAI.QuadraticInitialBound.finiteSexticRow_norm_le_one line 578
  33. theorem OAI.QuadraticInitialBound.canonical_polya_vinogradov line 591
  34. theorem OAI.QuadraticInitialBound.norm_ideal_moebius_le_one line 645
  35. theorem OAI.QuadraticInitialBound.canonical_masked_polya_vinogradov line 650