OAI/Analysis/CoulombRadii/FieldAnalysis/BlockIndex.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.blockIndex line 61
  2. def OAI.Coulomb.joinConfiguration line 66
  3. lemma OAI.Coulomb.joinConfiguration_measurePreserving line 71
  4. lemma OAI.Coulomb.joinConfiguration_left line 80
  5. lemma OAI.Coulomb.joinConfiguration_right line 86
  6. lemma OAI.Coulomb.joinConfiguration_right_single line 92
  7. lemma OAI.Coulomb.joinConfiguration_left_single line 109
  8. lemma OAI.Coulomb.joinConfiguration_symm_measurePreserving line 126
  9. def OAI.Coulomb.tensorValue line 131
  10. def OAI.Coulomb.tensorGradient line 136
  11. lemma OAI.Coulomb.tensorValue_memLp line 144
  12. lemma OAI.Coulomb.tensorGradient_memLp line 149
  13. lemma OAI.Coulomb.tensorValue_join line 167
  14. lemma OAI.Coulomb.tensorGradient_join_left line 173
  15. lemma OAI.Coulomb.tensorGradient_join_right line 179
  16. lemma OAI.Coulomb.tensor_weak_partial line 185
  17. def OAI.Coulomb.H1Vector.tensor line 232