OAI/NumberTheory/DirichletL/Eisenstein/SeedHeight.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.fullCuspHeight_le_barrier line 83
  2. lemma OAI.CubicEisenstein.cosetHeight_le_barrier line 94
  3. lemma OAI.CubicEisenstein.kernel_compact_seed_height_bound line 102
  4. def OAI.CubicEisenstein.kernelSeedHeightBound line 109
  5. lemma OAI.CubicEisenstein.kernelSeedHeightBound_spec line 112
  6. def OAI.CubicEisenstein.compactSeedTransition line 117
  7. def OAI.CubicEisenstein.compactSeedProfile line 121
  8. lemma OAI.CubicEisenstein.compactSeedProfile_entire line 124
  9. lemma OAI.CubicEisenstein.compactSeedProfile_apply line 128
  10. lemma OAI.CubicEisenstein.compactHeightProfile_seed line 139
  11. lemma OAI.CubicEisenstein.kernelCompactProfile_seed line 149
  12. def OAI.CubicEisenstein.kernelLocalSeedL2 line 163
  13. lemma OAI.CubicEisenstein.kernelLocalSeedL2_entire line 169
  14. lemma OAI.CubicEisenstein.kernelLocalSeedL2_ae_eq line 175
  15. def OAI.CubicEisenstein.kernelCorrectedSeed line 198
  16. def OAI.CubicEisenstein.kernelLocalCorrectedSeed line 201
  17. lemma OAI.CubicEisenstein.kernelLocalCorrectedSeed_meromorphicAt line 206
  18. lemma OAI.CubicEisenstein.kernelLocalCorrectedSeed_analyticAt_nonreal line 213
  19. lemma OAI.CubicEisenstein.kernelLocalCorrectedSeed_ae_eq line 221
  20. lemma OAI.CubicEisenstein.kernelLocalCorrectedSeed_residue_limit line 240
  21. lemma OAI.CubicEisenstein.partial_iteratedFDeriv_contDiffAt line 269
  22. lemma OAI.CubicEisenstein.compact_family_derivative_bound line 288
  23. theorem OAI.CubicEisenstein.compact_smooth_family_tsum line 314
  24. lemma OAI.CubicEisenstein.rowEnergy_real_smul line 341
  25. def OAI.CubicEisenstein.normalizedComplexRow line 346
  26. lemma OAI.CubicEisenstein.normalizedComplexRow_energy line 348
  27. lemma OAI.CubicEisenstein.rowEnergy_continuous line 353
  28. lemma OAI.CubicEisenstein.rowEnergy_unit_isCompact line 357
  29. lemma OAI.CubicEisenstein.rowEnergy_unit_ne_zero line 365
  30. def OAI.CubicEisenstein.regularSpatialHeight line 369
  31. lemma OAI.CubicEisenstein.regularSpatialHeight_pos line 372
  32. lemma OAI.CubicEisenstein.regularSpatialHeight_contDiff line 376
  33. lemma OAI.CubicEisenstein.regularSpatialHeight_eq line 381
  34. def OAI.CubicEisenstein.regularRowKernel line 386
  35. lemma OAI.CubicEisenstein.regularRowDenominator_contDiff line 390
  36. lemma OAI.CubicEisenstein.regularRowKernel_contDiffAt line 404
  37. lemma OAI.CubicEisenstein.heightDenominator_real_smul line 415
  38. lemma OAI.CubicEisenstein.heightDenominator_normalized line 424
  39. lemma OAI.CubicEisenstein.regularRowKernel_eq line 429
  40. lemma OAI.CubicEisenstein.normalized_row_summand line 437
  41. theorem OAI.CubicEisenstein.regular_eisenstein_compact_smooth line 457
  42. theorem OAI.CubicEisenstein.smoothEisenstein_contDiffAt line 474
  43. lemma OAI.CubicEisenstein.kernel_contMDiff_of_spatial line 506
  44. lemma OAI.CubicEisenstein.kernelQuotientEisenstein_coordinate line 532
  45. lemma OAI.CubicEisenstein.kernelQuotientEisenstein_contMDiff line 540
  46. lemma OAI.CubicEisenstein.kernelQuotientSeed_coordinate line 545
  47. lemma OAI.CubicEisenstein.kernelQuotientSeed_contMDiff line 553
  48. def OAI.CubicEisenstein.kernelCutoffRemainderTest line 558
  49. lemma OAI.CubicEisenstein.kernelCutoffRemainderTest_apply line 575
  50. def OAI.InitialMeanSquare.HasInitialCanonicalDensityAtRadius line 588