OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/WeightedNuclearCross.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute nuclear form errors control mixed terms on the full complex, spinful weak-H1 domain.

  1. theorem OAI.ContinuumCoulomb.weighted_inner_pairing line 13
  2. def OAI.ContinuumCoulomb.nuclearErrorCross line 37
  3. def OAI.ContinuumCoulomb.nuclearAbsoluteError line 40
  4. theorem OAI.ContinuumCoulomb.nuclearErrorCross_square_bound line 43
  5. theorem OAI.ContinuumCoulomb.nuclearAbsoluteError_bound line 64
  6. theorem OAI.ContinuumCoulomb.nuclearErrorCross_graph_square_bound line 75