OAI/MathematicalPhysics/ContinuumCoulomb/Programs/MediatorOffsetProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact rational threshold offsets for the fully computed mediator construction, using actual gcd-based rational-list summation.

  1. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.absoluteWeight line 12
  2. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.totalWeight line 15
  3. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.parameters line 20
  4. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.rRational line 28
  5. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.penalty line 32
  6. def OAI.ContinuumCoulomb.MediatorOffsetProgram.stageOffset line 36
  7. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.stageOffsetProgram line 40
  8. def OAI.ContinuumCoulomb.MediatorOffsetProgram.offset line 46
  9. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.offsetProgram line 53
  10. opaque OAI.ContinuumCoulomb.MediatorOffsetProgram.errorProgram line 58
  11. def OAI.ContinuumCoulomb.MediatorOffsetProgram.certificate line 65