OAI/NumberTheory/DirichletL/Eisenstein/BesselDerivatives.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.cubicBesselDensityDeriv line 83
  2. lemma OAI.CubicEisenstein.cubicBesselDensity_hasDerivAt line 85
  3. lemma OAI.CubicEisenstein.cubic_exp_damping line 95
  4. lemma OAI.CubicEisenstein.cubicBesselDensityDeriv_bound line 101
  5. lemma OAI.CubicEisenstein.cubicBesselDerivativeMajorant_integrable line 138
  6. lemma OAI.CubicEisenstein.cubicBesselDensityDeriv_integrable line 149
  7. lemma OAI.CubicEisenstein.cubicBesselIntegral_hasDerivAt line 157
  8. def OAI.CubicEisenstein.cubicBesselRealDeriv line 191
  9. def OAI.CubicEisenstein.schlafliBesselK_cubic_derivative line 195
  10. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_hasDerivAt line 197
  11. lemma OAI.CubicEisenstein.cubicBesselDerivativeMajorant_integral line 213
  12. lemma OAI.CubicEisenstein.cubicBesselIntegral_norm_bound line 220
  13. lemma OAI.CubicEisenstein.cubicBesselIntegralDeriv_norm_bound line 230
  14. def OAI.CubicEisenstein.cubicBesselDerivativeUpper line 242
  15. lemma OAI.CubicEisenstein.cubicBesselDerivativeUpper_nonneg line 247
  16. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_derivative_bound line 252
  17. lemma OAI.CubicEisenstein.primeCubicGauss_add_three line 288
  18. lemma OAI.CubicEisenstein.cubicUnitGaussSum_prime_cube_shift_pos line 293
  19. lemma OAI.CubicEisenstein.cubicUnitGaussSum_prime_cube_shift line 316
  20. def OAI.CubicEisenstein.primeExpansionTerm line 333
  21. lemma OAI.CubicEisenstein.primeExpansionTerm_cube_shift line 337
  22. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_cube_step line 357
  23. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_cube_recurrence line 398
  24. theorem OAI.CubicEisenstein.unramifiedGaussResidue_of_initial_relation line 422
  25. lemma OAI.CubicEisenstein.gaussPrimeWeight_analytic line 489
  26. lemma OAI.CubicEisenstein.gaussPrimeWeight_center line 496
  27. theorem OAI.CubicEisenstein.unramifiedGaussResidue_prime_recurrence line 505
  28. theorem OAI.CubicEisenstein.unramifiedGaussResidue_cube_recurrence line 534
  29. lemma OAI.CubicEisenstein.recurrence_roots_closed line 553
  30. theorem OAI.CubicEisenstein.unramifiedGaussResidue_cube_closed line 570
  31. def OAI.CubicEisenstein.inverseCuspPath line 591
  32. lemma OAI.CubicEisenstein.inverseCuspPath_zero line 595
  33. theorem OAI.CubicEisenstein.inverseCuspPath_hasDerivAt line 603
  34. theorem OAI.CubicEisenstein.inverseCuspPath_comp_hasDerivAt line 630