OAI/Analysis/CoulombRadii/Propagation/InitialInvariant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.propagationRHS_ball_bounds line 13
2. structure OAI.NeutralAtom.InitialPropagationData line 26
3. lemma OAI.NeutralAtom.InitialPropagationData.next_continuous line 51
4. lemma OAI.NeutralAtom.InitialPropagationData.branch_weak line 54
5. lemma OAI.NeutralAtom.InitialPropagationData.barrier_weak line 61
6. lemma OAI.NeutralAtom.InitialPropagationData.middle_weak line 72
7. lemma OAI.NeutralAtom.InitialPropagationData.next_weak line 94
8. lemma OAI.NeutralAtom.InitialPropagationData.branch_cap line 136
9. lemma OAI.NeutralAtom.InitialPropagationData.next_caps line 149
10. lemma OAI.NeutralAtom.InitialPropagationData.next_outer line 168
11. theorem OAI.NeutralAtom.InitialPropagationData.invariant line 177