OAI/Combinatorics/TriangleRemoval/Probability/AbsPmfMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.abs_pmfMean_le line 18
  2. lemma OAI.SharpTerminalLeave.pmfMean_swap line 26
  3. lemma OAI.SharpTerminalLeave.pmfMean_common_error line 39
  4. lemma OAI.SharpTerminalLeave.relative_error_absolute line 45
  5. lemma OAI.SharpTerminalLeave.product_relative_error line 53
  6. lemma OAI.SharpTerminalLeave.focusSurvival_mem_unit line 68
  7. lemma OAI.SharpTerminalLeave.cavityReference_le_one line 72
  8. theorem OAI.SharpTerminalLeave.singleton_survival_error line 78
  9. theorem OAI.SharpTerminalLeave.pair_survival_error line 94