OAI/Analysis/CoulombIonization/Variational/PhaseBathtub.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.CoulombAtom.phase_bathtubline 16 - def
OAI.CoulombAtom.momentumIntervalline 77 - lemma
OAI.CoulombAtom.measurableSet_momentumIntervalline 80 - lemma
OAI.CoulombAtom.momentumInterval_absline 83 - lemma
OAI.CoulombAtom.momentumInterval_disjointline 92 - lemma
OAI.CoulombAtom.volume_momentumIntervalline 104 - def
OAI.CoulombAtom.momentumCellline 117 - lemma
OAI.CoulombAtom.measurableSet_momentumCellline 120 - lemma
OAI.CoulombAtom.volume_momentumCellline 124 - lemma
OAI.CoulombAtom.momentumCell_disjointline 132 - lemma
OAI.CoulombAtom.momentumCell_norm_sqline 139