OAI/Computability/PerfectCompleteness/Decoding/LowerCutUniformCoordinatesLemmas.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutUniformCoordinates.NativeSample line 29
  2. abbrev OAI.PerfectCompleteness.LowerCutUniformCoordinates.LowerSample line 33
  3. def OAI.PerfectCompleteness.LowerCutUniformCoordinates.sampleEquiv line 39
  4. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.sampleEquiv_apply line 44
  5. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.lowerDirection_nonempty line 54
  6. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.uniformLaw_pushforward line 63
  7. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.probability_transport line 74
  8. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.expectation_transport line 88
  9. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.collision_transport line 105
  10. theorem OAI.PerfectCompleteness.LowerCutUniformCoordinates.collision_probability line 122
  11. theorem OAI.PerfectCompleteness.LowerCutUniformCollisionLaw.direction_probability_eq line 161
  12. theorem OAI.PerfectCompleteness.LowerCutUniformCollisionLaw.native_probability_eq line 184
  13. theorem OAI.PerfectCompleteness.LowerCutUniformCollisionLaw.answer_installMatrix line 227
  14. theorem OAI.PerfectCompleteness.LowerCutUniformCollisionLaw.probability_eq line 247
  15. theorem OAI.PerfectCompleteness.FixedLowerRawCollision.branchPositive line 328
  16. abbrev OAI.PerfectCompleteness.FixedLowerRawCollision.UpperTable line 335
  17. def OAI.PerfectCompleteness.FixedLowerRawCollision.fullCollisionProbability line 340
  18. theorem OAI.PerfectCompleteness.FixedLowerRawCollision.supported_fullCollision_le line 361
  19. theorem OAI.PerfectCompleteness.FixedLowerRawCollision.mean_fullCollision_le line 383