OAI/Analysis/Laughlin/FourBody/Scaled.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Certificate.weightSqrtDiagonal line 10
  2. def OAI.Laughlin.Certificate.certificateDiagonal line 13
  3. def OAI.Laughlin.Certificate.scaledError line 17
  4. def OAI.Laughlin.Certificate.scaledGram line 20
  5. theorem OAI.Laughlin.Certificate.cast_rat_diagonal line 23
  6. theorem OAI.Laughlin.Certificate.cast_rat_sub line 28
  7. theorem OAI.Laughlin.Certificate.copyWeight_nonneg line 33
  8. theorem OAI.Laughlin.Certificate.weightSqrtDiagonal_sq line 37
  9. theorem OAI.Laughlin.Certificate.weightSqrtDiagonal_middle_diagonal line 45
  10. theorem OAI.Laughlin.Certificate.scaled_compression_identity line 61
  11. theorem OAI.Laughlin.Certificate.scaled_compression_positive line 68