OAI/Analysis/CoulombIonization/Fermionic/MultiplierError.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAtom.graph_value_components_ext line 75
2. lemma OAI.CoulombAtom.complex_square_partition line 83
3. lemma OAI.CoulombAtom.FermionMultiplier.partition_apply line 92
4. lemma OAI.CoulombAtom.FermionMultiplier.partition_mass line 108
5. def OAI.CoulombAtom.multiplierError line 121
6. lemma OAI.CoulombAtom.multiplierError_nonneg line 126
7. theorem OAI.CoulombAtom.quantum_partition_ims line 134
8. lemma OAI.CoulombAtom.quantum_form_above_sector line 150
9. theorem OAI.CoulombAtom.quantum_partition_excess line 156