OAI/NumberTheory/PrimePackets/UnitOrbitIntegrals.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.tsum_lintegral_unitOrbitMellinKernel_ne_top line 146
  2. lemma OAI.PrimeDegreePackets.tsum_lintegral_weightedUnitOrbitMellinKernel_ne_top line 174
  3. theorem OAI.PrimeDegreePackets.integral_weightedIdealUnitOrbits line 197
  4. lemma OAI.PrimeDegreePackets.summable_norm_complexFlowGaussian_ideal line 239
  5. lemma OAI.PrimeDegreePackets.summable_residueWeightedGaussian line 249
  6. theorem OAI.PrimeDegreePackets.residueWeightedGaussian_ideal_units line 265
  7. def OAI.PrimeDegreePackets.integralIdealNonzeroEquiv line 295
  8. lemma OAI.PrimeDegreePackets.idealResidueFlowTheta_nonzero line 319
  9. theorem OAI.PrimeDegreePackets.idealResidueFlowTheta_ideal_units line 350
  10. lemma OAI.PrimeDegreePackets.integrable_weightedIdealUnitOrbits line 373
  11. lemma OAI.PrimeDegreePackets.unitOrbitMellinKernel_top line 401
  12. lemma OAI.PrimeDegreePackets.residueMellinKernel_eq_ideal_sum line 412
  13. theorem OAI.PrimeDegreePackets.idealResidueFlowTheta_mellin line 431
  14. theorem OAI.PrimeDegreePackets.idealResidueCompleted_entire line 472
  15. def OAI.PrimeDegreePackets.residueIdealMellinFactor line 492
  16. lemma OAI.PrimeDegreePackets.residueIdealMellinFactor_ne_zero line 496
  17. def OAI.PrimeDegreePackets.residueIdealContinued line 506
  18. theorem OAI.PrimeDegreePackets.residueIdealContinued_entire line 515
  19. theorem OAI.PrimeDegreePackets.residueIdealContinued_eq_series line 529