OAI/Analysis/CoulombRadii/Variational/WedgeInsert.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.wedgeInsert line 12
  2. def OAI.NeutralAtom.wedgeInsertGradient line 16
  3. theorem OAI.NeutralAtom.antisymmetrize_insert_eq line 21
  4. theorem OAI.NeutralAtom.HasWeakGradient.unique_of_ae_eq line 48
  5. def OAI.NeutralAtom.InsertionSupport line 64
  6. theorem OAI.NeutralAtom.insertionSupport_tensor line 67
  7. theorem OAI.NeutralAtom.InsertionSupport.swap line 86
  8. theorem OAI.NeutralAtom.InsertionSupport.placements_disjoint line 104
  9. theorem OAI.NeutralAtom.norm_sq_sum_of_disjoint line 114
  10. def OAI.NeutralAtom.spinsPerm line 131
  11. theorem OAI.NeutralAtom.spinsPerm_apply line 134
  12. theorem OAI.NeutralAtom.normSquared_permute line 137
  13. theorem OAI.NeutralAtom.energy_permute line 146
  14. theorem OAI.NeutralAtom.norm_sq_sum_real_smul_of_disjoint line 168
  15. theorem OAI.NeutralAtom.FormRegular.integrable_potential line 178
  16. theorem OAI.NeutralAtom.normSquared_disjoint_sum line 189
  17. theorem OAI.NeutralAtom.energy_disjoint_sum line 200
  18. theorem OAI.NeutralAtom.insertionSupport_gradient line 236
  19. theorem OAI.NeutralAtom.wedgeInsert_antisymmetric line 246
  20. theorem OAI.NeutralAtom.FormRegular.wedgeInsert line 261
  21. theorem OAI.NeutralAtom.normSquared_wedgeInsert line 268
  22. theorem OAI.NeutralAtom.energy_wedgeInsert line 281
  23. theorem OAI.NeutralAtom.integrable_supported_weight line 296
  24. theorem OAI.NeutralAtom.integrable_weighted_tensor line 310
  25. theorem OAI.NeutralAtom.integral_weighted_tensor line 323
  26. theorem OAI.NeutralAtom.inserted_nuclear_bound line 340
  27. theorem OAI.NeutralAtom.inserted_pair_bound line 351
  28. theorem OAI.NeutralAtom.FormRegular.insert_separated line 365
  29. theorem OAI.NeutralAtom.coulombPotential_cons line 401
  30. def OAI.NeutralAtom.gradientNormSquared line 413
  31. theorem OAI.NeutralAtom.gradientNormSquared_eq line 416
  32. def OAI.NeutralAtom.potentialForm line 422
  33. theorem OAI.NeutralAtom.energy_decompose line 425