OAI/NumberTheory/DirichletL/Arithmetic/SquarefreeDivisors.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SquarefreeDivisorBound.O line 76
  2. theorem OAI.SquarefreeDivisorBound.squarefree_divisor_card_le line 78
  3. theorem OAI.SquarefreeDivisorBound.prime_support_subsets_bound line 83
  4. theorem OAI.SquarefreeDivisorBound.squarefree_divisor_small_power line 128
  5. theorem OAI.SquarefreeDivisorBound.first_element_squarefree_fiber line 140
  6. theorem OAI.SquarefreeDivisorBound.first_element_fiber_small_power line 174
  7. theorem OAI.SquarefreeDivisorBound.first_element_energy_small_power line 192
  8. theorem OAI.VerticalContourShift.horizontal_integral_tendsto_zero line 222
  9. theorem OAI.VerticalContourShift.integral_eq_of_strip_decay line 239
  10. abbrev OAI.FirstPassCubeLabels.O line 298
  11. def OAI.FirstPassCubeLabels.bit line 301
  12. def OAI.FirstPassCubeLabels.conductorExponent line 303
  13. def OAI.FirstPassCubeLabels.crtExponent line 306
  14. def OAI.FirstPassCubeLabels.dilationExponent line 311
  15. def OAI.FirstPassCubeLabels.retained line 314
  16. theorem OAI.FirstPassCubeLabels.exponent_table line 316
  17. theorem OAI.FirstPassCubeLabels.row_pow line 325
  18. theorem OAI.FirstPassCubeLabels.row_prod line 329
  19. theorem OAI.FirstPassCubeLabels.row_sixth line 338
  20. theorem OAI.FirstPassCubeLabels.mask_mul line 345
  21. theorem OAI.FirstPassCubeLabels.mask_pow line 349
  22. theorem OAI.FirstPassCubeLabels.mask_prod line 354
  23. theorem OAI.FirstPassCubeLabels.row_zero_of_mask_zero line 359
  24. theorem OAI.FirstPassCubeLabels.row_power_mul_mask_power line 365
  25. def OAI.FirstPassCubeLabels.localFactor line 374
  26. theorem OAI.FirstPassCubeLabels.localFactor_eq line 380
  27. def OAI.FirstPassCubeLabels.parity line 396
  28. def OAI.FirstPassCubeLabels.evenDouble line 398
  29. def OAI.FirstPassCubeLabels.b0Exponent line 400
  30. theorem OAI.FirstPassCubeLabels.multiplicity_decomposition line 402
  31. theorem OAI.FirstPassCubeLabels.b0Exponent_pos_of_not_retained line 409
  32. theorem OAI.FirstPassCubeLabels.localFactor_eq_b0 line 420
  33. def OAI.FirstPassCubeLabels.primeProduct line 434
  34. def OAI.FirstPassCubeLabels.cubeRadical line 436
  35. def OAI.FirstPassCubeLabels.aLabel line 438
  36. def OAI.FirstPassCubeLabels.crtLabel line 441
  37. def OAI.FirstPassCubeLabels.dilationLabel line 445
  38. def OAI.FirstPassCubeLabels.jLabel line 449
  39. def OAI.FirstPassCubeLabels.j2Label line 453
  40. def OAI.FirstPassCubeLabels.squarefreeLabel line 457
  41. def OAI.FirstPassCubeLabels.b0Label line 460
  42. theorem OAI.FirstPassCubeLabels.first_pass_label_identity line 464
  43. theorem OAI.FirstPassCubeLabels.cube_product_decomposition line 482
  44. theorem OAI.FirstPassCubeLabels.jLabel_eq_squarefree_mul_j2 line 494
  45. theorem OAI.FirstPassCubeLabels.radical_mask_absorbs line 507
  46. theorem OAI.FirstPassCubeLabels.masked_dual_dilation line 517
  47. theorem OAI.FirstPassCubeLabels.first_pass_after_dual_dilation line 529
  48. theorem OAI.FirstPassCubeLabels.cube_pair_product_decomposition line 548
  49. theorem OAI.FirstPassCubeLabels.mobius_column_after_dual_dilation line 560
  50. def OAI.QuadraticInitialBound.quadraticSymbol line 588
  51. theorem OAI.QuadraticInitialBound.quadraticSymbol_eq_cross_product line 592
  52. theorem OAI.QuadraticInitialBound.quadraticSymbol_mul_reverse line 599
  53. theorem OAI.QuadraticInitialBound.quadraticSymbol_eq_zero_of_not_disjoint line 607
  54. theorem OAI.QuadraticInitialBound.quadraticSymbol_sq_eq_one line 619
  55. theorem OAI.QuadraticInitialBound.quadraticSymbol_reciprocity line 639
  56. theorem OAI.QuadraticInitialBound.quadraticSymbol_reciprocity_characters line 657