OAI/NumberTheory/DirichletL/Arithmetic/NormFiberMellin.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ShortDraftLocal.no_quadratic_scalar line 33
  2. theorem OAI.ActualEisensteinCubic.canonical_A5_jtwo_direct line 52
  3. theorem OAI.ActualEisensteinCubic.canonical_A5_jzero_direct_active line 76
  4. theorem OAI.ActualEisensteinCubic.canonical_A5_jzero_direct_full line 97
  5. def OAI.ShortDraftHeckeBridge.chiMinusThree line 124
  6. def OAI.ShortDraftHeckeBridge.baseChangeWeight line 127
  7. theorem OAI.ShortDraftHeckeBridge.baseChangeWeight_prime line 131
  8. def OAI.ShortDraftHeckeBridge.invCharAF line 137
  9. theorem OAI.ShortDraftHeckeBridge.invCharAF_apply line 140
  10. theorem OAI.ShortDraftHeckeBridge.invCharAF_mult line 148
  11. def OAI.ShortDraftHeckeBridge.pairAF line 153
  12. theorem OAI.ShortDraftHeckeBridge.pairAF_mult line 157
  13. theorem OAI.ShortDraftHeckeBridge.pairAF_eq_pairInverseCoeff line 162
  14. theorem OAI.ShortDraftHeckeBridge.normFiber_eq_pair_of_prime_powers line 171
  15. theorem OAI.ShortDraftHeckeBridge.pairAF_prime line 190
  16. theorem OAI.ShortDraftHeckeBridge.pairAF_prime_sq line 209
  17. theorem OAI.ShortDraftHeckeBridge.chiMinusThree_two line 254
  18. theorem OAI.ShortDraftHeckeBridge.chiMinusThree_ne_one line 262
  19. theorem OAI.ShortDraftHeckeBridge.not_both_principal line 271
  20. def OAI.ShortDraftHeckeBridge.normFiberExpSum line 289
  21. def OAI.ShortDraftHeckeBridge.normFiberMellin line 292
  22. theorem OAI.ShortDraftHeckeBridge.pairInverseCoeff_zero line 295
  23. theorem OAI.ShortDraftHeckeBridge.pairInverseCoeff_LSeriesSummable line 300
  24. theorem OAI.ShortDraftHeckeBridge.mobius_char_coeff_norm_le_one line 315
  25. theorem OAI.ShortDraftHeckeBridge.pairInverseCoeff_norm_le line 327
  26. theorem OAI.ShortDraftHeckeBridge.normFiberCoeff_norm_le line 356
  27. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_summable line 369
  28. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_continuousOn_pos line 390
  29. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_inv_locallyIntegrableOn_pos line 436
  30. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_norm_le_exp line 454
  31. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_flat_at_zero line 511
  32. theorem OAI.ShortDraftHeckeBridge.normFiberExpSum_mellin line 547
  33. theorem OAI.ShortDraftHeckeBridge.normFiberMellin_analytic line 565
  34. theorem OAI.ShortDraftHeckeBridge.normFiberMellin_eq_LSeries line 594
  35. theorem OAI.ShortDraftHeckeBridge.pair_zero_free_of_normFiber_exp_power_bound line 608
  36. theorem OAI.ShortDraftHeckeBridge.normFiberMellin_analytic_of_coeff line 633
  37. theorem OAI.ShortDraftHeckeBridge.normFiberMellin_eq_LSeries_of_coeff line 647
  38. theorem OAI.ShortDraftHeckeBridge.pair_zero_free_of_normFiber_exp_power_bound_only line 658
  39. theorem OAI.ShortDraftHeckeBridge.pair_zero_free_of_normFiber_exp_power_bound_principal_left line 676
  40. theorem OAI.ShortDraftHeckeBridge.pair_zero_free_of_normFiber_exp_power_bound_principal_right line 696