OAI/NumberTheory/DirichletL/Cusp/ResiduePhases.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ShortDraftCusp.A4_bad_modulus_ne_zero line 83
  2. def OAI.ShortDraftCusp.A4BadPhase line 91
  3. lemma OAI.ShortDraftCusp.A4BadPhase_eq line 95
  4. theorem OAI.ShortDraftCusp.A4_phase_product line 109
  5. theorem OAI.ShortDraftCusp.A3_A4_frequency_product line 168
  6. lemma OAI.ShortDraftCusp.A4BadPhase_eq_of_residue line 201
  7. lemma OAI.ShortDraftCusp.A4BadPhase_norm line 211
  8. lemma OAI.IdealGaussCRT.finiteAdditiveFourierCoeff_mulShift line 223
  9. theorem OAI.IdealGaussCRT.finite_fourier_weighted_shift_crt line 235
  10. theorem OAI.IdealGaussCRT.finiteAdditiveFourierCoeff_pair line 251
  11. theorem OAI.LocalReflectionBrackets.canonical_finite_reflection_shifted_crt line 289
  12. theorem OAI.FiniteGaussPhase.exists_product_trace_shifts line 332
  13. def OAI.FiniteGaussPhase.productTraceShift line 355
  14. lemma OAI.FiniteGaussPhase.productTraceShift_inverse line 361
  15. lemma OAI.FiniteGaussPhase.productTraceShift_character line 368
  16. theorem OAI.FiniteGaussPhase.product_trace_fourier_factor line 382
  17. theorem OAI.FiniteGaussPhase.product_trace_fourier_weighted line 397
  18. theorem OAI.LocalReflectionBrackets.canonical_product_reflection_crt line 421
  19. theorem OAI.ShortDraftCusp.A4BadPhase_strong_sector line 462
  20. def OAI.ShortDraftCusp.A4PhaseFromResidue line 477
  21. lemma OAI.ShortDraftCusp.A4BadPhase_as_fixed_residue line 482
  22. lemma OAI.ShortDraftCusp.A4PhaseFromResidue_range line 488
  23. lemma OAI.CompletedGauss.columnWeight_congr_primary line 507
  24. lemma OAI.CompletedGauss.cubeWeight_congr_primary line 513
  25. theorem OAI.CompletedGauss.completedT_congr_primary line 522
  26. lemma OAI.CompletedGauss.completedMellinCoefficient_congr_primary line 530
  27. theorem OAI.CompletedGauss.completedBesselProfile_congr_primary line 535
  28. lemma OAI.CubicEisenstein.fixedThetaTwist_congr_primary line 546
  29. def OAI.ShortDraftCRT.finiteCrossNumerator line 561
  30. lemma OAI.ShortDraftCRT.prime_dvd_other_cofactor line 564
  31. lemma OAI.ShortDraftCRT.finiteCrossNumerator_local line 567
  32. lemma OAI.ShortDraftCRT.finiteCrossNumerator_fixed line 587
  33. lemma OAI.ShortDraftCRT.finiteCrossNumerator_fixed_sector line 592
  34. lemma OAI.ShortDraftCRT.finiteCrossNumerator_coprime line 604