OAI/Analysis/CoulombIonization/RadialBounds/CoupledCoreExcessBarrier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.outKinetic_nonneg line 19
2. lemma OAI.CoulombAtom.outRepulsion_nonneg line 23
3. lemma OAI.CoulombAtom.cutExteriorPrice_eq_field_work line 31
4. lemma OAI.CoulombAtom.cutCoreExcess_le_field_work line 46
5. lemma OAI.CoulombAtom.conditionalFieldSum_le_max line 63
6. lemma OAI.CoulombAtom.radial_max_out_product_integrable line 73
7. theorem OAI.CoulombAtom.radial_full_field_work_budget line 96
8. theorem OAI.CoulombAtom.radial_core_excess_coupling line 130
9. lemma OAI.CoulombAtom.radial_freshMaximum_statistic_integrable line 151
10. lemma OAI.CoulombAtom.CoreObservationGraph.outMoment_eq_average line 163
11. theorem OAI.CoulombAtom.CoreObservationGraph.observe_excess_budget line 187