OAI/Analysis/CoulombIonization/ThomasFermi/PatchTF.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CoulombAnalysis.TFField line 16
  2. def OAI.CoulombAnalysis.tfPatchPair line 18
  3. lemma OAI.CoulombAnalysis.tfPatchPair_apply line 21
  4. def OAI.CoulombAnalysis.tfPatchLinear line 25
  5. lemma OAI.CoulombAnalysis.tfPatchLinear_apply line 28
  6. def OAI.CoulombAnalysis.tfPatchFunctional line 32
  7. lemma OAI.CoulombAnalysis.tfPatchFunctional_continuous line 35
  8. lemma OAI.CoulombAnalysis.tfPatchFunctional_lower line 41
  9. lemma OAI.CoulombAnalysis.tfPatchFunctional_bddBelow line 50
  10. lemma OAI.CoulombAnalysis.tfPatchFunctional_coercive line 63
  11. lemma OAI.CoulombAnalysis.tfPatchFunctional_gap line 71
  12. theorem OAI.CoulombAnalysis.tfPatchFunctional_exists_minimizer line 82
  13. lemma OAI.CoulombAnalysis.tfPatchFunctional_min_unique line 101
  14. def OAI.CoulombAnalysis.tfPatchMinimizer line 122
  15. lemma OAI.CoulombAnalysis.tfPatchMinimizer_nonneg line 125
  16. lemma OAI.CoulombAnalysis.tfPatchMinimizer_min line 129
  17. lemma OAI.CoulombAnalysis.nonnegDensity_zero line 134
  18. lemma OAI.CoulombAnalysis.tfPatchFunctional_zero line 139
  19. def OAI.CoulombAnalysis.tfPatchNormBound line 144
  20. lemma OAI.CoulombAnalysis.tfPatchMinimizer_norm_le line 147
  21. lemma OAI.CoulombAnalysis.tfPatchLinear_continuous line 170
  22. lemma OAI.CoulombAnalysis.tfPatchNormBound_continuous line 173
  23. lemma OAI.CoulombAnalysis.tfPatchNormBound_nonneg line 176
  24. lemma OAI.CoulombAnalysis.tfPatchMinimizer_distance_rpow line 179
  25. theorem OAI.CoulombAnalysis.tfPatchMinimizer_continuous line 225
  26. lemma OAI.CoulombAnalysis.tfPatchMinimizer_measurable line 258