OAI/Analysis/MatrixSigning/Potential/StateIA.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.State.LightPoint.IA line 19
  2. def OAI.CurrentKS.State.LightPoint.IB line 20
  3. def OAI.CurrentKS.State.LightPoint.wP line 21
  4. def OAI.CurrentKS.State.LightPoint.wQ line 22
  5. def OAI.CurrentKS.State.LightPoint.s0 line 23
  6. def OAI.CurrentKS.State.LightPoint.J line 24
  7. def OAI.CurrentKS.State.LightPoint.E0 line 25
  8. def OAI.CurrentKS.State.LightPoint.C1 line 26
  9. lemma OAI.CurrentKS.State.LightPoint.s0_pos line 27
  10. lemma OAI.CurrentKS.State.LightPoint.s0_le_one line 28
  11. lemma OAI.CurrentKS.State.LightPoint.E0_pos line 29
  12. lemma OAI.CurrentKS.State.LightPoint.C1_ge_one line 34
  13. lemma OAI.CurrentKS.State.LightPoint.C1_pos line 35
  14. lemma OAI.CurrentKS.State.LightPoint.primal_lower line 37
  15. lemma OAI.CurrentKS.State.LightPoint.primal_square_lower line 46
  16. lemma OAI.CurrentKS.State.LightPoint.interaction_row_gap line 56
  17. lemma OAI.CurrentKS.State.LightPoint.IA_psd line 87
  18. lemma OAI.CurrentKS.State.LightPoint.IB_psd line 88
  19. lemma OAI.CurrentKS.State.LightPoint.IA_norm_le line 89
  20. lemma OAI.CurrentKS.State.LightPoint.IB_norm_le line 102
  21. lemma OAI.CurrentKS.State.LightPoint.coupled_movement line 116
  22. lemma OAI.CurrentKS.State.LightPoint.covariance_movement_bounds line 127