OAI/NumberTheory/DirichletL/CubicSieve/ScaleCaps.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.finiteBlockExponent line 83
  2. def OAI.SecondPassArithmetic.cubeCoordinatesOfBlock line 89
  3. theorem OAI.SecondPassArithmetic.cubeCoordinatesOfBlock_support line 95
  4. theorem OAI.SecondPassArithmetic.cubeCoordinatesOfBlock_leftBit line 106
  5. theorem OAI.SecondPassArithmetic.cubeCoordinatesOfBlock_rightBit line 110
  6. theorem OAI.SecondPassArithmetic.cubeCoordinatesOfBlock_admissible line 114
  7. theorem OAI.SecondPassArithmetic.cubeCoordinatesOfBlock_primeProduct line 120
  8. def OAI.SecondPassArithmetic.globalSecondOfBlock line 136
  9. theorem OAI.SecondPassArithmetic.globalSecondOfBlock_injective line 144
  10. theorem OAI.SecondPassArithmetic.globalSecondOfBlock_admissible line 149
  11. theorem OAI.SecondPassArithmetic.globalSecondOfBlock_tuple line 160
  12. theorem OAI.SecondPassArithmetic.globalSecondOfBlock_triple line 182
  13. theorem OAI.SecondPassArithmetic.globalSecondOfBlock_label line 194
  14. abbrev OAI.SecondPassArithmetic.GlobalLogIndex line 214
  15. def OAI.SecondPassArithmetic.globalLogRep line 216
  16. theorem OAI.SecondPassArithmetic.globalLogRep_pos line 218
  17. theorem OAI.SecondPassArithmetic.globalLogRep_ge_one line 220
  18. def OAI.SecondPassArithmetic.globalScaleVector line 226
  19. def OAI.SecondPassArithmetic.globalScaleIndex line 233
  20. theorem OAI.SecondPassArithmetic.globalScaleVector_ge_one line 237
  21. theorem OAI.SecondPassArithmetic.globalScaleIndex_bounds line 256
  22. theorem OAI.SecondPassArithmetic.globalScaleIndex_error line 263
  23. def OAI.SecondPassArithmetic.globalLogSector line 269
  24. def OAI.SecondPassArithmetic.globalLogBox line 274
  25. theorem OAI.SecondPassArithmetic.globalLogBox_card line 277
  26. theorem OAI.SecondPassArithmetic.globalScaleIndex_mem_box line 281
  27. theorem OAI.SecondPassArithmetic.sum_globalLogSector line 291
  28. def OAI.SecondPassArithmetic.globalPooledColumnScale line 300
  29. def OAI.SecondPassArithmetic.globalPooledLabelScale line 303
  30. def OAI.SecondPassArithmetic.globalPooledRowScale line 306
  31. def OAI.SecondPassArithmetic.globalPooledDelta line 309
  32. def OAI.SecondPassArithmetic.globalPooledNaturalRow line 312
  33. theorem OAI.SecondPassArithmetic.globalPooledColumnScale_pos line 315
  34. theorem OAI.SecondPassArithmetic.globalPooledLabelScale_ge_one line 323
  35. theorem OAI.SecondPassArithmetic.globalPooled_mass line 330
  36. theorem OAI.SecondPassArithmetic.globalPooled_radial_ratio line 337
  37. theorem OAI.CanonicalQuadraticSieve.maskedPairDualTail_bound line 352
  38. theorem OAI.CanonicalQuadraticSieve.coprime_pair_error_energy line 422
  39. theorem OAI.CanonicalQuadraticSieve.maskedDualTailFamily_bound line 453
  40. def OAI.SecondPassArithmetic.globalActualResidualScale line 495
  41. theorem OAI.SecondPassArithmetic.globalActualResidualScale_pos line 502
  42. theorem OAI.SecondPassArithmetic.globalPooled_log_coordinates line 510
  43. theorem OAI.SecondPassArithmetic.globalPooled_target_bounds line 568
  44. theorem OAI.SecondPassArithmetic.five_factor_bounds line 604
  45. theorem OAI.SecondPassArithmetic.globalSupported_small_norms line 629
  46. theorem OAI.SecondPassArithmetic.globalCube_radical_bound line 659
  47. theorem OAI.SecondPassArithmetic.globalSupported_divisor_bound line 677
  48. theorem OAI.SecondPassArithmetic.globalSupported_cutoff_row_bound line 693
  49. def OAI.SecondPassArithmetic.globalNormCaps line 743
  50. theorem OAI.SecondPassArithmetic.globalScaleVector_le_caps line 748
  51. theorem OAI.SecondPassArithmetic.globalScaleIndex_mem_concrete_box line 779