OAI/Analysis/CoulombIonization/RadialBounds/BallAverageKernelBarrier.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.space_closedBall_real line 19
2. def OAI.CoulombAtom.ballAverageKernel line 24
3. lemma OAI.CoulombAtom.ballAverageKernel_measurable line 27
4. lemma OAI.CoulombAtom.ballAverageKernel_nonneg line 30
5. lemma OAI.CoulombAtom.ballAverageKernel_support line 35
6. lemma OAI.CoulombAtom.ballAverageKernel_bound line 40
7. lemma OAI.CoulombAtom.ballAverageKernel_radial line 47
8. lemma OAI.CoulombAtom.ballAverageKernel_mass line 51
9. lemma OAI.CoulombAtom.joinLists_empty line 62
10. lemma OAI.CoulombAtom.coreSlice_empty line 68
11. lemma OAI.CoulombAtom.coreLawAverage_empty line 74
12. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_mass line 81
13. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_countMoment line 85
14. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_fieldMoment line 89
15. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_excess line 93
16. lemma OAI.CoulombAtom.CoreObservationEnsemble.countMoment_le_of_radius line 98
17. lemma OAI.CoulombAtom.CoreObservationEnsemble.outMoment_le_ball_field line 102
18. def OAI.CoulombAtom.localHistoryRadius line 135
19. def OAI.CoulombAtom.localHistoryReach line 136
20. lemma OAI.CoulombAtom.localHistoryRadius_pos line 138
21. lemma OAI.CoulombAtom.localHistoryRadius_le line 141
22. lemma OAI.CoulombAtom.localHistoryReach_nonneg line 146
23. lemma OAI.CoulombAtom.localHistoryReach_lt line 151
24. lemma OAI.CoulombAtom.localHistoryReach_step line 155
25. inductive OAI.CoulombAtom.CoreLocalHistory line 162
26. lemma OAI.CoulombAtom.CoreLocalHistory.mass line 176
27. lemma OAI.CoulombAtom.CoreLocalHistory.countMoment line 181
28. lemma OAI.CoulombAtom.CoreLocalHistory.countMoment_local line 187
29. lemma OAI.CoulombAtom.CoreLocalHistory.center_nuclear_separation line 197
30. lemma OAI.CoulombAtom.CoreLocalHistory.next_center line 206