OAI/Analysis/CoulombIonization/ThomasFermi/TfInfiniteFieldDominatesDilation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAnalysis.tfInfiniteField_dominates_dilation line 67
  2. lemma OAI.CoulombAnalysis.tf_first_field_large line 82
  3. lemma OAI.CoulombAnalysis.tfInfiniteField_singular_lower line 96
  4. theorem OAI.CoulombAnalysis.tfInfiniteField_singularProfile line 120
  5. def OAI.CoulombAnalysis.tfSupportRadius line 148
  6. lemma OAI.CoulombAnalysis.tfSupportRadius_gt_one line 150
  7. lemma OAI.CoulombAnalysis.TFUnitData.uniform_support line 155
  8. lemma OAI.CoulombAnalysis.TFUnitData.exterior_field line 169
  9. lemma OAI.CoulombAnalysis.TFUnitData.radialField_le_infinite line 179
  10. def OAI.CoulombAnalysis.tfRealRadial line 188
  11. def OAI.CoulombAnalysis.tfUnitDeficit line 189
  12. lemma OAI.CoulombAnalysis.tfRealRadial_tendsto line 191
  13. def OAI.CoulombAnalysis.tfResidualCharge line 210
  14. lemma OAI.CoulombAnalysis.tfResidualCharge_pos line 212
  15. lemma OAI.CoulombAnalysis.TFUnitData.deficit_eq line 219
  16. theorem OAI.CoulombAnalysis.tf_unit_deficit_tendsto line 224
  17. lemma OAI.CoulombAnalysis.tfUnitDeficit_nonneg line 231
  18. lemma OAI.CoulombAnalysis.tfUnitDeficit_le line 237