OAI/NumberTheory/DirichletL/Eisenstein/VariationalLaplacian.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.kernelLiftedCutoff line 81
  2. lemma OAI.CubicEisenstein.kernelLiftedCutoff_continuous line 84
  3. lemma OAI.CubicEisenstein.kernelLiftedCutoff_compact line 87
  4. lemma OAI.CubicEisenstein.kernelLiftedCutoff_bounded line 95
  5. lemma OAI.CubicEisenstein.kernelCutoffGradient_memLp line 101
  6. def OAI.CubicEisenstein.kernelCutoffGradient line 111
  7. lemma OAI.CubicEisenstein.kernelCutoffGradient_coe line 114
  8. def OAI.CubicEisenstein.kernelCutoffGradientLinear line 118
  9. lemma OAI.CubicEisenstein.kernelCutoffGradient_bound line 133
  10. def OAI.CubicEisenstein.kernelCutoffGradientCLM line 143
  11. lemma OAI.CubicEisenstein.kernelCutoffGradient_norm_sq line 146
  12. lemma OAI.CubicEisenstein.kernelCutoffGradient_core_norm_sq line 158
  13. lemma OAI.CubicEisenstein.kernelLocalizedField_reverse_energy line 166
  14. lemma OAI.CubicEisenstein.kernelLocalizedDensity_nonneg line 202
  15. lemma OAI.CubicEisenstein.hyperbolicVolume_le_densityBound line 207
  16. instance OAI.CubicEisenstein.hyperbolicVolume_finiteOnCompacts line 218
  17. lemma OAI.CubicEisenstein.integrable_sq_mul_of_compact line 248
  18. lemma OAI.CubicEisenstein.kernelLiftedCutoffEnergy_integrable line 255
  19. lemma OAI.CubicEisenstein.kernelLiftedCutoffEnergy_integral line 261
  20. lemma OAI.CubicEisenstein.kernelCutoffGradient_core_estimate line 270
  21. lemma OAI.CubicEisenstein.kernelCutoffGradient_core_bounded line 342
  22. lemma OAI.CubicEisenstein.kernelEnergyCutoffGradient_eq_zero line 378
  23. lemma OAI.CubicEisenstein.kernelCutoffGradient_faithful line 391
  24. theorem OAI.CubicEisenstein.kernelEnergyMass_eq_zero line 428
  25. theorem OAI.CubicEisenstein.kernelEnergyMass_injective line 436
  26. lemma OAI.CubicEisenstein.kernelInitialGradient_closure_unique line 442
  27. theorem OAI.CubicEisenstein.kernelInitialGradient_isClosable line 464
  28. def OAI.CubicEisenstein.kernelWeakGradient line 468
  29. theorem OAI.CubicEisenstein.kernelWeakGradient_closed line 470
  30. theorem OAI.CubicEisenstein.kernelWeakGradient_dense_domain line 473
  31. lemma OAI.CubicEisenstein.kernelEnergyGraph_inner line 482
  32. lemma OAI.CubicEisenstein.kernelEnergyMass_norm_le line 486
  33. lemma OAI.CubicEisenstein.kernelEnergyMass_opNorm_le line 490
  34. def OAI.CubicEisenstein.kernelVariationalSolution line 493
  35. lemma OAI.CubicEisenstein.kernelVariationalSolution_equation line 496
  36. lemma OAI.CubicEisenstein.kernelVariationalSolution_unique line 503
  37. theorem OAI.CubicEisenstein.kernelVariationalSolution_existsUnique line 513
  38. lemma OAI.CubicEisenstein.kernelVariationalSolution_norm_le line 520
  39. def OAI.CubicEisenstein.kernelVariationalResolvent line 530
  40. lemma OAI.CubicEisenstein.kernelVariationalResolvent_norm_le line 533
  41. lemma OAI.CubicEisenstein.selfAdjoint_comp_adjoint line 537
  42. lemma OAI.CubicEisenstein.kernelVariationalResolvent_selfAdjoint line 544
  43. lemma OAI.CubicEisenstein.kernelVariationalResolvent_positive line 547
  44. lemma OAI.CubicEisenstein.kernelVariationalResolvent_injective line 553
  45. lemma OAI.CubicEisenstein.kernelVariationalResolvent_dense line 570
  46. def OAI.CubicEisenstein.kernelLaplacianEquation line 583
  47. def OAI.CubicEisenstein.kernelLaplacianGraph line 588
  48. lemma OAI.CubicEisenstein.mem_kernelLaplacianGraph line 591
  49. lemma OAI.CubicEisenstein.kernelLaplacianGraph_unique line 596
  50. def OAI.CubicEisenstein.kernelEnergyLaplacian line 604
  51. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_graph line 607
  52. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_closed line 610
  53. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_resolvent_graph line 614
  54. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_resolvent_domain line 620
  55. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_resolvent_apply line 624
  56. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_dense_domain line 630
  57. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_resolvent_relation line 636
  58. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_isFormalAdjoint line 642
  59. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_form line 652
  60. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_nonnegative line 662
  61. theorem OAI.CubicEisenstein.kernelEnergyLaplacian_selfAdjoint line 672