OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorScaleBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete weight and inverse-weight bounds for the three mediator stages. Each bound is a fixed polynomial in entering unary parameters.

  1. theorem OAI.ContinuumCoulomb.MediatorParameters.spoke_lower_half line 10
  2. theorem OAI.ContinuumCoulomb.MediatorParameters.spoke_upper line 21
  3. def OAI.ContinuumCoulomb.MediatorParameters.secondWeight line 28
  4. def OAI.ContinuumCoulomb.MediatorParameters.thirdWeight line 31
  5. def OAI.ContinuumCoulomb.MediatorParameters.finalWeight line 35
  6. theorem OAI.ContinuumCoulomb.MediatorParameters.secondWeight_two_le line 39
  7. theorem OAI.ContinuumCoulomb.MediatorParameters.thirdWeight_two_le line 43
  8. theorem OAI.ContinuumCoulomb.MediatorParameters.finalWeight_two_le line 47
  9. theorem OAI.ContinuumCoulomb.MediatorParameters.second_spoke_bounds line 51
  10. theorem OAI.ContinuumCoulomb.MediatorParameters.third_spoke_bounds line 63
  11. theorem OAI.ContinuumCoulomb.MediatorParameters.third_central_bounds line 80