OAI/NumberTheory/DirichletL/RowCompletion/ThetaNonvanishing.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalRowCompletion.corrected_weighted_mellin_identity line 85
  2. theorem OAI.CanonicalRowCompletion.dirichlet_open_strip_of_theta_models line 105
  3. theorem OAI.CanonicalRowCompletion.dirichlet_nonvanishing_of_theta_models line 134
  4. theorem OAI.CanonicalRowCompletion.dirichletTarget_of_theta_models line 145
  5. lemma OAI.QuadraticAllOddCRT.lambda_odd line 168
  6. lemma OAI.QuadraticAllOddCRT.lambda_residue line 171
  7. lemma OAI.QuadraticAllOddCRT.lambda_quadratic_ray_ne_zero line 179
  8. lemma OAI.QuadraticAllOddCRT.character_lambda_primary line 184
  9. def OAI.QuadraticAllOddCRT.lambdaQuadraticRay line 191
  10. theorem OAI.QuadraticAllOddCRT.character_lambda_eq_ray line 195
  11. def OAI.QuadraticAllOddCRT.lambdaQuadraticTable line 231
  12. lemma OAI.QuadraticAllOddCRT.lambdaQuadraticTable_mul line 236
  13. lemma OAI.QuadraticAllOddCRT.lambdaQuadraticTable_eq_ray line 244
  14. def OAI.QuadraticAllOddCRT.lambdaQuadraticCharacter line 268
  15. lemma OAI.QuadraticAllOddCRT.lambdaQuadraticCharacter_periodic line 282
  16. lemma OAI.CanonicalRowCompletion.localRowValue_square line 299
  17. theorem OAI.CanonicalRowCompletion.idealRowHom_square line 309
  18. lemma OAI.CanonicalRowCompletion.actualSextic_cube_quadratic line 324
  19. lemma OAI.CanonicalRowCompletion.idealRowHom_lambda_prime_cube line 337
  20. theorem OAI.CanonicalRowCompletion.idealRowHom_lambda_cube line 354
  21. theorem OAI.CanonicalRowCompletion.idealRowHom_lambda_formula line 376
  22. theorem OAI.CanonicalRowCompletion.idealRowHom_lambda_mod_thirty_six line 401
  23. lemma OAI.CubicEisenstein.cuspRemainder_absolute_chart line 421
  24. theorem OAI.CubicEisenstein.cuspRemainder_absolute_bound line 444
  25. lemma OAI.CubicEisenstein.cuspRemainder_aux_norm line 461
  26. lemma OAI.CubicEisenstein.cuspRemainder_row_scaled_deriv_aux_bound line 466
  27. def OAI.CubicEisenstein.weightedHeightProfile line 486
  28. lemma OAI.CubicEisenstein.weightedHeightProfile_axis_differentiable line 489
  29. lemma OAI.CubicEisenstein.heightPoincare_axis_termwise line 495
  30. lemma OAI.CubicEisenstein.weightedRemainder_axis_deriv line 527
  31. def OAI.CubicEisenstein.eisensteinRemainderField line 547
  32. theorem OAI.CubicEisenstein.eisensteinRemainder_axis_termwise line 550
  33. lemma OAI.CubicEisenstein.weightedRemainder_scaled_deriv_bound line 582
  34. theorem OAI.CubicEisenstein.eisensteinRemainder_scaled_axis_bound line 603
  35. def OAI.CubicEisenstein.kernelEisensteinRemainder line 629
  36. lemma OAI.CubicEisenstein.kernelEisensteinRemainder_smooth line 632
  37. lemma OAI.CubicEisenstein.kernelEisensteinRemainder_euclidean_smooth line 637
  38. lemma OAI.CubicEisenstein.kernelEisensteinRemainder_euclidean_eq line 643
  39. theorem OAI.CubicEisenstein.kernelEisensteinRemainder_scaled_fderiv_bound line 654