OAI/Analysis/CoulombIonization/Variational/OwnStateResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.OwnProbabilityTailTiltState.mono_error line 14
2. lemma OAI.CoulombAtom.normalized_sector_excess_le line 23
3. lemma OAI.CoulombAtom.exists_small_error_product line 33
4. lemma OAI.CoulombAtom.own_state_graph_bound line 44
5. def OAI.CoulombAtom.SmallSectorResidual line 51
6. lemma OAI.CoulombAtom.smallSectorResidual_of_own line 55
7. lemma OAI.CoulombAtom.exists_own_state_small_residual line 60
8. lemma OAI.CoulombAtom.exists_own_state_shell_residual line 69