OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorUnaryScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual unary programs for the polynomial mediator scale, its square, and the retained-term and spoke coefficient bounds.

  1. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.scale line 11
  2. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.delta line 18
  3. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.retainedBound line 27
  4. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.spokeBound line 31