OAI/NumberTheory/DirichletL/CubicSieve/RadialProfiles.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.positiveRadialProfile line 81
  2. theorem OAI.SecondPassArithmetic.positiveRadialProfile_support line 84
  3. theorem OAI.SecondPassArithmetic.positiveRadialProfile_compact line 99
  4. theorem OAI.SecondPassArithmetic.positiveRadialProfile_smooth line 104
  5. def OAI.SecondPassArithmetic.radialFromLog line 122
  6. theorem OAI.SecondPassArithmetic.radialFromLog_apply_pos line 126
  7. theorem OAI.SecondPassArithmetic.radialFromLog_hasCompactSupport line 132
  8. theorem OAI.SecondPassArithmetic.radialFromLog_support line 136
  9. theorem OAI.SecondPassArithmetic.radialFromLog_column line 140
  10. def OAI.CubicEisenstein.kernelTestPartitionTerm line 153
  11. lemma OAI.CubicEisenstein.kernelTestPartitionTerm_tsupport line 159
  12. lemma OAI.CubicEisenstein.kernelTestPartition_sum line 165
  13. theorem OAI.CubicEisenstein.kernelSmoothTest_finite_chart_partition line 180
  14. def OAI.CubicEisenstein.kernelFullCutoffFun line 201
  15. lemma OAI.CubicEisenstein.kernelFullCutoffFun_smooth line 204
  16. lemma OAI.CubicEisenstein.kernelFullCutoffFun_tsupport line 208
  17. lemma OAI.CubicEisenstein.kernelFullCutoffFun_compact line 219
  18. def OAI.CubicEisenstein.kernelFullCutoff line 223
  19. lemma OAI.CubicEisenstein.kernelFullCutoff_one line 229
  20. lemma OAI.CubicEisenstein.kernelFullCutoff_eventually_one line 235
  21. def OAI.CubicEisenstein.kernelCoreLift line 240
  22. lemma OAI.CubicEisenstein.kernelCoreLift_eventually_eq line 243
  23. lemma OAI.CubicEisenstein.kernelCoreLift_tsupport_outer line 250
  24. lemma OAI.CubicEisenstein.kernelCoreLift_tsupport line 254
  25. lemma OAI.CubicEisenstein.kernelCoreLift_eq_on_outer line 277
  26. def OAI.CubicEisenstein.euclideanHeightCLM line 294
  27. lemma OAI.CubicEisenstein.euclideanHeightCLM_apply line 297
  28. lemma OAI.CubicEisenstein.upperHeightDivide_smooth line 299
  29. lemma OAI.CubicEisenstein.upperHeightDivide_compact line 318
  30. def OAI.CubicEisenstein.upperHeightDivide line 324
  31. lemma OAI.CubicEisenstein.upperHeightDivide_apply line 329
  32. lemma OAI.CubicEisenstein.upperHeightDivide_tsupport line 333
  33. lemma OAI.CubicEisenstein.upperHeightDivide_lineDeriv line 342
  34. lemma OAI.CubicEisenstein.upperSchwartz_derivative_compact line 357
  35. def OAI.CubicEisenstein.upperWeightedPartial line 362
  36. def OAI.CubicEisenstein.upperWeightedDivergence line 369
  37. def OAI.CubicEisenstein.complexHermitianBilin line 374
  38. lemma OAI.CubicEisenstein.schwartz_hermitian_integrable line 377
  39. lemma OAI.CubicEisenstein.schwartz_hermitian_lineGreen line 381
  40. lemma OAI.CubicEisenstein.upperWeighted_green line 385
  41. def OAI.CubicEisenstein.upperPositiveLaplacian line 404
  42. lemma OAI.CubicEisenstein.upperWeightedDivergence_apply_ne_zero line 408
  43. lemma OAI.CubicEisenstein.upperWeightedDivergence_apply line 423
  44. theorem OAI.CubicEisenstein.upperHyperbolic_green line 444
  45. lemma OAI.CubicEisenstein.kernelEuclideanProjection_integral_complex line 460
  46. lemma OAI.CubicEisenstein.hyperbolicEuclidean_setIntegral_complex line 471
  47. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_zero_of_notMem line 486
  48. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_euclidean line 503
  49. lemma OAI.CubicEisenstein.kernelCoreLift_fderiv_eq_on_outer line 521
  50. lemma OAI.CubicEisenstein.kernelCoreLift_pair_on_outer line 540
  51. theorem OAI.CubicEisenstein.kernelDirichletForm_eq_chart_pairing line 556
  52. theorem OAI.CubicEisenstein.kernelDirichletForm_eq_chart_laplacian line 594