OAI/Analysis/CoulombRadii/Propagation/PropagationDatumRegularity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.continuous_ball_bounds line 14
2. lemma OAI.NeutralAtom.propagationPairOffset_joint_measurable line 24
3. lemma OAI.NeutralAtom.propagationPairOffset_uniform_bounds line 31
4. lemma OAI.NeutralAtom.propagationNextOffset_joint_measurable line 48
5. lemma OAI.NeutralAtom.propagationNextOffset_uniform_bounds line 56
6. lemma OAI.NeutralAtom.propagationStepError_joint_measurable line 66
7. lemma OAI.NeutralAtom.propagationStepError_uniform_bounds line 75
8. lemma OAI.NeutralAtom.atomic_screenedField_nuclear line 101
9. lemma OAI.NeutralAtom.conditionalPacketField_nuclear line 116
10. structure OAI.NeutralAtom.PropagationInvariant line 137
11. lemma OAI.NeutralAtom.PropagationStepHypotheses.next_invariant line 147
12. lemma OAI.NeutralAtom.propagationCoreSource_joint_measurable line 160
13. lemma OAI.NeutralAtom.propagationCoreSource_uniform_bounds line 167
14. lemma OAI.NeutralAtom.propagationCoreSource_average line 177
15. theorem OAI.NeutralAtom.PropagationInvariant.average line 190