OAI/NumberTheory/PrimePackets/IntegerEmbeddings.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.integerEmbeddingMatrix line 140
  2. lemma OAI.PrimeDegreePackets.integerEmbeddingMatrix_det_ne_zero line 144
  3. def OAI.PrimeDegreePackets.integerEuclideanBasis line 161
  4. lemma OAI.PrimeDegreePackets.integerEuclideanBasis_apply line 167
  5. def OAI.PrimeDegreePackets.residueCharacterTheta line 180
  6. lemma OAI.PrimeDegreePackets.residueCharacterTheta_eq line 185
  7. def OAI.PrimeDegreePackets.orderedIntegerBasis line 197
  8. theorem OAI.PrimeDegreePackets.residueCharacterTheta_mellin_entire line 204
  9. lemma OAI.PrimeDegreePackets.residueCharacterTheta_mellin_convergent line 211
  10. def OAI.PrimeDegreePackets.rationalUnitReduction line 226
  11. def OAI.PrimeDegreePackets.rationalCongruenceUnits line 230
  12. lemma OAI.PrimeDegreePackets.mem_rationalCongruenceUnits line 233
  13. lemma OAI.PrimeDegreePackets.rationalCongruenceUnits_finiteIndex line 239
  14. lemma OAI.PrimeDegreePackets.rationalCongruenceUnits_index line 247
  15. lemma OAI.PrimeDegreePackets.residueCharacter_congruenceUnit_mul line 251
  16. lemma OAI.PrimeDegreePackets.rationalCongruenceUnits_log_lattice line 258
  17. def OAI.PrimeDegreePackets.subgroupUnitLogOnto line 274
  18. lemma OAI.PrimeDegreePackets.subgroupUnitLogOnto_surjective line 281
  19. def OAI.PrimeDegreePackets.subgroupUnitLogKernelEmbedding line 287
  20. instance OAI.PrimeDegreePackets.subgroupUnitLogOnto_ker_finite line 301
  21. lemma OAI.PrimeDegreePackets.subgroupUnitLogOnto_ker_unit_eq_one_or_neg_one line 310
  22. lemma OAI.PrimeDegreePackets.subgroupUnitLogOnto_ker_card_le_two line 317
  23. theorem OAI.PrimeDegreePackets.lintegral_arithmeticFlowGaussian_subgroup line 326
  24. def OAI.PrimeDegreePackets.ThetaConstruction.moduleResidueEquiv line 352
  25. lemma OAI.PrimeDegreePackets.ThetaConstruction.rationalModulus_nsmul line 357
  26. def OAI.PrimeDegreePackets.ThetaConstruction.idealModNReduction line 365
  27. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealModNReduction_mk line 370
  28. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealModNReduction_surjective line 374
  29. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealModNReduction_bijective line 388
  30. def OAI.PrimeDegreePackets.ThetaConstruction.idealResidueEquiv line 399
  31. def OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterWeight line 405
  32. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterWeight_sum_zero line 409
  33. lemma OAI.PrimeDegreePackets.ThetaConstruction.moduleResidueEquiv_zero line 419
  34. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterWeight_zero line 427
  35. theorem OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_uniform_positive_scale_bound line 442
  36. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_joint_stronglyMeasurable line 503
  37. def OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail line 521
  38. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_eq_zero line 524
  39. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_stronglyMeasurable line 528
  40. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_uniform_bound line 534
  41. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_integrable_average line 557
  42. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_bounds line 568
  43. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_locallyIntegrable line 605
  44. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_bigO_zero line 619
  45. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_bigO_exp line 627
  46. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_mellin_entire line 636
  47. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedWeightedThetaTail_mellin_convergent line 648