OAI/NumberTheory/PrimePackets/XiBoundary.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.completedXiBoundaryValue line 75
  2. lemma OAI.PrimeDegreePackets.completedXiBoundaryValue_eq line 79
  3. lemma OAI.PrimeDegreePackets.completedXiBoundaryValue_ne_zero line 97
  4. lemma OAI.PrimeDegreePackets.tendsto_completedXi_from_right line 105
  5. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_one line 126
  6. lemma OAI.PrimeDegreePackets.totallyRealCompletedXi_not_continuousAt_one line 131
  7. theorem OAI.PrimeDegreePackets.bounded_discriminant_zeta_scale line 148
  8. theorem OAI.PrimeDegreePackets.weightedIdeal_realInterval_bounded_discriminant line 170
  9. theorem OAI.PrimeDegreePackets.packet_cube_moment_bounded_discriminant line 200
  10. theorem OAI.PrimeDegreePackets.packet_tight_bounded_discriminant line 237
  11. theorem OAI.PrimeDegreePackets.packet_probability_subsequence_bounded_discriminant line 292
  12. theorem OAI.PrimeDegreePackets.packet_box_moment_bounded_discriminant line 323
  13. theorem OAI.PrimeDegreePackets.packet_ball_bound_bounded_discriminant line 362
  14. theorem OAI.PrimeDegreePackets.packet_limit_ball_bound_bounded_discriminant line 402
  15. theorem OAI.PrimeDegreePackets.packet_limit_positive_ergodic_components_bounded_discriminant line 425
  16. def OAI.PrimeDegreePackets.ThetaConstruction.integerVector line 458
  17. def OAI.PrimeDegreePackets.ThetaConstruction.torusProjection line 460
  18. lemma OAI.PrimeDegreePackets.ThetaConstruction.torusProjection_openQuotient line 463
  19. lemma OAI.PrimeDegreePackets.ThetaConstruction.torusProjection_eq_iff line 467
  20. def OAI.PrimeDegreePackets.ThetaConstruction.translate line 483
  21. def OAI.PrimeDegreePackets.ThetaConstruction.LocallyNormal line 486
  22. def OAI.PrimeDegreePackets.ThetaConstruction.periodizedReal line 490
  23. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodizedReal_apply line 492
  24. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodizedReal_per line 497
  25. def OAI.PrimeDegreePackets.ThetaConstruction.torusRepresentative line 509
  26. lemma OAI.PrimeDegreePackets.ThetaConstruction.torusProjection_representative line 513
  27. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodizedReal_representative line 517
  28. def OAI.PrimeDegreePackets.ThetaConstruction.periodizedTorus line 525
  29. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodizedTorus_apply line 535
  30. instance OAI.PrimeDegreePackets.ThetaConstruction.integerTranslationAction line 542
  31. instance OAI.PrimeDegreePackets.ThetaConstruction.integerTranslationMeasurable line 553
  32. instance OAI.PrimeDegreePackets.ThetaConstruction.integerTranslationPreservesVolume line 556
  33. def OAI.PrimeDegreePackets.ThetaConstruction.unitCube line 561
  34. lemma OAI.PrimeDegreePackets.ThetaConstruction.unitCube_fundamental line 563
  35. lemma OAI.PrimeDegreePackets.ThetaConstruction.integral_periodization line 579
  36. lemma OAI.PrimeDegreePackets.ThetaConstruction.torusProjection_add_integer line 598
  37. def OAI.PrimeDegreePackets.ThetaConstruction.fourierCharacter line 602
  38. lemma OAI.PrimeDegreePackets.ThetaConstruction.fourierCharacter_norm line 605
  39. lemma OAI.PrimeDegreePackets.ThetaConstruction.fourierCharacter_periodic line 610
  40. lemma OAI.PrimeDegreePackets.ThetaConstruction.integrable_character_mul line 616
  41. lemma OAI.PrimeDegreePackets.ThetaConstruction.fourierCoeff_periodizedTorus line 623
  42. theorem OAI.PrimeDegreePackets.ThetaConstruction.multivariate_poisson line 642