OAI/Analysis/MatrixSigning/Potential/StatePsi.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.State.LightPoint.contDiffAt_R line 16
  2. lemma OAI.CurrentKS.State.LightPoint.contDiffAt_R_line line 23
  3. lemma OAI.CurrentKS.State.LightPoint.contDiffAt_penalty_line line 28
  4. def OAI.CurrentKS.State.LightPoint.Psi line 34
  5. def OAI.CurrentKS.State.LightPoint.omega line 36
  6. def OAI.CurrentKS.State.LightPoint.mu line 39
  7. def OAI.CurrentKS.State.LightPoint.dirs line 42
  8. def OAI.CurrentKS.State.LightPoint.driftCurvature line 45
  9. lemma OAI.CurrentKS.State.LightPoint.omega_nonneg line 49
  10. lemma OAI.CurrentKS.State.LightPoint.Psi_first line 52
  11. lemma OAI.CurrentKS.State.LightPoint.Psi_second line 62
  12. lemma OAI.CurrentKS.State.LightPoint.R_driftCurvature_nonpos line 73
  13. lemma OAI.CurrentKS.State.LightPoint.dirs_energy line 90
  14. lemma OAI.CurrentKS.State.LightPoint.penalty_driftCurvature line 97
  15. lemma OAI.CurrentKS.State.LightPoint.Psi_driftCurvature line 123
  16. theorem OAI.CurrentKS.State.LightPoint.exists_descent_ensemble line 131