OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteTensorKineticCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual differential residual identifies the finite tensor kinetic and bounded-potential form with its CAR matrix.

  1. theorem OAI.ContinuumCoulomb.finiteTensorState_residual_compression line 15
  2. theorem OAI.ContinuumCoulomb.finiteTensorState_bounded_compression line 56