OAI/Analysis/CoulombIonization/FieldAnalysis/CoreHistoryFieldBarrier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoulombAtom.coreFieldSquare line 18
2. lemma OAI.CoulombAtom.coreFieldSquare_nonneg line 21
3. lemma OAI.CoulombAtom.coreFieldSquare_le_nuclear line 24
4. lemma OAI.CoulombAtom.coreFieldSquare_coreSlice_integrable line 31
5. lemma OAI.CoulombAtom.sum_nextCoreObservation_fieldSquare line 43
6. def OAI.CoulombAtom.CoreObservationGraph.fieldMoment line 64
7. def OAI.CoulombAtom.CoreObservationGraph.excess line 67
8. lemma OAI.CoulombAtom.CoreObservationGraph.fieldMoment_nonneg line 70
9. lemma OAI.CoulombAtom.CoreObservationGraph.fieldMoment_le_nuclear line 74
10. theorem OAI.CoulombAtom.CoreObservationGraph.fieldMoment_le_observe_excess line 87