OAI/Analysis/CoulombRadii/SpectralTheory/BindingCut.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.bindingCut line 12
2. lemma OAI.Coulomb.bindingCut_smooth line 13
3. lemma OAI.Coulomb.bindingCut_partition line 14
4. lemma OAI.Coulomb.bindingCut_derivative line 17
5. lemma OAI.Coulomb.bindingCut_attraction line 20
6. def OAI.Coulomb.bindingLocalized line 30
7. def OAI.Coulomb.configurationBox line 34
8. lemma OAI.Coulomb.configurationBox_measurable line 35
9. lemma OAI.Coulomb.configurationBox_finite line 38
10. lemma OAI.Coulomb.bindingLocalized_value_outside line 55
11. lemma OAI.Coulomb.bindingLocalized_norm_le line 66
12. lemma OAI.Coulomb.binding_loss_controls_cut line 74
13. lemma OAI.Coulomb.binding_loss_bound line 98