OAI/Geometry/RCD/Harmonic/GramTraceDefect.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Trace and square moments controlled by the original Gram defect

  1. def OAI.RegularPointCoordinates.matrixGramDefect line 11
  2. theorem OAI.RegularPointCoordinates.matrixGramDefect_nonneg line 14
  3. theorem OAI.RegularPointCoordinates.gram_trace_defect line 17
  4. theorem OAI.RegularPointCoordinates.gram_square_defect line 29