OAI/Analysis/CoulombIonization/ThomasFermi/TfReactionCoefficient.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAnalysis.tfReactionCoefficient line 67
  2. lemma OAI.CoulombAnalysis.tfReactionCoefficient_pos line 69
  3. lemma OAI.CoulombAnalysis.tfField_finiteProfile line 74
  4. theorem OAI.CoulombAnalysis.tf_finiteProfile_exists line 121
  5. structure OAI.CoulombAnalysis.TFUnitData line 134
  6. lemma OAI.CoulombAnalysis.tfUnitData_nonempty line 145
  7. def OAI.CoulombAnalysis.tfUnitData line 149
  8. def OAI.CoulombAnalysis.TFUnitData.field line 154
  9. def OAI.CoulombAnalysis.TFUnitData.radialField line 155
  10. def OAI.CoulombAnalysis.TFUnitData.charge line 156
  11. lemma OAI.CoulombAnalysis.TFUnitData.finiteProfile line 158
  12. lemma OAI.CoulombAnalysis.TFUnitData.support_le line 161
  13. lemma OAI.CoulombAnalysis.TFUnitData.ray_norm line 164
  14. lemma OAI.CoulombAnalysis.TFUnitData.ray_ne_zero line 166
  15. lemma OAI.CoulombAnalysis.TFUnitData.field_radial line 169
  16. lemma OAI.CoulombAnalysis.TFUnitData.radialField_eq line 174
  17. lemma OAI.CoulombAnalysis.TFUnitData.radialField_ray line 180
  18. lemma OAI.CoulombAnalysis.TFUnitData.radialField_nonneg line 184
  19. lemma OAI.CoulombAnalysis.TFUnitData.mass_le_charge line 188
  20. lemma OAI.CoulombAnalysis.TFUnitData.charge_nonneg line 197
  21. lemma OAI.CoulombAnalysis.TFUnitData.charge_hasDerivAt line 204
  22. lemma OAI.CoulombAnalysis.TFUnitData.radialField_hasDerivAt line 208
  23. lemma OAI.CoulombAnalysis.TFUnitData.charge_antitone line 218
  24. lemma OAI.CoulombAnalysis.TFUnitData.radialField_antitone line 225
  25. lemma OAI.CoulombAnalysis.TFUnitData.charge_bound line 232
  26. lemma OAI.CoulombAnalysis.TFUnitData.radialField_upper line 255
  27. lemma OAI.CoulombAnalysis.TFUnitData.charge_equation line 266
  28. lemma OAI.CoulombAnalysis.TFUnitData.radialField_le_charge_div line 276
  29. def OAI.CoulombAnalysis.TFUnitData.chargeCap line 291
  30. def OAI.CoulombAnalysis.TFUnitData.slopeCap line 292
  31. lemma OAI.CoulombAnalysis.TFUnitData.chargeCap_pos line 294
  32. lemma OAI.CoulombAnalysis.TFUnitData.slopeCap_pos line 299
  33. lemma OAI.CoulombAnalysis.TFUnitData.charge_le_cap line 302
  34. lemma OAI.CoulombAnalysis.TFUnitData.radialField_far_bound line 308
  35. lemma OAI.CoulombAnalysis.TFUnitData.deriv_bound line 313
  36. lemma OAI.CoulombAnalysis.TFUnitData.lipschitz line 320