OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteTensorResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The polynomial tensor residual is the actual differential residual of finite tensor synthesis in the full physical spin space.

  1. def OAI.ContinuumCoulomb.finiteTensorResidualValue line 15
  2. theorem OAI.ContinuumCoulomb.tensorOrbitalResidual_memLp line 20
  3. theorem OAI.ContinuumCoulomb.finiteTensorResidualValue_memLp line 36
  4. theorem OAI.ContinuumCoulomb.finiteTensorResidualValue_eq_flat line 44
  5. theorem OAI.ContinuumCoulomb.finiteTensorResidualValue_norm line 64
  6. theorem OAI.ContinuumCoulomb.finiteTensorState_value_C2 line 77
  7. theorem OAI.ContinuumCoulomb.finiteTensorState_gradient_classical line 88
  8. theorem OAI.ContinuumCoulomb.finiteTensorState_operator_residual line 101