OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ContactCalibration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous calibration of every edge of the actual positive mediator graph, together with whole-matrix Coulomb coercivity for its realized sites.

  1. theorem OAI.ContinuumCoulomb.ContactMediator.exists_calibrated_finalGraph_above line 14
  2. theorem OAI.ContinuumCoulomb.ContactMediator.exists_calibrated_finalGraph line 75