OAI/Analysis/CoulombIonization/ThomasFermi/TfIncreasingData.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAnalysis.tfIncreasingData line 64
  2. def OAI.CoulombAnalysis.tfIncreasingField line 65
  3. def OAI.CoulombAnalysis.tfIncreasingCharge line 66
  4. def OAI.CoulombAnalysis.tfInfiniteRadial line 67
  5. lemma OAI.CoulombAnalysis.tfIncreasingField_monotone line 69
  6. lemma OAI.CoulombAnalysis.tfIncreasingField_bounded line 80
  7. lemma OAI.CoulombAnalysis.tfIncreasingField_le line 86
  8. lemma OAI.CoulombAnalysis.tfInfiniteRadial_nonneg line 89
  9. lemma OAI.CoulombAnalysis.tfIncreasingField_tendsto line 92
  10. lemma OAI.CoulombAnalysis.tfInfiniteRadial_upper line 96
  11. lemma OAI.CoulombAnalysis.tfInfiniteRadial_far_bound line 101
  12. lemma OAI.CoulombAnalysis.tfInfiniteRadial_lipschitz line 106
  13. lemma OAI.CoulombAnalysis.tfInfiniteRadial_continuous line 114
  14. lemma OAI.CoulombAnalysis.positive_uIcc line 118
  15. lemma OAI.CoulombAnalysis.positive_uIoc line 121
  16. lemma OAI.CoulombAnalysis.tf_reaction_continuous line 124
  17. lemma OAI.CoulombAnalysis.tf_reaction_nonneg line 129
  18. def OAI.CoulombAnalysis.tfFluxSource line 133
  19. def OAI.CoulombAnalysis.tfFiniteSource line 134
  20. lemma OAI.CoulombAnalysis.tfFluxSource_continuous line 136
  21. lemma OAI.CoulombAnalysis.tfFiniteSource_continuous line 139
  22. lemma OAI.CoulombAnalysis.tfFluxSource_intervalIntegrable line 143
  23. lemma OAI.CoulombAnalysis.tfFiniteSource_intervalIntegrable line 148
  24. lemma OAI.CoulombAnalysis.tfFiniteSource_integral_tendsto line 153
  25. lemma OAI.CoulombAnalysis.tfIncreasingCharge_integral line 168
  26. structure OAI.CoulombAnalysis.TFChargeAnchor line 180
  27. lemma OAI.CoulombAnalysis.tfChargeAnchor_nonempty line 186
  28. def OAI.CoulombAnalysis.tfChargeAnchor line 192
  29. def OAI.CoulombAnalysis.tfInfiniteCharge line 193
  30. lemma OAI.CoulombAnalysis.tfIncreasingCharge_subseq_tendsto line 195
  31. lemma OAI.CoulombAnalysis.tfInfiniteCharge_nonneg line 201
  32. lemma OAI.CoulombAnalysis.tfInfiniteCharge_cap line 205
  33. lemma OAI.CoulombAnalysis.tfInfiniteCharge_hasDerivAt line 210
  34. def OAI.CoulombAnalysis.tfInfiniteSlope line 216
  35. def OAI.CoulombAnalysis.tfFiniteSlope line 217
  36. lemma OAI.CoulombAnalysis.tfInfiniteSlope_continuous line 219
  37. lemma OAI.CoulombAnalysis.tfFiniteSlope_continuous line 222
  38. lemma OAI.CoulombAnalysis.tfInfiniteSlope_intervalIntegrable line 225
  39. lemma OAI.CoulombAnalysis.tfFiniteSlope_intervalIntegrable line 230
  40. lemma OAI.CoulombAnalysis.tfFiniteSlope_integral_subseq line 235
  41. lemma OAI.CoulombAnalysis.tfInfiniteRadial_integral line 250
  42. lemma OAI.CoulombAnalysis.tfInfiniteRadial_hasDerivAt line 262
  43. lemma OAI.CoulombAnalysis.tfInfiniteCharge_contDiffOn line 271
  44. lemma OAI.CoulombAnalysis.tfInfiniteRadial_contDiffOn line 280