OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorTotalReplacement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Summing one-body residuals over electron coordinates costs only the square of the electron count, even though the tensor coefficient space is exponential.

  1. def OAI.ContinuumCoulomb.tensorTotalReplacement line 13
  2. theorem OAI.ContinuumCoulomb.finite_sum_norm_square_le line 17
  3. theorem OAI.ContinuumCoulomb.tensorTotalReplacement_memLp line 23
  4. theorem OAI.ContinuumCoulomb.tensorTotalReplacement_L2_bound line 30