OAI/NumberTheory/DirichletL/Eisenstein/BarrierPotential.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.axisLaplacian_const_add line 83
  2. lemma OAI.CubicEisenstein.fullCuspProfileField_summable line 88
  3. lemma OAI.CubicEisenstein.fullCuspProfileField_add line 94
  4. lemma OAI.CubicEisenstein.cuspBarrierProfile_laplacian_zero line 100
  5. def OAI.CubicEisenstein.cuspBarrierField line 106
  6. def OAI.CubicEisenstein.cuspBarrierDefectField line 109
  7. lemma OAI.CubicEisenstein.cuspBarrierField_eq line 112
  8. lemma OAI.CubicEisenstein.cuspBarrierDefectField_eq line 116
  9. lemma OAI.CubicEisenstein.cuspBarrierField_laplace_defect line 120
  10. def OAI.CubicEisenstein.kernelBarrierPotential line 139
  11. lemma OAI.CubicEisenstein.kernelBarrierPotential_lower line 142
  12. lemma OAI.CubicEisenstein.cuspBarrier_euclidean_eq line 169
  13. lemma OAI.CubicEisenstein.cuspBarrierDefect_euclidean_eq line 175
  14. lemma OAI.CubicEisenstein.kernelQuotientBarrier_laplace_defect line 181
  15. lemma OAI.CubicEisenstein.kernelBarrierPotential_continuous line 210
  16. lemma OAI.CubicEisenstein.kernelBarrierPotential_equation line 218
  17. lemma OAI.CubicEisenstein.kernelSmoothTest_weighted_mass_integrable line 231
  18. lemma OAI.CubicEisenstein.kernelBarrierPotential_weighted_integrable line 243
  19. theorem OAI.CubicEisenstein.ground_state_square_completion line 253
  20. theorem OAI.CubicEisenstein.ground_state_directional_inequality line 262
  21. theorem OAI.SecondPassArithmetic.globalFirstQuantitativeBudget_below_rank line 280
  22. theorem OAI.SecondPassArithmetic.reopenedCanonicalFirstErrors line 356
  23. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_two_heights line 424
  24. theorem OAI.SecondPassArithmetic.reopenedCanonicalEnergy_two_heights line 437
  25. theorem OAI.SecondPassArithmetic.CanonicalStateCondition.row_bound line 462
  26. theorem OAI.SecondPassArithmetic.canonicalFirstZero_normalization line 475
  27. theorem OAI.SecondPassArithmetic.canonicalFirstTail_numerator line 496
  28. theorem OAI.SecondPassArithmetic.canonicalCutoff_ratio line 523
  29. theorem OAI.SecondPassArithmetic.canonicalFirstTail_polynomial line 528
  30. theorem OAI.SecondPassArithmetic.CanonicalStateCondition.terminal_energy line 559