OAI/Analysis/CoulombRadii/FormDomain/RetainedPotentialMean.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.fromH1_raw_bounded_integral line 13
2. theorem OAI.NeutralAtom.retainedEvent_potential_mean line 29
3. lemma OAI.NeutralAtom.conditionalPacketPotential_integrable line 66
4. lemma OAI.NeutralAtom.normalized_event_const_sub line 78
5. lemma OAI.NeutralAtom.normalized_event_le line 86
6. lemma OAI.NeutralAtom.le_normalized_event line 98
7. theorem OAI.NeutralAtom.retainedEvent_field_mean line 110