OAI/Analysis/CoulombIonization/Localization/Observation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.SplitPositionSupport line 15
2. lemma OAI.CoulombAtom.orderedCutForm_nonzero_factors line 19
3. lemma OAI.CoulombAtom.SplitPositionSupport.observe line 45
4. lemma OAI.CoulombAtom.SplitPositionSupport.mono line 70
5. def OAI.CoulombAtom.CoreObservationGraph.supported line 78
6. lemma OAI.CoulombAtom.CoreObservationGraph.initial_supported line 80
7. lemma OAI.CoulombAtom.CoreObservationGraph.observe_supported line 84
8. def OAI.CoulombAtom.CoreObservationEnsemble.supported line 92
9. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_supported line 94
10. lemma OAI.CoulombAtom.CoreObservationEnsemble.observe_supported line 97
11. lemma OAI.CoulombAtom.cell_core_nonzero_distance line 107
12. lemma OAI.CoulombAtom.cell_out_nonzero_norm line 114
13. lemma OAI.CoulombAtom.CoreObservationEnsemble.observeCells_supported line 127
14. lemma OAI.CoulombAtom.CoreObservationEnsemble.annular_stencil_support line 149
15. lemma OAI.CoulombAtom.exists_scaled_shell_stencil line 166