OAI/Analysis/MatrixSigning/Potential/CoarseBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.State.contDiff_S line 27
2. lemma OAI.CurrentKS.State.contDiffAt_eta line 32
3. def OAI.CurrentKS.State.coarseBudget line 41
4. lemma OAI.CurrentKS.State.coarseBudget_bounds line 45
5. lemma OAI.CurrentKS.State.contDiffAt_face_eta line 65
6. lemma OAI.CurrentKS.State.strip_S_jet line 72
7. lemma OAI.CurrentKS.State.strip_eta_jet line 85
8. lemma OAI.CurrentKS.State.kkt_strip_jet line 97
9. theorem OAI.CurrentKS.State.value_strip_derivatives line 116