OAI/Analysis/CoulombIonization/Variational/Slices.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAtom.smooth_test_product line 37
  2. lemma OAI.CoulombAtom.lineDeriv_test_product line 51
  3. lemma OAI.CoulombAtom.weak_slice_fixed_test line 63
  4. theorem OAI.CoulombAtom.IsWeakDerivative.slice_left line 87
  5. lemma OAI.CoulombAtom.IsWeakDerivative.pullback line 110
  6. def OAI.CoulombAtom.joinLists line 137
  7. lemma OAI.CoulombAtom.joinLists_left line 140
  8. lemma OAI.CoulombAtom.joinLists_right line 144
  9. def OAI.CoulombAtom.configurationJoin line 148
  10. lemma OAI.CoulombAtom.configurationJoin_apply line 153
  11. lemma OAI.CoulombAtom.configurationJoin_preserving line 163
  12. lemma OAI.CoulombAtom.configurationJoin_direction line 167
  13. def OAI.CoulombAtom.corePerm line 180
  14. lemma OAI.CoulombAtom.corePerm_sign line 183
  15. lemma OAI.CoulombAtom.joinLists_corePerm line 187
  16. def OAI.CoulombAtom.coreSlice line 194
  17. def OAI.CoulombAtom.SobolevFermion line 199
  18. lemma OAI.CoulombAtom.FormAdmissible.sobolevFermion line 206
  19. theorem OAI.CoulombAtom.SobolevFermion.ae_coreSlice line 209
  20. def OAI.CoulombAtom.formMass line 249
  21. lemma OAI.CoulombAtom.formMass_nonneg line 252
  22. def OAI.CoulombAtom.scaleForm line 255
  23. lemma OAI.CoulombAtom.SobolevFermion.scale line 259
  24. lemma OAI.CoulombAtom.scaled_norm_sq line 273
  25. lemma OAI.CoulombAtom.formMass_scale line 276
  26. lemma OAI.CoulombAtom.formEnergy_scale line 280
  27. lemma OAI.CoulombAtom.SobolevFermion.admissible line 290
  28. theorem OAI.CoulombAtom.SobolevFermion.normalize line 298
  29. lemma OAI.CoulombAtom.energy_le_form line 304
  30. lemma OAI.CoulombAtom.SobolevFermion.mass_zero_nuclear line 314
  31. theorem OAI.CoulombAtom.SobolevFermion.energy_mul_mass_le line 326
  32. theorem OAI.CoulombAtom.conditional_core_energy line 349