OAI/Probability/SKGap/Brownian/LogDetPath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.logPath line 14
2. lemma OAI.SKGap.pathDiagonal_square_at line 17
3. lemma OAI.SKGap.pathShift_eq line 28
4. lemma OAI.SKGap.logPath_eq line 32
5. lemma OAI.SKGap.hasDerivAt_logPath line 39
6. lemma OAI.SKGap.pathK_agrees_at line 47
7. def OAI.SKGap.logPathCutoffDerivative line 71
8. lemma OAI.SKGap.logPath_trace_derivative line 76
9. lemma OAI.SKGap.continuous_logPathCutoffDerivative line 83