OAI/Analysis/MatrixSigning/Potential/Line.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.State.line line 15
  2. lemma OAI.CurrentKS.State.line_zero line 17
  3. lemma OAI.CurrentKS.State.hasDerivAt_line_coord line 19
  4. lemma OAI.CurrentKS.State.contDiff_line line 25
  5. lemma OAI.CurrentKS.State.eventually_line_interior line 30
  6. def OAI.CurrentKS.State.penalty line 36
  7. def OAI.CurrentKS.State.penalty₁ line 38
  8. def OAI.CurrentKS.State.penalty₂ line 40
  9. lemma OAI.CurrentKS.State.contDiffAt_penalty line 42
  10. lemma OAI.CurrentKS.State.hasDerivAt_penalty_line line 48
  11. lemma OAI.CurrentKS.State.hasDerivAt_penalty₁_line line 54
  12. lemma OAI.CurrentKS.State.penalty_line_first line 61
  13. lemma OAI.CurrentKS.State.penalty_line_second line 65
  14. lemma OAI.CurrentKS.State.second_deriv_add line 73
  15. lemma OAI.CurrentKS.State.second_deriv_const_mul line 77