OAI/NumberTheory/DirichletL/Cusp/WeylRepresentatives.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortDraftCusp.A3WeylCusp line 83
  2. lemma OAI.ShortDraftCusp.A3_ramified_relative_matrix line 86
  3. lemma OAI.ShortDraftCusp.A3_unramified_relative_matrix line 94
  4. lemma OAI.ShortDraftCusp.A3_principal_mem_levelThree line 102
  5. lemma OAI.ShortDraftCusp.A3_ramified_mem_levelThree line 109
  6. lemma OAI.ShortDraftCusp.A3_unramified_mem_levelThree line 122
  7. lemma OAI.ShortDraftCusp.A3_principal_character line 140
  8. lemma OAI.ShortDraftCusp.A3_ramified_literal_character line 147
  9. lemma OAI.ShortDraftCusp.A3_unramified_literal_character line 157
  10. theorem OAI.ShortDraftCusp.A3_ramified_character line 167
  11. theorem OAI.ShortDraftCusp.A3_unramified_character line 185
  12. lemma OAI.CubicEisenstein.fixedCuspArrayIndex_ne_zero line 215
  13. lemma OAI.CubicEisenstein.fixedCuspArrayIndex_norm_sq line 220
  14. lemma OAI.CubicEisenstein.fixedCuspArrayIndex_norm line 233
  15. lemma OAI.CubicEisenstein.fixedCuspArrayWeight_div_norm line 239
  16. theorem OAI.CubicEisenstein.fixedConjugateCuspArray_div_norm line 253
  17. lemma OAI.CubicEisenstein.thetaFullFrequency_eq_fixedCuspArrayIndex line 279
  18. lemma OAI.CubicEisenstein.sourceCuspRadialLength_full_index line 282
  19. lemma OAI.CubicEisenstein.thetaRamifiedScale_eq line 289
  20. lemma OAI.CubicEisenstein.thetaRamifiedScale_cube line 296
  21. lemma OAI.CubicEisenstein.sourceCusp_full_index_kernel_argument line 302
  22. def OAI.CubicEisenstein.sourceFrequencyAngle line 309
  23. lemma OAI.CubicEisenstein.sourceFrequencyAngle_norm line 311
  24. lemma OAI.CubicEisenstein.sourceCuspRadialCoefficient_angle line 315
  25. def OAI.CubicEisenstein.fixedRadialCoefficientScalar line 330
  26. theorem OAI.CubicEisenstein.sourceCuspRadialCoefficient_fixed_array line 333
  27. lemma OAI.CubicEisenstein.thetaFullIndex_denominator_pos line 355
  28. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothed_unit_phase_norm line 367
  29. theorem OAI.CubicEisenstein.SourceCuspDatum.smoothedFullCoefficient_normalization line 372
  30. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothedFullCoefficient_norm_le line 391
  31. theorem OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel_fixed_array line 408
  32. theorem OAI.CanonicalRowCompletion.idealRowHom_congr_mod line 436
  33. lemma OAI.CanonicalRowCompletion.sexticReciprocityPhase_congr_right line 454
  34. lemma OAI.CanonicalRowCompletion.sexticReciprocityPhase_norm line 459
  35. def OAI.CanonicalRowCompletion.reciprocalRow line 463
  36. lemma OAI.CanonicalRowCompletion.reciprocalRow_norm line 470
  37. lemma OAI.CanonicalRowCompletion.reciprocalRow_periodic line 477
  38. lemma OAI.CanonicalRowCompletion.reciprocalRow_eq_idealRowHom line 486
  39. def OAI.CubicEisenstein.FixedCuspShape.amplitude line 507
  40. lemma OAI.CubicEisenstein.FixedCuspShape.amplitude_norm line 513
  41. theorem OAI.CubicEisenstein.FixedCuspShape.smoothedKernel_fixed_shape line 522
  42. lemma OAI.CubicEisenstein.FixedCuspShape.smoothed_row_factor line 554
  43. lemma OAI.ShortDraftCRT.exists_controlled_inverse line 572
  44. lemma OAI.ShortDraftCRT.exists_controlled_zero_inverse line 578
  45. lemma OAI.ShortDraftCRT.fixed_completion_upper_right_dvd line 587
  46. theorem OAI.ShortDraftCRT.exists_fixed_completion_upper_right line 602
  47. theorem OAI.ShortDraftCRT.exists_fixed_completion_lower_right line 611
  48. theorem OAI.ShortDraftCRT.controlled_completion_matrix_congr line 624