OAI/NumberTheory/DirichletL/Eisenstein/CoordinateLaplacian.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.kernelCoordinateLaplacian line 83
  2. lemma OAI.CubicEisenstein.kernelCoreLift_laplacian line 89
  3. lemma OAI.CubicEisenstein.kernelDirichletForm_coordinate_equation_chart line 106
  4. lemma OAI.CubicEisenstein.kernelDirichletForm_sum_right line 152
  5. theorem OAI.CubicEisenstein.kernelDirichletForm_coordinate_equation line 162
  6. lemma OAI.CubicEisenstein.kernelL2_inner_toLp_smooth line 191
  7. lemma OAI.CubicEisenstein.kernelCoordinateLaplacian_form line 205
  8. theorem OAI.CubicEisenstein.kernelEnergyLaplacian_graph_of_coordinate line 220
  9. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_domain_of_coordinate line 234
  10. lemma OAI.CubicEisenstein.kernelEnergyLaplacian_apply_of_coordinate line 240
  11. theorem OAI.SecondPassIntegration.densityChildEnergy_from_canonical_state line 263
  12. def OAI.SecondPassArithmetic.globalCanonicalLabels line 303
  13. theorem OAI.SecondPassArithmetic.globalCanonicalLabels_bounds line 308
  14. theorem OAI.SecondPassArithmetic.actualSecondLabel_coprime line 329
  15. theorem OAI.SecondPassArithmetic.globalNewLabel_coprime line 340
  16. theorem OAI.SecondPassArithmetic.globalCanonicalLabels_coprime line 346
  17. theorem OAI.CanonicalRowCompletion.finite_integral_energy_polynomial line 367
  18. theorem OAI.CanonicalRowCompletion.norm_add_sum_sq_le line 404
  19. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_binned_energy line 416
  20. def OAI.CanonicalCoefficientClass.IsBaseRayTwist line 448
  21. def OAI.CanonicalCoefficientClass.baseRayOrbit line 451
  22. lemma OAI.CanonicalCoefficientClass.mem_baseRayOrbit line 454
  23. lemma OAI.CanonicalCoefficientClass.baseRayOrbit_card line 464
  24. lemma OAI.CanonicalCoefficientClass.rayMonoid_mul line 473
  25. lemma OAI.CanonicalCoefficientClass.conjugateRayMonoid_eq line 477
  26. lemma OAI.CanonicalCoefficientClass.IsBaseRayTwist.mul_ray line 481
  27. lemma OAI.CanonicalCoefficientClass.firstCoreTwist_single_ray line 487
  28. lemma OAI.CanonicalCoefficientClass.IsBaseRayTwist.firstCore line 498
  29. lemma OAI.CanonicalCoefficientClass.secondRayMinus_single_ray line 504
  30. lemma OAI.CanonicalCoefficientClass.secondRayPlus_single_ray line 509
  31. lemma OAI.CanonicalCoefficientClass.IsBaseRayTwist.secondMinus line 514
  32. lemma OAI.CanonicalCoefficientClass.IsBaseRayTwist.secondPlus line 519
  33. lemma OAI.CanonicalCoefficientClass.IsBaseRayTwist.norm_le line 524
  34. def OAI.CanonicalCoefficientClass.FactorsModulo line 532
  35. lemma OAI.CanonicalCoefficientClass.IsBaseRayTwist.factorsModulo line 535
  36. def OAI.CanonicalCoefficientClass.initialBase line 548
  37. lemma OAI.CanonicalCoefficientClass.initialBase_norm line 551
  38. lemma OAI.CanonicalCoefficientClass.initial_minus_member line 557
  39. lemma OAI.CanonicalCoefficientClass.initial_plus_member line 561
  40. lemma OAI.CanonicalCoefficientClass.norm_eval_mod line 571
  41. theorem OAI.CanonicalCoefficientClass.normCharacter_factorsModulo line 583
  42. theorem OAI.CanonicalCoefficientClass.initialBase_factorsModulo line 605
  43. def OAI.CanonicalCoefficientClass.fixedBaseConductor line 611
  44. theorem OAI.CanonicalCoefficientClass.initialOrbit_factorsModulo line 613
  45. lemma OAI.CanonicalCoefficientClass.fixedBaseConductor_principal line 617
  46. lemma OAI.CanonicalCoefficientClass.fixedBaseConductor_ne_zero line 624
  47. lemma OAI.CanonicalCoefficientClass.fixedBaseConductor_norm line 630