OAI/Computability/PerfectCompleteness/Decoding/LowerProjectedFiberAverage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.LowerProjectedFiberAverage.probability_product line 19
  2. abbrev OAI.PerfectCompleteness.LowerProjectedFiberAverage.Background line 45
  3. def OAI.PerfectCompleteness.LowerProjectedFiberAverage.backgroundLaw line 47
  4. def OAI.PerfectCompleteness.LowerProjectedFiberAverage.baseline line 51
  5. def OAI.PerfectCompleteness.LowerProjectedFiberAverage.readForm line 56
  6. def OAI.PerfectCompleteness.LowerProjectedFiberAverage.collision line 63
  7. def OAI.PerfectCompleteness.LowerProjectedFiberAverage.rawCollision line 71
  8. theorem OAI.PerfectCompleteness.LowerProjectedFiberAverage.fiber_collision_eq line 78
  9. theorem OAI.PerfectCompleteness.LowerProjectedFiberAverage.rawCollision_eq_mean line 108
  10. def OAI.PerfectCompleteness.LowerProjectedFiberAverage.meanSuccess line 135
  11. theorem OAI.PerfectCompleteness.LowerProjectedFiberAverage.meanSuccess_square_le line 142