OAI/Analysis/CoulombIonization/ThomasFermi/PatchEuler.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.tfPatchFunctional_hasDerivAt line 17
2. lemma OAI.CoulombAnalysis.tfPatchFunctional_variation_nonneg line 38
3. lemma OAI.CoulombAnalysis.tfPatchFunctional_variation_self line 48
4. def OAI.CoulombAnalysis.tfPatchGradient line 62
5. lemma OAI.CoulombAnalysis.tfPatchGradient_integrable line 66
6. lemma OAI.CoulombAnalysis.tfPatchGradient_mul_integrable line 73
7. lemma OAI.CoulombAnalysis.tfPatchGradient_pair line 81
8. lemma OAI.CoulombAnalysis.tfPatchGradient_nonneg line 99
9. lemma OAI.CoulombAnalysis.tfPatchGradient_complementarity line 122
10. theorem OAI.CoulombAnalysis.tfPatchFunctional_euler line 133