OAI/NumberTheory/DirichletL/QuadraticSieve/IdealQuotients.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.primaryGenerator_admissible line 80
  2. theorem OAI.CanonicalQuadraticSieve.primaryGenerator_inj_on_admissible line 84
  3. theorem OAI.CanonicalQuadraticSieve.sieveNorm_initial line 91
  4. def OAI.CanonicalQuadraticSieve.idealQuotient line 152
  5. theorem OAI.CanonicalQuadraticSieve.idealQuotient_mul line 154
  6. theorem OAI.CanonicalQuadraticSieve.idealQuotient_dvd line 158
  7. theorem OAI.CanonicalQuadraticSieve.idealQuotient_injective_on line 162
  8. theorem OAI.CanonicalQuadraticSieve.admissible_of_dvd line 170
  9. theorem OAI.CanonicalQuadraticSieve.admissible_idealQuotient line 177
  10. theorem OAI.CanonicalQuadraticSieve.idealQuotient_norm_le line 180
  11. theorem OAI.CanonicalQuadraticSieve.quotient_family_squared_norm_le line 192
  12. def OAI.CanonicalQuadraticSieve.quotientMatrix line 210
  13. theorem OAI.CanonicalQuadraticSieve.quotientMatrix_squared_norm_le line 214
  14. def OAI.FourierBridge.fourierSeminormBound line 262
  15. def OAI.FourierBridge.fourierPointBound line 267
  16. theorem OAI.FourierBridge.fourierPointBound_nonneg line 270
  17. theorem OAI.FourierBridge.uniform_fourier_pointwise line 273
  18. theorem OAI.LocalLogFourier.coupled_positive_log_separation_envelope line 305
  19. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_log_separation_envelope line 415
  20. def OAI.FirstPassCubeLabels.rayIdealRow line 451
  21. def OAI.FirstPassCubeLabels.rayPairWeight line 462
  22. def OAI.FirstPassCubeLabels.rayIdealEnergy line 467
  23. theorem OAI.FirstPassCubeLabels.rayIdealEnergy_nonneg line 474
  24. theorem OAI.FirstPassCubeLabels.idealPairReindex_eq_ray_rows line 481
  25. theorem OAI.FirstPassCubeLabels.idealPairReindex_norm_le line 494
  26. theorem OAI.FirstPassCubeLabels.norm_rayPairWeight line 514
  27. def OAI.FirstPassCubeLabels.cubeLogCoefficient line 534
  28. theorem OAI.FirstPassCubeLabels.cubeLogCoefficient_continuous line 544
  29. theorem OAI.FirstPassCubeLabels.norm_cubeLogCoefficient_eq_zero line 559
  30. theorem OAI.FirstPassCubeLabels.rayIdealRow_continuous line 573
  31. theorem OAI.FirstPassCubeLabels.rayIdealRow_uniform_bound line 582
  32. theorem OAI.FirstPassCubeLabels.rayIdealEnergy_continuous line 604
  33. theorem OAI.FirstPassCubeLabels.rayIdealEnergy_uniform_bound line 616
  34. theorem OAI.FirstPassCubeLabels.integrable_rayIdealEnergy line 633
  35. theorem OAI.FirstPassCubeLabels.cube_integral_norm_le_energy line 645