OAI/Combinatorics/TriangleRemoval/Process/HistoryCompensator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.historyCompensator line 17
2. theorem OAI.SharpTerminalLeave.history_noise_compensator line 22
3. def OAI.SharpTerminalLeave.prefixNormalizedCodegree line 44
4. def OAI.SharpTerminalLeave.prefixCodegreePredictableError line 48
5. def OAI.SharpTerminalLeave.PrefixCodegreeDriftExit line 53
6. theorem OAI.SharpTerminalLeave.codegree_first_exit_noise_or_drift line 60