OAI/NumberTheory/DirichletL/QuadraticSieve/InitialBound.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadraticInitialBound.quadraticRow line 77
  2. theorem OAI.QuadraticInitialBound.quadraticRow_eq_canonical line 81
  3. theorem OAI.QuadraticInitialBound.quadraticRow_star line 90
  4. theorem OAI.QuadraticInitialBound.quadraticRow_disjoint_union line 101
  5. theorem OAI.QuadraticInitialBound.quadraticRow_pair_kernel line 107
  6. theorem OAI.QuadraticInitialBound.quadratic_gram_offdiagonal line 131
  7. def OAI.QuadraticInitialBound.supportNorm line 145
  8. theorem OAI.QuadraticInitialBound.supportNorm_nonneg line 148
  9. theorem OAI.QuadraticInitialBound.two_pow_card_le_supportNorm line 151
  10. theorem OAI.QuadraticInitialBound.divisor_conductor_bound line 168
  11. theorem OAI.QuadraticInitialBound.quadratic_gram_offdiagonal_of_norm_le line 187
  12. def OAI.QuadraticInitialBound.diagonalControl line 200
  13. theorem OAI.QuadraticInitialBound.diagonalControl_nonneg line 204
  14. theorem OAI.QuadraticInitialBound.radial_weight_lattice_bound line 208
  15. theorem OAI.QuadraticInitialBound.quadraticRow_norm_le_one line 242
  16. theorem OAI.QuadraticInitialBound.quadratic_pair_summable line 249
  17. theorem OAI.QuadraticInitialBound.quadratic_gram_diagonal line 266
  18. theorem OAI.QuadraticInitialBound.norm_sq_finite_sum line 285
  19. theorem OAI.QuadraticInitialBound.quadratic_mean_summable line 297
  20. theorem OAI.QuadraticInitialBound.quadratic_mean_expand line 315
  21. theorem OAI.QuadraticInitialBound.quadratic_initial_mean_bound line 348
  22. def OAI.QuadraticInitialBound.sieveBump line 406
  23. def OAI.QuadraticInitialBound.sieveCutoff line 412
  24. theorem OAI.QuadraticInitialBound.sieveCutoff_apply line 419
  25. theorem OAI.QuadraticInitialBound.sieveBump_eq_one line 421
  26. theorem OAI.QuadraticInitialBound.quadratic_initial_finite_bound line 426
  27. def OAI.QuadraticInitialBound.initialSieveConstant line 464
  28. theorem OAI.QuadraticInitialBound.initialSieveConstant_pos line 467
  29. theorem OAI.QuadraticInitialBound.ideal_initial_quadratic_sieve line 473
  30. def OAI.CubicReflectionKernel.gammaMultiplier line 527
  31. theorem OAI.CubicReflectionKernel.gammaMultiplier_neg line 531
  32. theorem OAI.CubicReflectionKernel.Gamma_vertical_ne_zero line 534
  33. theorem OAI.CubicReflectionKernel.Gamma_vertical_conj line 539
  34. theorem OAI.CubicReflectionKernel.gammaMultiplier_norm_imaginary line 547
  35. theorem OAI.CubicReflectionKernel.Gamma_vertical_continuous line 557
  36. def OAI.CubicReflectionKernel.axisMultiplier line 571
  37. theorem OAI.CubicReflectionKernel.axisMultiplier_norm line 573
  38. theorem OAI.CubicReflectionKernel.axisMultiplier_continuous line 576
  39. def OAI.CubicReflectionKernel.spectralProfile line 596
  40. theorem OAI.CubicReflectionKernel.spectralProfile_norm line 598
  41. theorem OAI.CubicReflectionKernel.spectralProfile_continuous line 602
  42. theorem OAI.CubicReflectionKernel.spectralProfile_moment_integrable line 605
  43. theorem OAI.CubicReflectionKernel.spectralProfile_pow_integrable line 609
  44. def OAI.CubicReflectionKernel.reflectedLogProfile line 616
  45. theorem OAI.CubicReflectionKernel.reflectedLogProfile_smooth line 618
  46. theorem OAI.CubicReflectionKernel.reflectedLogProfile_deriv line 622