OAI/NumberTheory/DirichletL/Eisenstein/CompactEnergyFamilies.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.compact_of_norm_le_compact line 84
  2. lemma OAI.CubicEisenstein.compact_finite_pi line 106
  3. def OAI.CubicEisenstein.kernelChartCore line 121
  4. def OAI.CubicEisenstein.kernelChartCoreImage line 124
  5. lemma OAI.CubicEisenstein.kernelChartCore_open line 127
  6. lemma OAI.CubicEisenstein.kernelChartCore_subset line 130
  7. lemma OAI.CubicEisenstein.kernelChartCoreImage_open line 137
  8. abbrev OAI.CubicEisenstein.KernelGoodCutoff line 148
  9. lemma OAI.CubicEisenstein.kernelChartCoreImage_cover line 151
  10. lemma OAI.CubicEisenstein.kernelCompact_finite_chart_cover line 164
  11. lemma OAI.CubicEisenstein.kernelChartCore_mass_estimate line 170
  12. lemma OAI.CubicEisenstein.kernelChartCore_mass_bound line 217
  13. def OAI.CubicEisenstein.kernelMassRestriction line 234
  14. lemma OAI.CubicEisenstein.kernelMassRestriction_coe line 238
  15. def OAI.CubicEisenstein.kernelMassRestrictionLinear line 243
  16. lemma OAI.CubicEisenstein.kernelMassRestriction_norm_le line 265
  17. def OAI.CubicEisenstein.kernelMassRestrictionCLM line 274
  18. lemma OAI.CubicEisenstein.kernelMassRestriction_norm_sq line 281
  19. lemma OAI.CubicEisenstein.kernelMassRestriction_smooth_norm_sq line 299
  20. def OAI.CubicEisenstein.kernelEnergyMassRestriction line 309
  21. lemma OAI.CubicEisenstein.integral_le_finite_cover line 313
  22. def OAI.CubicEisenstein.kernelEnergyChartFamily line 339
  23. lemma OAI.CubicEisenstein.kernelEnergyChartFamily_isCompact line 343
  24. lemma OAI.CubicEisenstein.finite_sum_weighted_norm_sq_le line 347
  25. lemma OAI.CubicEisenstein.kernelEnergyChartFamily_core_apply line 356
  26. lemma OAI.CubicEisenstein.kernelCompact_mass_bound line 363
  27. theorem OAI.CubicEisenstein.kernelEnergyMassRestriction_isCompact line 385
  28. lemma OAI.CubicEisenstein.kernelVariationalResolvent_compact_restriction line 410
  29. def OAI.CanonicalRowCompletion.primeValueHom line 424
  30. theorem OAI.CanonicalRowCompletion.primeValueHom_prime line 438
  31. theorem OAI.CanonicalRowCompletion.primeValueHom_norm_le_one line 445
  32. def OAI.CanonicalRowCompletion.principalIdealHom line 460
  33. def OAI.CanonicalRowCompletion.localRowValue line 466
  34. theorem OAI.CanonicalRowCompletion.localRowValue_good line 472
  35. theorem OAI.CanonicalRowCompletion.localRowValue_norm line 476
  36. def OAI.CanonicalRowCompletion.idealRowHom line 484
  37. def OAI.CanonicalRowCompletion.rowTwist line 486
  38. theorem OAI.CanonicalRowCompletion.idealRowHom_prime line 489
  39. theorem OAI.CanonicalRowCompletion.idealRowHom_norm line 494
  40. theorem OAI.CanonicalRowCompletion.rowTwist_norm line 497
  41. theorem OAI.CanonicalRowCompletion.idealRowHom_product line 503
  42. theorem OAI.CanonicalRowCompletion.rowTwist_product line 514
  43. theorem OAI.CanonicalRowCompletion.squarefreeGaussCoefficient_finset line 538
  44. theorem OAI.CanonicalRowCompletion.columnWeight_finset line 547
  45. theorem OAI.CanonicalRowCompletion.selected_column_sum line 563