OAI/Combinatorics/TriangleRemoval/Tracking/PrefixCodegreeErrorExit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.PrefixCodegreeErrorExit line 17
  2. lemma OAI.SharpTerminalLeave.codegreeNoiseRadius_tendsto_zero line 22
  3. lemma OAI.SharpTerminalLeave.pmfMean_event_or_upper line 28
  4. lemma OAI.SharpTerminalLeave.any_codegree_exit_noise_or_drift line 47
  5. def OAI.SharpTerminalLeave.prefixCodegreeErrorProbability line 61
  6. def OAI.SharpTerminalLeave.prefixCodegreeDriftProbability line 67
  7. def OAI.SharpTerminalLeave.prefixCodegreeNoiseProbability line 73
  8. lemma OAI.SharpTerminalLeave.prefix_codegree_error_probability_split line 77
  9. lemma OAI.SharpTerminalLeave.prefix_codegree_noise_probability_bound line 91
  10. theorem OAI.SharpTerminalLeave.prefix_codegree_error_probability_reduction line 97