OAI/Analysis/MatrixSigning/Potential/NegativeWeight.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.State.negativeWeight line 24
  2. def OAI.CurrentKS.State.mixedTerm line 27
  3. lemma OAI.CurrentKS.State.mixedTerm_bound line 30
  4. lemma OAI.CurrentKS.State.secondExpansion_bound line 60
  5. lemma OAI.CurrentKS.State.hasDerivAt_S_line line 78
  6. def OAI.CurrentKS.State.eta₁ line 82
  7. def OAI.CurrentKS.State.eta₂ line 85
  8. lemma OAI.CurrentKS.State.eta₁_apply line 88
  9. lemma OAI.CurrentKS.State.eta₂_apply line 92
  10. lemma OAI.CurrentKS.State.hasDerivAt_eta_line line 96
  11. lemma OAI.CurrentKS.State.hasDerivAt_eta₁_line line 107
  12. lemma OAI.CurrentKS.State.hasDerivAt_deriv_eta_line line 118