OAI/Analysis/CoulombRadii/FormDomain/OrbitalHilbertBasis.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Coulomb.exists_countable_spatial_basis line 14
  2. theorem OAI.Coulomb.hilbertBasis_parseval line 23
  3. def OAI.Coulomb.orbitalHilbertBasis line 31
  4. lemma OAI.Coulomb.orbitalHilbertBasis_apply line 49
  5. theorem OAI.Coulomb.completeOrbitals_parseval line 56
  6. def OAI.Coulomb.spinOrbital line 64
  7. lemma OAI.Coulomb.spinOrbital_memLp line 67
  8. lemma OAI.Coulomb.tensorSpinOrbital_apply line 74
  9. lemma OAI.Coulomb.spinOrbital_orthonormal line 90
  10. lemma OAI.Coulomb.tensorSpinHilbert_inner line 119
  11. theorem OAI.Coulomb.tensorSpinHilbert_orthogonal_eq_bot line 145
  12. def OAI.Coulomb.tensorSpinHilbertBasis line 166
  13. lemma OAI.Coulomb.tensorSpinHilbertBasis_apply line 178
  14. theorem OAI.Coulomb.orbitalCoefficient_spin_parseval line 186
  15. lemma OAI.Coulomb.fin_strictMono_nat_le line 195
  16. theorem OAI.Coulomb.levels_sum_le line 209
  17. theorem OAI.Coulomb.FermionicCoefficients.levels_lower line 227
  18. lemma OAI.Coulomb.measurePreserving_permutePi line 247
  19. lemma OAI.Coulomb.scalarTensor_inner_integral line 257
  20. lemma OAI.Coulomb.scalarTensor_orthonormal line 264
  21. def OAI.Coulomb.scalarCoefficient line 282
  22. def OAI.Coulomb.ProductAntisymmetric line 286
  23. lemma OAI.Coulomb.scalarCoefficient_antisymmetric line 290
  24. theorem OAI.Coulomb.scalarCoefficient_parseval line 309
  25. lemma OAI.Coulomb.scalarCoefficient_summable line 325
  26. theorem OAI.Coulomb.scalarCoefficient_levels_lower line 339
  27. def OAI.Coulomb.cosineMode line 362
  28. def OAI.Coulomb.evenOnSegment line 365
  29. lemma OAI.Coulomb.evenOnSegment_memLp line 368
  30. lemma OAI.Coulomb.evenOnSegment_pos line 375
  31. lemma OAI.Coulomb.evenOnSegment_eq_zero line 380
  32. lemma OAI.Coulomb.evenOnSegment_neg line 390
  33. lemma OAI.Coulomb.fourierOn_ae_zero line 394