OAI/Analysis/CoulombRadii/ThomasFermi/PatchNegativeCost.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.tf_negative_cost_integrable line 19
2. lemma OAI.Coulomb.rawTF_negativeError_le_gap line 39
3. lemma OAI.Coulomb.tf_negative_center_le_gap line 54
4. theorem OAI.Coulomb.exists_patch_negative_center_bound line 84
5. def OAI.Coulomb.patchSliceTFGap line 126
6. lemma OAI.Coulomb.patchSliceTFGap_nonneg line 135
7. lemma OAI.Coulomb.patchSliceTFGap_weight_integrable line 149