OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorSlotReplacement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The residual in any electron coordinate has the same polynomial bound. The regrouping is an exact measure-preserving separation of that coordinate.

  1. def OAI.ContinuumCoulomb.tensorSlotReplacement line 13
  2. theorem OAI.ContinuumCoulomb.tensorSlotReplacement_regroup line 17
  3. theorem OAI.ContinuumCoulomb.sum_insertNth_coefficient_norm line 39
  4. def OAI.ContinuumCoulomb.separateTensorSlot line 48
  5. theorem OAI.ContinuumCoulomb.separateTensorSlot_apply line 52
  6. theorem OAI.ContinuumCoulomb.separateTensorSlot_measurePreserving line 56
  7. theorem OAI.ContinuumCoulomb.tensorSlotReplacement_memLp line 62
  8. theorem OAI.ContinuumCoulomb.tensorSlotReplacement_L2_bound line 71