OAI/Analysis/CoulombIonization/Variational/ActualSectorPlateau.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.quantum_strict_binding_particle_bound line 18
2. lemma OAI.CoulombAtom.quantum_energy_step_at_coarse_fence line 24
3. theorem OAI.CoulombAtom.quantum_energy_plateau line 33
4. lemma OAI.CoulombAtom.quantum_energy_coarse_fence_minimum line 43
5. theorem OAI.CoulombAtom.quantum_unpriced_infimum_finite line 49
6. theorem OAI.CoulombAtom.actual_priced_particle_bound_three line 61