OAI/Analysis/CoulombIonization/RadialBounds/FockKineticReindexBarrier.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.sum_out_reindex line 17
2. lemma OAI.CoulombAtom.outKinetic_reindex line 30
3. def OAI.CoulombAtom.unorderedOutKinetic line 51
4. lemma OAI.CoulombAtom.full_out_kinetic_eq line 58
5. lemma OAI.CoulombAtom.core_branch_gradient_zero line 68
6. lemma OAI.CoulombAtom.weighted_gradient_le_out_branches line 86
7. def OAI.CoulombAtom.localGradientTrace line 117
8. lemma OAI.CoulombAtom.local_gradient_integrable line 121
9. lemma OAI.CoulombAtom.local_gradient_integral_le line 132
10. theorem OAI.CoulombAtom.localGradientTrace_le_full_out line 157