OAI/NumberTheory/DirichletL/QuadraticSieve/MainTermDifference.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuadraticMainTermDifference.O line 74
  2. theorem OAI.QuadraticMainTermDifference.sum_powerset_disjoint_union line 77
  3. def OAI.QuadraticMainTermDifference.normCutoff line 92
  4. def OAI.QuadraticMainTermDifference.partialSquarefreeSum line 95
  5. def OAI.QuadraticMainTermDifference.divisorSum line 101
  6. theorem OAI.QuadraticMainTermDifference.actual_main_terms_difference line 108
  7. def OAI.CubicReflectionKernel.realBeta line 159
  8. theorem OAI.CubicReflectionKernel.realBeta_nonneg line 162
  9. theorem OAI.CubicReflectionKernel.betaIntegral_ofReal line 167
  10. theorem OAI.CubicReflectionKernel.norm_betaIntegral_le line 178
  11. theorem OAI.CubicReflectionKernel.realBeta_eq_Gamma line 189
  12. theorem OAI.CubicReflectionKernel.Gamma_ratio_eq_beta line 197
  13. theorem OAI.CubicReflectionKernel.Gamma_vertical_ratio_bound line 204
  14. theorem OAI.CubicReflectionKernel.inverse_Gamma_shift line 218
  15. theorem OAI.CubicReflectionKernel.Gamma_shifted_pair_bound line 229
  16. theorem OAI.CubicReflectionKernel.gammaMultiplier_left_bound line 246
  17. theorem OAI.CubicReflectionKernel.norm_Gamma_shift_factor line 268
  18. theorem OAI.CubicReflectionKernel.Gamma_pair_strip_bound line 287
  19. theorem OAI.CubicReflectionKernel.gammaMultiplier_strip_bound line 358
  20. theorem OAI.CubicReflectionKernel.section_deriv_smooth line 382
  21. theorem OAI.CubicReflectionKernel.section_iteratedDeriv_smooth line 391
  22. theorem OAI.CubicReflectionKernel.tsupport_iteratedDeriv_subset line 400
  23. theorem OAI.CubicReflectionKernel.compact_family_deriv_integrable line 408
  24. theorem OAI.CubicReflectionKernel.compact_family_deriv_L1_bound line 419
  25. theorem OAI.CubicReflectionKernel.compact_family_fourier_power_bound line 447
  26. theorem OAI.CubicReflectionKernel.compact_family_fourier_weighted_bound line 477
  27. def OAI.CubicReflectionKernel.mellinLogFamily line 502
  28. theorem OAI.CubicReflectionKernel.mellinLogFamily_smooth line 505
  29. theorem OAI.CubicReflectionKernel.mellinLogFamily_support line 511
  30. theorem OAI.CubicReflectionKernel.mellin_eq_logFamily_fourier line 524
  31. theorem OAI.CubicReflectionKernel.compact_source_mellin_strip_decay line 532
  32. def OAI.CubicReflectionKernel.mellinData line 564
  33. def OAI.CubicReflectionKernel.mellinEulerData line 566
  34. theorem OAI.CubicReflectionKernel.mellinData_strip_decay line 568
  35. theorem OAI.CubicReflectionKernel.weighted_two_to_cauchy line 597
  36. theorem OAI.CubicReflectionKernel.mellinEulerData_strip_bound line 603
  37. theorem OAI.CubicReflectionKernel.mellinEulerData_differentiableAt line 628
  38. theorem OAI.CubicReflectionKernel.mellinEulerData_vertical_integrable line 635