OAI/NumberTheory/DirichletL/Poisson/LatticeEnvelopes.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EisensteinSchwartzPoisson.nonzeroLatticeEnvelopeConstant line 79
  2. theorem OAI.EisensteinSchwartzPoisson.nonzeroLatticeEnvelopeConstant_nonneg line 82
  3. theorem OAI.EisensteinSchwartzPoisson.scaled_cauchy_nonzero_mass line 88
  4. theorem OAI.EisensteinSchwartzPoisson.nonzero_lattice_envelope_sum line 104
  5. def OAI.CanonicalQuadraticSieve.originalMiddleDecayConstant line 135
  6. def OAI.CanonicalQuadraticSieve.dualMiddleDecayConstant line 138
  7. theorem OAI.CanonicalQuadraticSieve.originalMiddleDecayConstant_nonneg line 141
  8. theorem OAI.CanonicalQuadraticSieve.dualMiddleDecayConstant_nonneg line 145
  9. theorem OAI.CanonicalQuadraticSieve.divisorBlockCost_mono_coefficients line 149
  10. def OAI.CanonicalQuadraticSieve.originalMiddleAt line 166
  11. def OAI.CanonicalQuadraticSieve.dualMiddleAt line 176
  12. theorem OAI.CanonicalQuadraticSieve.originalMiddleAt_nonneg line 188
  13. theorem OAI.CanonicalQuadraticSieve.dualMiddleAt_nonneg line 196
  14. theorem OAI.CanonicalQuadraticSieve.actual_original_middle_all_frequencies line 215
  15. theorem OAI.CanonicalQuadraticSieve.dual_middle_scale_identity line 266
  16. theorem OAI.CanonicalQuadraticSieve.actual_dual_middle_all_frequencies line 277
  17. def OAI.CanonicalQuadraticSieve.divisorExponentConstant line 346
  18. theorem OAI.CanonicalQuadraticSieve.divisorExponentConstant_pos line 349
  19. theorem OAI.CanonicalQuadraticSieve.divisor_cost_with_constant line 352
  20. theorem OAI.CanonicalQuadraticSieve.sqrt_div_mul_rpow line 365
  21. theorem OAI.CanonicalQuadraticSieve.original_middle_scale_shape line 370
  22. theorem OAI.CanonicalQuadraticSieve.dual_middle_scale_shape line 378
  23. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.original_middle_block line 408
  24. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_middle_block line 436
  25. def OAI.CubicEisenstein.integralComplexMatrix line 472
  26. lemma OAI.CubicEisenstein.integralComplexMatrix_apply line 474
  27. lemma OAI.CubicEisenstein.integralComplexMatrix_levelThree line 477
  28. lemma OAI.CubicEisenstein.row_wedge_gram line 480
  29. lemma OAI.CubicEisenstein.row_wedge_le_energy line 488
  30. lemma OAI.CubicEisenstein.bottom_row_wedge_mul line 493
  31. theorem OAI.CubicEisenstein.hyperbolicHeight_mul_bound line 501
  32. lemma OAI.CubicEisenstein.one_le_normSq_embedding line 519
  33. theorem OAI.CubicEisenstein.integral_hyperbolicHeight_mul_le_one line 524
  34. def OAI.CubicEisenstein.cuspHoroball line 532
  35. theorem OAI.CubicEisenstein.cuspHoroball_disjoint line 535
  36. def OAI.CubicEisenstein.InequivalentCusps line 548
  37. def OAI.CubicEisenstein.cuspNeighborhood line 551
  38. lemma OAI.CubicEisenstein.cuspNeighborhood_invariant line 554
  39. theorem OAI.CubicEisenstein.cuspNeighborhood_disjoint line 570
  40. lemma OAI.CubicEisenstein.cosetHeight_pos line 587
  41. lemma OAI.CubicEisenstein.cosetHeight_rightEquiv line 591
  42. lemma OAI.CubicEisenstein.high_coset_unique line 598
  43. lemma OAI.CubicEisenstein.high_cosets_finite line 617
  44. def OAI.CubicEisenstein.cuspCutoffTerm line 623
  45. lemma OAI.CubicEisenstein.cuspCutoffTerm_finiteSupport line 626
  46. lemma OAI.CubicEisenstein.cuspCutoffTerm_summable line 635
  47. def OAI.CubicEisenstein.cuspCutoffCorrection line 639
  48. lemma OAI.CubicEisenstein.cuspCutoffTerm_automorphy line 642
  49. theorem OAI.CubicEisenstein.cuspCutoffCorrection_automorphy line 654
  50. lemma OAI.CubicEisenstein.cuspCutoffCorrection_eq line 663
  51. lemma OAI.CubicEisenstein.hyperbolicHeight_upperPoint line 673
  52. def OAI.CubicEisenstein.infinityConstantMode line 678
  53. def OAI.CubicEisenstein.truncatedAtInfinity line 681
  54. theorem OAI.CubicEisenstein.truncatedAtInfinity_automorphy line 684
  55. theorem OAI.CubicEisenstein.truncatedAtInfinity_upperPoint line 692