OAI/NumberTheory/DirichletL/QuadraticSieve/SelectedExponents.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.poissonComparisonMajorant_small_power line 78
  2. lemma OAI.CubicEisenstein.hyperbolicHeight_continuous line 123
  3. lemma OAI.CubicEisenstein.matrixCross_eq_gram line 132
  4. lemma OAI.CubicEisenstein.hyperbolicGram_upperPoint line 135
  5. def OAI.CubicEisenstein.hyperbolicHorizontal line 142
  6. lemma OAI.CubicEisenstein.hyperbolicHorizontal_continuous line 145
  7. lemma OAI.CubicEisenstein.hyperbolicHorizontal_upperPoint line 150
  8. def OAI.CubicEisenstein.hyperbolicCoordinates line 155
  9. lemma OAI.CubicEisenstein.hyperbolicCoordinates_continuous line 158
  10. lemma OAI.CubicEisenstein.upperCoordinates_left_inverse line 161
  11. lemma OAI.CubicEisenstein.upperCoordinates_right_inverse line 167
  12. def OAI.CubicEisenstein.upperCoordinatesHomeomorph line 174
  13. lemma OAI.CubicEisenstein.fundamentalSet_measure_le_cover line 182
  14. def OAI.CubicEisenstein.spatialHeightSplit line 197
  15. lemma OAI.CubicEisenstein.spatialHeightSplit_fst line 201
  16. lemma OAI.CubicEisenstein.spatialHeightSplit_snd_zero line 202
  17. lemma OAI.CubicEisenstein.spatialHeightSplit_snd_one line 203
  18. lemma OAI.CubicEisenstein.spatialHeightSplit_preserves_volume line 205
  19. def OAI.CubicEisenstein.horizontalUnitBox line 209
  20. lemma OAI.CubicEisenstein.horizontalUnitBox_measurable line 210
  21. lemma OAI.CubicEisenstein.horizontalUnitBox_volume line 212
  22. def OAI.CubicEisenstein.euclideanCuspBox line 216
  23. lemma OAI.CubicEisenstein.euclideanCuspBox_measurable line 218
  24. lemma OAI.CubicEisenstein.euclideanCuspBox_positive line 220
  25. theorem OAI.CubicEisenstein.euclideanCuspBox_volume line 224
  26. instance OAI.CubicEisenstein.fullSLMeasurableAction line 245
  27. instance OAI.CubicEisenstein.fullSLVolumeInvariant line 247
  28. def OAI.CubicEisenstein.hyperbolicCuspBox line 252
  29. lemma OAI.CubicEisenstein.hyperbolicCuspBox_measurable line 255
  30. lemma OAI.CubicEisenstein.hyperbolicCuspBox_volume_le line 259
  31. lemma OAI.CubicEisenstein.hyperbolicCuspBox_volume_lt_top line 278
  32. theorem OAI.CubicEisenstein.hyperbolicFundamentalSet_volume_lt_top line 282
  33. lemma OAI.CubicEisenstein.integralQuotientVolume_univ line 312
  34. theorem OAI.CubicEisenstein.integralQuotientVolume_finite line 317
  35. instance OAI.CubicEisenstein.kernelQuotientVolume_finite line 321
  36. theorem OAI.CanonicalQuadraticSieve.improved_threshold_ge_column line 331
  37. theorem OAI.CanonicalQuadraticSieve.improved_threshold_power line 341
  38. theorem OAI.CanonicalQuadraticSieve.improved_threshold_main line 348
  39. theorem OAI.CanonicalQuadraticSieve.improved_threshold_shape line 357
  40. theorem OAI.CanonicalQuadraticSieve.improved_threshold_reciprocal line 362
  41. theorem OAI.CanonicalQuadraticSieve.improved_threshold_low line 371
  42. theorem OAI.CanonicalQuadraticSieve.sieveNorm_large_rows line 390
  43. theorem OAI.CanonicalQuadraticSieve.hasSieveExponent_of_threshold_band line 404
  44. theorem OAI.CanonicalQuadraticSieve.hasSieveExponent_of_shell_threshold line 459
  45. def OAI.CanonicalQuadraticSieve.fixedBadNorm line 547
  46. def OAI.CanonicalQuadraticSieve.fixedCutoffBase line 548
  47. theorem OAI.CanonicalQuadraticSieve.fixedBadNorm_one_le line 550
  48. theorem OAI.CanonicalQuadraticSieve.fixedCutoffBase_bounds line 563
  49. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.annular_selected_bound line 566