OAI/NumberTheory/DirichletL/QuadraticSieve/CoprimeBilinearBound.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CoprimeBilinearSieve.disjoint_bilinear_expansion line 76
  2. theorem OAI.CoprimeBilinearSieve.coprime_bilinear_operator_bound line 119
  3. abbrev OAI.IdealCoprimeBilinearSieve.O line 179
  4. theorem OAI.IdealCoprimeBilinearSieve.support_weighted_energy_bound line 182
  5. theorem OAI.IdealCoprimeBilinearSieve.ideal_coprime_bilinear_operator_bound line 195
  6. abbrev OAI.DivisorBlockCauchy.O line 234
  7. theorem OAI.DivisorBlockCauchy.divisor_mask_energy line 237
  8. def OAI.DivisorBlockCauchy.divisorConstant line 254
  9. theorem OAI.DivisorBlockCauchy.divisorConstant_pos line 257
  10. theorem OAI.DivisorBlockCauchy.divisor_mask_energy_small_power line 260
  11. theorem OAI.DivisorBlockCauchy.rectangular_cauchy line 276
  12. abbrev OAI.IdealDivisorBilinearBlocks.O line 301
  13. def OAI.IdealDivisorBilinearBlocks.blockValue line 304
  14. theorem OAI.IdealDivisorBilinearBlocks.blockValue_nonneg line 312
  15. theorem OAI.IdealDivisorBilinearBlocks.divisor_block_bound line 319
  16. def OAI.FiniteSieveRestriction.extendByZero line 381
  17. theorem OAI.FiniteSieveRestriction.extendByZero_apply_image line 385
  18. theorem OAI.FiniteSieveRestriction.extendByZero_zero line 395
  19. theorem OAI.FiniteSieveRestriction.extendByZero_energy line 402
  20. theorem OAI.FiniteSieveRestriction.extendByZero_matrix line 417
  21. theorem OAI.FiniteSieveRestriction.masked_column_restriction_norm_le line 430
  22. theorem OAI.FiniteSieveRestriction.column_restriction_norm_le line 452
  23. theorem OAI.FiniteSieveRestriction.row_restriction_norm_le line 458
  24. theorem OAI.FiniteSieveRestriction.submatrix_norm_le line 467
  25. theorem OAI.FiniteSieveOperator.squared_norm_le_of_energy line 480
  26. abbrev OAI.CanonicalQuadraticSieve.O line 496
  27. theorem OAI.CanonicalQuadraticSieve.idealSexticRow_ambient line 499
  28. def OAI.CanonicalQuadraticSieve.Admissible line 522
  29. theorem OAI.CanonicalQuadraticSieve.singletonPositive line 526
  30. theorem OAI.CanonicalQuadraticSieve.singletonGood line 531
  31. def OAI.CanonicalQuadraticSieve.quadraticRow line 538
  32. theorem OAI.CanonicalQuadraticSieve.quadraticRow_eq line 543
  33. def OAI.CanonicalQuadraticSieve.idealRange line 554
  34. theorem OAI.CanonicalQuadraticSieve.mem_idealRange line 556
  35. theorem OAI.CanonicalQuadraticSieve.idealRange_mono line 571
  36. def OAI.CanonicalQuadraticSieve.matrix line 576
  37. def OAI.CanonicalQuadraticSieve.sieveNorm line 579
  38. theorem OAI.CanonicalQuadraticSieve.sieveNorm_nonneg line 581
  39. def OAI.CanonicalQuadraticSieve.rangeInclusion line 583
  40. theorem OAI.CanonicalQuadraticSieve.rangeInclusion_injective line 586
  41. theorem OAI.CanonicalQuadraticSieve.sieveNorm_mono line 591
  42. theorem OAI.CanonicalQuadraticSieve.family_squared_norm_le line 600
  43. theorem OAI.CanonicalQuadraticSieve.energy_bound line 615