OAI/Analysis/MatrixSigning/Potential/LightPoint.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentKS.State.LightPoint line 15
  2. lemma OAI.CurrentKS.State.lightPoint_of_optimizer line 48
  3. lemma OAI.CurrentKS.State.inner_smul_right_fixed line 65
  4. def OAI.CurrentKS.State.LightPoint.X line 71
  5. def OAI.CurrentKS.State.LightPoint.Y line 72
  6. def OAI.CurrentKS.State.LightPoint.a line 73
  7. def OAI.CurrentKS.State.LightPoint.b line 74
  8. def OAI.CurrentKS.State.LightPoint.pp line 75
  9. def OAI.CurrentKS.State.LightPoint.qq line 76
  10. def OAI.CurrentKS.State.LightPoint.T line 77
  11. def OAI.CurrentKS.State.LightPoint.l line 78
  12. def OAI.CurrentKS.State.LightPoint.m line 79
  13. lemma OAI.CurrentKS.State.LightPoint.X_pos line 80
  14. lemma OAI.CurrentKS.State.LightPoint.Y_pos line 81
  15. lemma OAI.CurrentKS.State.LightPoint.a_pos line 82
  16. lemma OAI.CurrentKS.State.LightPoint.b_pos line 84
  17. lemma OAI.CurrentKS.State.LightPoint.pp_pos line 86
  18. lemma OAI.CurrentKS.State.LightPoint.qq_pos line 88
  19. lemma OAI.CurrentKS.State.LightPoint.scales_pos line 90
  20. lemma OAI.CurrentKS.State.LightPoint.lm_eq line 92
  21. lemma OAI.CurrentKS.State.LightPoint.lT_eq line 94
  22. lemma OAI.CurrentKS.State.LightPoint.mT_eq line 97
  23. lemma OAI.CurrentKS.State.LightPoint.product_bound line 100
  24. lemma OAI.CurrentKS.State.LightPoint.square_bounds line 102
  25. lemma OAI.CurrentKS.State.LightPoint.drift_bounds line 105
  26. lemma OAI.CurrentKS.State.LightPoint.kappa_bounds line 109