OAI/Analysis/CoulombRadii/FieldAnalysis/ConfigurationMeasurableEquiv.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Coulomb.measurePreserving_uncurry line 16
  2. def OAI.Coulomb.configurationMeasurableEquiv line 37
  3. theorem OAI.Coulomb.configurationMeasurableEquiv_apply line 43
  4. theorem OAI.Coulomb.configurationMeasurableEquiv_measurePreserving line 46
  5. theorem OAI.Coulomb.tensorOrbital_memLp line 54
  6. theorem OAI.Coulomb.tensorOrbital_inner_integral line 72
  7. abbrev OAI.Coulomb.StateHilbert line 93
  8. def OAI.Coulomb.H1Vector.toHilbert line 95
  9. def OAI.Coulomb.tensorHilbert line 98
  10. lemma OAI.Coulomb.inner_toLp_complex line 104
  11. lemma OAI.Coulomb.norm_toLp_sq_complex line 112
  12. lemma OAI.Coulomb.H1Vector.toHilbert_norm_sq line 128
  13. lemma OAI.Coulomb.tensorHilbert_inner line 133
  14. lemma OAI.Coulomb.tensorHilbert_orthonormal line 143
  15. lemma OAI.Coulomb.orbitalCoefficient_eq_inner line 166
  16. theorem OAI.Coulomb.orbitalCoefficient_summable_and_bound line 175
  17. theorem OAI.Coulomb.orbitalCoefficient_pauli line 187
  18. lemma OAI.Coulomb.memLp_fiber_ae line 203
  19. lemma OAI.Coulomb.integralInner_sq_le line 210
  20. def OAI.Coulomb.fiberContract line 217
  21. lemma OAI.Coulomb.fiberContract_memLp line 220
  22. lemma OAI.Coulomb.fiberContract_norm_sq_le line 231
  23. lemma OAI.Coulomb.tensorPair_memLp line 243
  24. lemma OAI.Coulomb.integrable_star_mul line 251
  25. lemma OAI.Coulomb.integral_tensorPair line 259
  26. def OAI.Coulomb.CompleteOrbitals line 275
  27. theorem OAI.Coulomb.completeOrbitals_tensorPair line 284
  28. theorem OAI.Coulomb.HilbertBasis_completeOrbitals line 313
  29. theorem OAI.Coulomb.CompleteOrbitals.comp line 328
  30. lemma OAI.Coulomb.scalarTensor_memLp line 341
  31. theorem OAI.Coulomb.completeOrbitals_finPi line 355
  32. theorem OAI.Coulomb.orthonormal_subtype_countable line 397