OAI/Analysis/CoulombRadii/RandomFields/CoreGap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.RecordedEnsemble.core_gap_lower line 16
2. lemma OAI.Coulomb.RecordedEnsemble.predecessor_bound_of_core_budget line 33
3. lemma OAI.NeutralAtom.event_count_upper line 62
4. theorem OAI.NeutralAtom.atomic_arrayEvent_deficit_upper line 94
5. lemma OAI.NeutralAtom.raw_inner_observed_count_le line 123
6. lemma OAI.NeutralAtom.observed_deficit_event_measurable line 141
7. lemma OAI.NeutralAtom.observed_deficit_event_symmetric line 147
8. theorem OAI.NeutralAtom.atomic_observed_inner_deficit_tail line 156