OAI/Analysis/CoulombIonization/Variational/Spatial.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.spatial_coordinate_derivative line 89
  2. def OAI.CoulombAtom.spatialProductValue line 105
  3. lemma OAI.CoulombAtom.spatialProduct_regular line 108
  4. lemma OAI.CoulombAtom.spatialProduct_derivative line 112
  5. lemma OAI.CoulombAtom.spatial_factor_bound line 137
  6. lemma OAI.CoulombAtom.spatial_product_sub_bound line 144
  7. def OAI.CoulombAtom.spatialProduct line 149
  8. lemma OAI.CoulombAtom.spatial_square_partition line 162
  9. theorem OAI.CoulombAtom.spatial_cut_mass line 169
  10. theorem OAI.CoulombAtom.spatial_cut_energy line 173
  11. def OAI.CoulombAtom.CoreAntisymmetric line 183
  12. lemma OAI.CoulombAtom.SobolevFermion.coreAntisymmetric line 188
  13. theorem OAI.CoulombAtom.SobolevVector.ae_coreSlice line 193
  14. theorem OAI.CoulombAtom.CoreAntisymmetric.ae_coreSlice line 217
  15. lemma OAI.CoulombAtom.CoreAntisymmetric.multiply line 237
  16. lemma OAI.CoulombAtom.spatialProduct_invariant line 248
  17. def OAI.CoulombAtom.coreCutLabels line 260
  18. lemma OAI.CoulombAtom.coreCutLabels_invariant line 263
  19. theorem OAI.CoulombAtom.spatial_coreSlice_fermion line 269
  20. theorem OAI.CoulombAtom.spatial_coreSlice_priced line 280
  21. lemma OAI.CoulombAtom.binary_product_square_sum line 288