OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteAtomicOutputs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed YES and NO instances need only finiteness of the atomic energy. No hydrogen spectral formula is needed for this branch of the reduction.

  1. def OAI.ContinuumCoulomb.atomicThresholdOutput line 12

    Source documentation

    A fixed one-electron unit nucleus with adjacent integer thresholds.

    def atomicThresholdOutput (z : ℤ) : UnitCoulomb where
…

    Mentions: OAI.ContinuumCoulomb.UnitCoulomb

  2. theorem OAI.ContinuumCoulomb.atomicThresholdOutput_valid line 18
  3. theorem OAI.ContinuumCoulomb.atomicThresholdOutput_data line 37
  4. theorem OAI.ContinuumCoulomb.exists_atomic_yes_no line 46