OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorFirstReplacement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Replacing one orbital in a finite tensor expansion costs the squared L2 size of the replacement family, without an exponential dimension factor.

  1. def OAI.ContinuumCoulomb.tensorCoefficientSlice line 15
  2. def OAI.ContinuumCoulomb.tensorFirstReplacement line 19
  3. theorem OAI.ContinuumCoulomb.tensorCoefficientSlice_memLp line 23
  4. theorem OAI.ContinuumCoulomb.tensorCoefficientSlice_norm line 32
  5. theorem OAI.ContinuumCoulomb.tensorFirstReplacement_memLp line 51
  6. theorem OAI.ContinuumCoulomb.tensorFirstReplacement_pointwise line 60
  7. theorem OAI.ContinuumCoulomb.tensorFirstReplacement_L2_bound line 71
  8. theorem OAI.ContinuumCoulomb.sum_cons_coefficient_norm line 99