OAI/Analysis/CoulombRadii/FieldAnalysis/RawThomasFermiEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.rawThomasFermiEnergy line 137
2. lemma OAI.Coulomb.sliceExpectation_congr_ae line 140
3. lemma OAI.Coulomb.discreteFineTF_eq_raw line 148
4. theorem OAI.Coulomb.conditional_source_free_lower line 159
5. lemma OAI.Coulomb.source_free_trial_raw line 188
6. def OAI.Coulomb.SourceFreeHoleDensity line 221
7. def OAI.Coulomb.packetKineticError line 229
8. lemma OAI.Coulomb.source_free_trial_from_density line 232
9. lemma OAI.Coulomb.sliceExpectation_number line 244
10. theorem OAI.Coulomb.conditional_source_free_upper line 249
11. theorem OAI.Coulomb.source_free_patch_comparison line 290