OAI/Analysis/MatrixSigning/Potential/DerivPathObjective.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.State.hasDerivAt_path_objective line 24
2. lemma OAI.CurrentKS.State.deriv_deriv_path_objective line 35
3. lemma OAI.CurrentKS.State.first_response_path line 50
4. lemma OAI.CurrentKS.State.first_response_path_neg line 63
5. lemma OAI.CurrentKS.State.deriv_deriv_S_line line 77
6. lemma OAI.CurrentKS.State.second_response_path line 84
7. lemma OAI.CurrentKS.State.deriv_deriv_neg_S_line line 104
8. lemma OAI.CurrentKS.State.second_response_path_neg line 111