OAI/NumberTheory/PrimePackets/LatticeDuality.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_selfAdjoint line 89
  2. lemma OAI.PrimeDegreePackets.ThetaConstruction.adjointEquiv_logScaledLattice line 99
  3. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_det line 113
  4. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScaledLattice_det line 123
  5. lemma OAI.PrimeDegreePackets.restoredLogCoordinates_sum line 136
  6. lemma OAI.PrimeDegreePackets.restoredLogCoordinates_neg line 140
  7. theorem OAI.PrimeDegreePackets.arithmeticFlowTheta_inversion line 147
  8. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaXi_reflection line 163
  9. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaXi_average_reflection line 178
  10. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedThetaMellinXi_differentiable line 197
  11. lemma OAI.PrimeDegreePackets.restoredLogCoordinates_abs_bound_on_compact line 246
  12. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaXi_boundedAverage_entire line 258
  13. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaXi_unitAverage_entire line 328
  14. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaXi_average_eq_epstein line 339
  15. def OAI.PrimeDegreePackets.arithmeticFlowGaussian line 374
  16. lemma OAI.PrimeDegreePackets.arithmeticFlowGaussian_measurable line 378
  17. lemma OAI.PrimeDegreePackets.arithmeticFlowGaussian_unit_translate line 390
  18. theorem OAI.PrimeDegreePackets.lintegral_arithmeticFlowGaussian_units line 405
  19. theorem OAI.PrimeDegreePackets.lintegral_arithmeticFlowGaussian_ideal line 423
  20. def OAI.PrimeDegreePackets.fractionalIdealNonzeroIntegerEquiv line 459
  21. lemma OAI.PrimeDegreePackets.normalizedTheta_fractionalIdeal_gaussian_sum line 486
  22. theorem OAI.PrimeDegreePackets.fractionalIdealTheta_unit_unfolding line 518