OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/SpinTensorResidual.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Tensor residual bounds in the full physical spin measure, with the exact mass of the weak-H1 finite tensor state as normalization.

  1. theorem OAI.ContinuumCoulomb.spinTensorResidual_L2_bound line 16
  2. theorem OAI.ContinuumCoulomb.flatRealSpinOrbital_norm_sq line 40