OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/NuclearPerturbedComplement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complement elimination with the actual singular nuclear error form. The general form error enters quadratically through its mixed term.

  1. def OAI.ContinuumCoulomb.nuclearPerturbedForm line 13
  2. theorem OAI.ContinuumCoulomb.nuclearPerturbedForm_add line 16
  3. theorem OAI.ContinuumCoulomb.nuclearPerturbed_coercive_complement line 29
  4. theorem OAI.ContinuumCoulomb.nuclearPerturbed_interacting_lower line 49