OAI/Analysis/CoulombRadii/FormDomain/AppendJensen.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.H1Vector.appendCut line 13
  2. theorem OAI.Coulomb.appendCut_positive_jensen line 20
  3. lemma OAI.Coulomb.mass_appendCut line 38
  4. lemma OAI.Coulomb.form_appendCut line 46
  5. lemma OAI.Coulomb.potentialForm_appendCut line 54
  6. def OAI.Coulomb.PartlyAntisymmetric line 73
  7. def OAI.Coulomb.coreIndexSet line 77
  8. lemma OAI.Coulomb.Antisymmetric.partly line 79
  9. lemma OAI.Coulomb.reindexConfiguration_measurePreserving line 82
  10. lemma OAI.Coulomb.reindex_permute line 88
  11. lemma OAI.Coulomb.PartlyAntisymmetric.reindex line 93
  12. lemma OAI.Coulomb.PartlyAntisymmetric.labelCut line 111
  13. lemma OAI.Coulomb.PartlyAntisymmetric.coreSlice line 137
  14. lemma OAI.Coulomb.appendCut_partlyAntisymmetric line 148