OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedGramConstants.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed positive coercivity constant once the total off-site leakage is at most half the common diagonal dual mass.

  1. def OAI.ContinuumCoulomb.localizedGramConstant line 13
  2. theorem OAI.ContinuumCoulomb.localizedGramConstant_positive line 16
  3. theorem OAI.ContinuumCoulomb.localizedGram_uniform_coercive line 21