OAI/Analysis/CoulombIonization/Localization/ObservedInnerCap.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.annular_cut_cost_innerScale line 14
2. lemma OAI.CoulombAtom.finite_annular_excess_at_innerScale line 24
3. lemma OAI.CoulombAtom.actual_observed_local_count line 54
4. theorem OAI.CoulombAtom.exists_actual_observed_innerCap_constant line 73
5. structure OAI.CoulombAtom.FullStatistic line 122
6. lemma OAI.CoulombAtom.rawFormPair_reindex line 129
7. lemma OAI.CoulombAtom.rawFormPair_nextCoreObservation line 140
8. lemma OAI.CoulombAtom.sum_rawFormPair_nextCoreObservation line 148
9. def OAI.CoulombAtom.CoreObservationGraph.fullAverage line 174
10. lemma OAI.CoulombAtom.CoreObservationGraph.observe_fullAverage line 176
11. def OAI.CoulombAtom.CoreObservationEnsemble.fullAverage line 183
12. lemma OAI.CoulombAtom.CoreObservationEnsemble.initial_fullAverage line 185
13. lemma OAI.CoulombAtom.CoreObservationEnsemble.observe_fullAverage line 189
14. lemma OAI.CoulombAtom.CoreObservationEnsemble.observeCells_fullAverage line 196