OAI/NumberTheory/DirichletL/Eisenstein/DirichletForm.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.kernelTestPartial line 78
  2. lemma OAI.CubicEisenstein.kernelTestPartial_add line 81
  3. lemma OAI.CubicEisenstein.kernelTestPartial_sub line 89
  4. lemma OAI.CubicEisenstein.kernelTestPartial_smul line 97
  5. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_eq_partials line 104
  6. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_smul line 120
  7. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_parallelogram line 125
  8. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_smul line 133
  9. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_parallelogram line 138
  10. lemma OAI.CubicEisenstein.kernelDirichletEnergy_smul line 144
  11. lemma OAI.CubicEisenstein.kernelDirichletEnergy_parallelogram line 150
  12. def OAI.CubicEisenstein.kernelGradientAt line 161
  13. lemma OAI.CubicEisenstein.kernelGradientAt_norm_sq line 172
  14. def OAI.CubicEisenstein.kernelDirichletPairDensity line 179
  15. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_coordinate line 184
  16. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_integrable line 191
  17. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_add_right line 198
  18. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_smul_right line 204
  19. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_conj line 210
  20. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_self line 219
  21. def OAI.CubicEisenstein.kernelDirichletForm line 227
  22. lemma OAI.CubicEisenstein.kernelDirichletForm_add_right line 230
  23. lemma OAI.CubicEisenstein.kernelDirichletForm_smul_right line 236
  24. lemma OAI.CubicEisenstein.kernelDirichletForm_conj line 242
  25. lemma OAI.CubicEisenstein.kernelDirichletForm_self line 250
  26. lemma OAI.CubicEisenstein.kernelDirichletForm_self_nonneg line 256
  27. theorem OAI.CompletedGauss.finite_integral_energy_bound line 269
  28. theorem OAI.CompletedGauss.integrated_product_quadratic line 297
  29. def OAI.CompletedGauss.completedRowFiber line 343
  30. theorem OAI.CompletedGauss.rowResidualPart_injective_on_fiber line 346
  31. theorem OAI.CompletedGauss.completedRowFiber_residual_range line 357
  32. theorem OAI.CompletedGauss.completedRowFiber_energy_le line 368
  33. theorem OAI.CompletedGauss.completed_kernel_three_window line 390
  34. theorem OAI.CompletedGauss.completed_smooth_quadratic line 416
  35. def OAI.InitialMeanSquare.initialLogProfile line 518
  36. lemma OAI.InitialMeanSquare.initialLogProfile_apply line 528
  37. theorem OAI.InitialMeanSquare.initialLogProfile_support line 533
  38. theorem OAI.InitialMeanSquare.initialLogProfile_normalized line 551
  39. lemma OAI.InitialMeanSquare.mobiusRow_mul line 577
  40. theorem OAI.InitialMeanSquare.mobiusRow_initial_normalization line 587
  41. theorem OAI.InitialMeanSquare.mobiusRow_initial_energy line 601