OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteTensorCross.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual finite tensor subspace has a polynomial mixed one-body form bound against its orthogonal complement.

  1. theorem OAI.ContinuumCoulomb.finiteTensorState_mixed_square_bound line 14