OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorFormDecomposition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact form polarization for the full finite tensor projection and its weak-H1 remainder, including the singular electron repulsion.

  1. theorem OAI.ContinuumCoulomb.h1_add_sub_cancel line 14
  2. theorem OAI.ContinuumCoulomb.finiteTensorProjection_add_remainder line 25
  3. theorem OAI.ContinuumCoulomb.tensorProjection_form_decomposition line 35