OAI/NumberTheory/DirichletL/GaussSum/GlobalScales.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompletedGauss.largeCubeCoefficient_small_power line 76
  2. def OAI.SecondPassArithmetic.globalRowScaleFloor line 92
  3. theorem OAI.SecondPassArithmetic.globalRowScaleFloor_pos line 95
  4. theorem OAI.SecondPassArithmetic.globalNormCaps_antitone_row line 100
  5. theorem OAI.SecondPassArithmetic.globalRowScaleFloor_le_pooled line 114
  6. theorem OAI.SecondPassArithmetic.globalScaleIndex_mem_uniform_box line 142
  7. def OAI.SecondPassArithmetic.weightedGlobalArithmeticBinSource line 177
  8. theorem OAI.SecondPassArithmetic.weightedGlobalArithmeticBinSource_squarefree line 187
  9. theorem OAI.SecondPassArithmetic.full_uniform_weightedGlobalArithmeticBin_transfer line 213
  10. theorem OAI.SecondPassArithmetic.weightedGlobalPositiveBin_transfer line 281
  11. theorem OAI.SecondPassArithmetic.fixedSecondTest_subunit line 362
  12. theorem OAI.SecondPassIntegration.childEnergy_subunit line 382
  13. theorem OAI.SecondPassIntegration.densityChildEnergy_subunit line 394
  14. theorem OAI.SecondPassIntegration.childDensity_elementary_all_scales line 402
  15. def OAI.SecondPassArithmetic.globalTerminalConstant line 432
  16. def OAI.SecondPassArithmetic.globalRayTripleConstant line 435
  17. theorem OAI.SecondPassArithmetic.globalTerminalConstant_nonneg line 437
  18. theorem OAI.SecondPassArithmetic.radial_decay_step line 443
  19. theorem OAI.SecondPassArithmetic.globalPooledRow_radial_bound line 451
  20. theorem OAI.SecondPassArithmetic.globalRadialBin_terminal_bound line 472
  21. theorem OAI.SecondPassArithmetic.globalRadialBin_terminal_bound_all_bins line 567
  22. def OAI.CanonicalQuadraticSieve.liftingPrimeElement line 621
  23. def OAI.CanonicalQuadraticSieve.liftingPrime line 622
  24. theorem OAI.CanonicalQuadraticSieve.liftingPrimeElement_norm line 624
  25. theorem OAI.CanonicalQuadraticSieve.liftingPrime_norm line 629
  26. theorem OAI.CanonicalQuadraticSieve.liftingPrime_prime line 632
  27. theorem OAI.CanonicalQuadraticSieve.liftingPrime_supported line 642
  28. theorem OAI.CanonicalQuadraticSieve.liftingPrime_admissible line 666
  29. theorem OAI.CanonicalQuadraticSieve.supported_pow line 669
  30. theorem OAI.CanonicalQuadraticSieve.exists_lifting_exponent line 682
  31. def OAI.CanonicalQuadraticSieve.liftingExponent line 696
  32. def OAI.CanonicalQuadraticSieve.liftedRow line 699
  33. theorem OAI.CanonicalQuadraticSieve.liftedRow_norm line 702
  34. theorem OAI.CanonicalQuadraticSieve.liftedRow_bounds line 708
  35. theorem OAI.CanonicalQuadraticSieve.liftedRow_squarefreePart line 714
  36. theorem OAI.CanonicalQuadraticSieve.liftedRow_supported line 718
  37. theorem OAI.CanonicalQuadraticSieve.liftedRow_character line 723
  38. theorem OAI.CanonicalQuadraticSieve.liftedRow_injective line 732