OAI/Analysis/CoulombRadii/Variational/ConfigurationSplit.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.configurationSplit line 12
  2. theorem OAI.NeutralAtom.configurationSplit_apply line 15
  3. theorem OAI.NeutralAtom.configurationSplit_preserving line 18
  4. def OAI.NeutralAtom.configurationPerm line 25
  5. theorem OAI.NeutralAtom.configurationPerm_apply line 28
  6. theorem OAI.NeutralAtom.configurationPerm_preserving line 31
  7. theorem OAI.NeutralAtom.configurationPerm_direction line 36
  8. theorem OAI.NeutralAtom.configurationPerm_symm_direction line 45
  9. def OAI.NeutralAtom.permuteWavefunction line 50
  10. def OAI.NeutralAtom.permuteGradient line 53
  11. theorem OAI.NeutralAtom.HasWeakGradient.permute line 56
  12. theorem OAI.NeutralAtom.half_ordered_sum line 69
  13. theorem OAI.NeutralAtom.coulombPotential_permute line 90
  14. theorem OAI.NeutralAtom.configurationSplit_direction_zero line 108
  15. theorem OAI.NeutralAtom.configurationSplit_direction_succ line 112
  16. def OAI.NeutralAtom.insertWavefunction line 116
  17. def OAI.NeutralAtom.insertGradient line 119
  18. theorem OAI.NeutralAtom.HasWeakGradient.insert line 126
  19. theorem OAI.NeutralAtom.insertWavefunction_memLp line 161
  20. theorem OAI.NeutralAtom.insertGradient_memLp line 179
  21. theorem OAI.NeutralAtom.integral_tensor_norm line 211
  22. theorem OAI.NeutralAtom.normSquared_insert line 224
  23. def OAI.NeutralAtom.FormRegular line 236
  24. theorem OAI.NeutralAtom.formDomain_iff line 244
  25. theorem OAI.NeutralAtom.FormRegular.pair line 247
  26. theorem OAI.NeutralAtom.FormRegular.permute line 255
  27. theorem OAI.NeutralAtom.WeakDirectionalDerivative.finite_sum line 274
  28. theorem OAI.NeutralAtom.integrable_weighted_norm_sum line 298
  29. def OAI.NeutralAtom.sumWavefunction line 318
  30. def OAI.NeutralAtom.sumGradient line 321
  31. theorem OAI.NeutralAtom.FormRegular.finite_sum line 324
  32. def OAI.NeutralAtom.permutationSign line 346
  33. theorem OAI.NeutralAtom.permutationSign_mul line 348
  34. theorem OAI.NeutralAtom.permutationSign_sq line 352
  35. def OAI.NeutralAtom.antisymmetrize line 356
  36. def OAI.NeutralAtom.antisymmetrizeGradient line 359
  37. theorem OAI.NeutralAtom.antisymmetrize_antisymmetric line 362
  38. theorem OAI.NeutralAtom.FormRegular.antisymmetrize line 389
  39. theorem OAI.NeutralAtom.configurationTail_quasiPreserving line 393
  40. theorem OAI.NeutralAtom.permutationSign_decompose line 398
  41. theorem OAI.NeutralAtom.insert_permute_decompose line 407