OAI/NumberTheory/DirichletL/CubicSieve/RowMajorants.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.first_passage_transfer_input_family line 81
  2. theorem OAI.SecondPassArithmetic.exists_rowMajorant line 155
  3. def OAI.SecondPassArithmetic.rowMajorant line 182
  4. lemma OAI.SecondPassArithmetic.rowMajorant_nonneg line 184
  5. lemma OAI.SecondPassArithmetic.rowMajorant_one line 187
  6. lemma OAI.SecondPassArithmetic.rowMajorant_zero line 190
  7. def OAI.SecondPassArithmetic.rowMajorantBall line 193
  8. lemma OAI.SecondPassArithmetic.rowMajorant_zero_outside line 195
  9. lemma OAI.SecondPassArithmetic.rowMajorant_tsum_eq_sum line 207
  10. lemma OAI.SecondPassArithmetic.rowMajorant_summable line 214
  11. theorem OAI.SecondPassArithmetic.finite_row_energy_le_rowMajorant line 220
  12. theorem OAI.SecondPassArithmetic.firstCoreInputRow_finite_le_second_poisson line 247
  13. theorem OAI.SecondPassArithmetic.firstCoreInputRow_majorant_integrable line 269
  14. theorem OAI.SecondPassArithmetic.firstCoreInputRow_integrated_le_majorant line 288
  15. def OAI.SecondPassArithmetic.secondPreKernelPair line 318
  16. def OAI.SecondPassArithmetic.secondChildKernelPair line 324
  17. theorem OAI.SecondPassArithmetic.secondPreKernelPair_eq_children line 332
  18. def OAI.SecondPassArithmetic.secondKernelPair line 360
  19. theorem OAI.SecondPassArithmetic.secondKernelPair_eq_pre line 366
  20. theorem OAI.SecondPassArithmetic.secondKernelPair_eq_children line 404
  21. def OAI.CubicEisenstein.denominatorCondition line 426
  22. abbrev OAI.CubicEisenstein.AdmissibleDenominator line 427
  23. abbrev OAI.CubicEisenstein.LevelLower line 428
  24. lemma OAI.CubicEisenstein.denominatorCondition_shift line 430
  25. lemma OAI.CubicEisenstein.row_symbol_shift line 442
  26. def OAI.CubicEisenstein.primitiveSigmaEquiv line 453
  27. abbrev OAI.CubicEisenstein.DenominatorResidue line 462
  28. def OAI.CubicEisenstein.denominatorRep line 463
  29. lemma OAI.CubicEisenstein.denominatorRep_spec line 465
  30. abbrev OAI.CubicEisenstein.AdmissibleResidue line 468
  31. lemma OAI.CubicEisenstein.finite_admissibleResidue line 471
  32. def OAI.CubicEisenstein.residueDenominatorMap line 475
  33. lemma OAI.CubicEisenstein.residueDenominatorMap_bijective line 478
  34. def OAI.CubicEisenstein.residueDenominatorEquiv line 514
  35. lemma OAI.CubicEisenstein.residueDenominatorEquiv_val line 518
  36. def OAI.CubicEisenstein.primitiveTerm line 521
  37. theorem OAI.CubicEisenstein.primitive_terms_summable line 525
  38. theorem OAI.CubicEisenstein.upperEisenstein_eq_by_lower line 531
  39. theorem OAI.CubicEisenstein.denominator_sum_residues line 538
  40. lemma OAI.CubicEisenstein.primitiveTerm_shift line 546
  41. lemma OAI.CubicEisenstein.denominator_zero_unique line 558
  42. lemma OAI.CubicEisenstein.zero_lower_sum line 562
  43. def OAI.CubicEisenstein.residueSeries line 572
  44. theorem OAI.CubicEisenstein.upperEisenstein_eq_residue_series line 576
  45. lemma OAI.CubicEisenstein.residueSeries_finite line 596
  46. def OAI.CubicEisenstein.periodBasis line 612
  47. lemma OAI.CubicEisenstein.periodBasis_zero line 614
  48. lemma OAI.CubicEisenstein.periodBasis_one line 616
  49. def OAI.CubicEisenstein.periodLattice line 619
  50. def OAI.CubicEisenstein.periodDomain line 620
  51. instance OAI.CubicEisenstein.(instance at line 622) line 622
  52. instance OAI.CubicEisenstein.(instance at line 623) line 623
  53. lemma OAI.CubicEisenstein.periodDomain_fundamental line 626
  54. lemma OAI.CubicEisenstein.periodDomain_measurable line 628
  55. lemma OAI.CubicEisenstein.three_embedding_mem line 631
  56. def OAI.CubicEisenstein.periodPoint line 643
  57. lemma OAI.CubicEisenstein.periodPoint_val line 644
  58. lemma OAI.CubicEisenstein.periodPoint_bijective line 645
  59. def OAI.CubicEisenstein.periodEquiv line 664
  60. theorem OAI.CubicEisenstein.integral_eq_period_integrals line 666
  61. theorem OAI.CubicEisenstein.lintegral_eq_period_lintegrals line 677
  62. lemma OAI.CubicEisenstein.periodDomain_volume line 688
  63. lemma OAI.CubicEisenstein.periodization_lintegral_norm_ne_top line 700
  64. theorem OAI.CubicEisenstein.integral_periodization line 705