OAI/Analysis/MatrixSigning/Potential/StateR.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.State.LightPoint.R line 17
  2. def OAI.CurrentKS.State.LightPoint.tildeA line 18
  3. def OAI.CurrentKS.State.LightPoint.tildeB line 19
  4. def OAI.CurrentKS.State.LightPoint.resp line 20
  5. def OAI.CurrentKS.State.LightPoint.direction line 21
  6. def OAI.CurrentKS.State.LightPoint.invEnergy line 22
  7. lemma OAI.CurrentKS.State.LightPoint.tildeA_pos line 26
  8. lemma OAI.CurrentKS.State.LightPoint.tildeB_pos line 27
  9. lemma OAI.CurrentKS.State.LightPoint.wP_pos line 28
  10. lemma OAI.CurrentKS.State.LightPoint.wQ_pos line 29
  11. lemma OAI.CurrentKS.State.LightPoint.multiplied_direction line 30
  12. lemma OAI.CurrentKS.State.LightPoint.R_first line 34
  13. lemma OAI.CurrentKS.State.LightPoint.R_second line 48
  14. lemma OAI.CurrentKS.State.LightPoint.crossed_identity line 67
  15. lemma OAI.CurrentKS.State.LightPoint.negativeWeight_lower line 73
  16. lemma OAI.CurrentKS.State.LightPoint.R_second_rescaled line 93
  17. lemma OAI.CurrentKS.State.LightPoint.R_ensemble_curvature line 100