OAI/NumberTheory/DirichletL/QuadraticSieve/CuspCoercivity.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.unrestrictedPrincipalDensity_twisted_squarefree line 77
  2. theorem OAI.CanonicalQuadraticSieve.densityPairSum_weighted_sum line 97
  3. theorem OAI.CanonicalQuadraticSieve.summed_dual_density line 116
  4. theorem OAI.CanonicalQuadraticSieve.actual_source_dual_density_cancellation line 137
  5. lemma OAI.CubicEisenstein.cusp_hardy_square_identity line 166
  6. lemma OAI.CubicEisenstein.cusp_hardy_boundary_hasDerivAt line 175
  7. theorem OAI.CubicEisenstein.cusp_hardy_interval_identity line 184
  8. theorem OAI.CubicEisenstein.cusp_hardy_interval line 220
  9. theorem OAI.CubicEisenstein.cusp_hardy_halfline line 234
  10. theorem OAI.CubicEisenstein.cusp_hardy_interval_lintegral line 247
  11. theorem OAI.CubicEisenstein.cusp_hardy_halfline_lintegral line 273
  12. abbrev OAI.CubicEisenstein.CuspChartCoordinates line 309
  13. def OAI.CubicEisenstein.cuspBaseArea line 311
  14. instance OAI.CubicEisenstein.cuspBaseArea_sFinite line 312
  15. def OAI.CubicEisenstein.cuspChartVolume line 314
  16. abbrev OAI.CubicEisenstein.CuspChartL2 line 318
  17. example OAI.CubicEisenstein.(example at line 320) line 320
  18. example OAI.CubicEisenstein.(example at line 321) line 321
  19. def OAI.CubicEisenstein.cuspVerticalDerivative line 323
  20. def OAI.CubicEisenstein.cuspVerticalVelocity line 326
  21. lemma OAI.CubicEisenstein.cusp_weight_mass_identity line 329
  22. lemma OAI.CubicEisenstein.cusp_weight_velocity_identity line 336
  23. theorem OAI.CubicEisenstein.cusp_chart_vertical_coercivity line 344
  24. theorem OAI.CubicEisenstein.cusp_chart_normalized_vertical_coercivity line 376
  25. theorem OAI.CubicEisenstein.cusp_chart_memLp_of_vertical line 386
  26. def OAI.CubicEisenstein.cuspCoordinateVelocity line 403
  27. def OAI.CubicEisenstein.cuspDirichletEnergy line 409
  28. lemma OAI.CubicEisenstein.cusp_vertical_energy_le line 412
  29. theorem OAI.CubicEisenstein.cusp_chart_dirichlet_coercivity line 420
  30. theorem OAI.CubicEisenstein.cusp_chart_memLp_of_energy line 427
  31. lemma OAI.CubicEisenstein.cusp_height_volume line 443
  32. theorem OAI.CubicEisenstein.cuspChartVolume_univ line 461
  33. lemma OAI.CubicEisenstein.cuspChartVolume_finite line 473
  34. def OAI.CubicEisenstein.cuspCoordinateVector line 481
  35. lemma OAI.CubicEisenstein.cuspCoordinateVelocity_eq_fderiv line 483
  36. lemma OAI.CubicEisenstein.cuspCoordinateVelocity_continuous_compact line 497
  37. lemma OAI.CubicEisenstein.cusp_compact_smooth_memLp line 508
  38. theorem OAI.CubicEisenstein.cuspChartL2_dense_smooth_energy line 517
  39. theorem OAI.CanonicalQuadraticSieve.commonMaskIdeal_primeSupport line 534
  40. theorem OAI.CanonicalQuadraticSieve.commonMask_subset_sum_eq_divisors line 544
  41. theorem OAI.CanonicalQuadraticSieve.primaryProduct_norm line 550
  42. def OAI.CanonicalQuadraticSieve.maskedPairIdealDualKernel line 560
  43. theorem OAI.CanonicalQuadraticSieve.originalPairIdealDualKernel_eq_divisors line 567
  44. theorem OAI.CanonicalQuadraticSieve.originalPairDualKernel_eq_divisors line 594