OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/CoerciveComplementLower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar form estimates for replacing the manufactured density by point nuclei. The complement norm can be the full H1 norm rather than L2 mass.

  1. theorem OAI.ContinuumCoulomb.coercive_complement_scalar_lower line 11
  2. theorem OAI.ContinuumCoulomb.three_mixed_square_bound line 20
  3. theorem OAI.ContinuumCoulomb.perturbed_coercive_complement line 25