OAI/NumberTheory/PrimePackets/IdealThetaFlow.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.idealUnitMulEquiv line 143
  2. lemma OAI.PrimeDegreePackets.idealResidueFlowTheta_eq_complex line 152
  3. lemma OAI.PrimeDegreePackets.idealResidueFlowTheta_unit_covariance line 166
  4. lemma OAI.PrimeDegreePackets.idealResidueFlowTheta_congruence_periodic line 179
  5. def OAI.PrimeDegreePackets.rationalCongruenceLogDomain line 192
  6. lemma OAI.PrimeDegreePackets.rationalCongruenceLogDomain_fundamental line 199
  7. lemma OAI.PrimeDegreePackets.rationalCongruenceLogDomain_measurable line 207
  8. lemma OAI.PrimeDegreePackets.rationalCongruenceLogDomain_bounded line 213
  9. theorem OAI.PrimeDegreePackets.idealResidueFlowTheta_congruenceAverage_entire line 221
  10. theorem OAI.PrimeDegreePackets.subgroupUnitGaussian_mellin_lintegral line 233
  11. lemma OAI.PrimeDegreePackets.complex_tsum_comp_surjective_addHom line 255
  12. theorem OAI.PrimeDegreePackets.integral_tsum_addHom_fundamentalDomain_complex line 282
  13. lemma OAI.PrimeDegreePackets.integral_complexFlowGaussian_subgroup line 318
  14. lemma OAI.PrimeDegreePackets.complexFlowGaussian_eq_ofReal line 347
  15. lemma OAI.PrimeDegreePackets.radialKernel_eq_complexFlowGaussian line 358
  16. lemma OAI.PrimeDegreePackets.complexFlowGaussian_ae_integrable line 369
  17. theorem OAI.PrimeDegreePackets.subgroupUnitGaussian_mellin line 383
  18. def OAI.PrimeDegreePackets.idealIntegerElement line 420
  19. lemma OAI.PrimeDegreePackets.idealIntegerElement_coe line 424
  20. lemma OAI.PrimeDegreePackets.idealIntegerElement_unitAction line 429
  21. def OAI.PrimeDegreePackets.idealResidueElementWeight line 437
  22. lemma OAI.PrimeDegreePackets.idealResidueElementWeight_unitAction line 442
  23. lemma OAI.PrimeDegreePackets.idealResidueElementWeight_congruence line 450
  24. def OAI.PrimeDegreePackets.idealResidueCoefficient line 460
  25. lemma OAI.PrimeDegreePackets.idealResidueCoefficient_eq_of_generator line 467
  26. lemma OAI.PrimeDegreePackets.finiteMulChar_norm_le_one line 480
  27. lemma OAI.PrimeDegreePackets.idealResidueElementWeight_norm_le_one line 494
  28. lemma OAI.PrimeDegreePackets.idealResidueCoefficient_summable line 504
  29. lemma OAI.PrimeDegreePackets.measurable_complexFlowGaussian_joint line 530
  30. lemma OAI.PrimeDegreePackets.enorm_complexFlowGaussian line 537
  31. def OAI.PrimeDegreePackets.unitOrbitMellinKernel line 545
  32. lemma OAI.PrimeDegreePackets.measurable_unitOrbitMellinKernel line 550
  33. lemma OAI.PrimeDegreePackets.enorm_unitOrbitMellinKernel_le line 563
  34. lemma OAI.PrimeDegreePackets.lintegral_enorm_unitOrbitMellinKernel_le line 582
  35. theorem OAI.PrimeDegreePackets.integrable_unitOrbitMellinKernel line 606
  36. theorem OAI.PrimeDegreePackets.integral_unitOrbitMellinKernel line 626