OAI/Computability/PerfectCompleteness/Decoding/RepresentativeBucketCollisionLemmas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RepresentativeBucketCollision.bucketTable line 24
  2. def OAI.PerfectCompleteness.RepresentativeBucketCollision.bucketAccepted line 29
  3. theorem OAI.PerfectCompleteness.RepresentativeBucketCollision.bucketTable_eq_some_iff line 32
  4. theorem OAI.PerfectCompleteness.RepresentativeBucketCollision.collision_probability_lower_bound line 45
  5. theorem OAI.PerfectCompleteness.RepresentativeDecoder.residualVector_subtype line 88
  6. theorem OAI.PerfectCompleteness.RepresentativeDecoder.residualVector_section line 96
  7. theorem OAI.PerfectCompleteness.RepresentativeDecoder.correctionFunctional_comp_subtype line 105
  8. theorem OAI.PerfectCompleteness.RepresentativeDecoder.correctionFunctional_comp_section line 115
  9. theorem OAI.PerfectCompleteness.RepresentativeDecoder.correctionFunctional_decomposition line 123
  10. theorem OAI.PerfectCompleteness.RepresentativeDecoder.correctionFunctional_unique line 136
  11. theorem OAI.PerfectCompleteness.RepresentativeDecoder.quotientFunctional_mem_annihilator line 150
  12. theorem OAI.PerfectCompleteness.RepresentativeDecoder.coset_apply line 158
  13. theorem OAI.PerfectCompleteness.RepresentativeDecoder.coset_comp_subtype line 170
  14. theorem OAI.PerfectCompleteness.RepresentativeDecoder.add_quotient_comp_subtype line 177
  15. theorem OAI.PerfectCompleteness.RepresentativeDecoder.coset_apply_at_image line 183
  16. theorem OAI.PerfectCompleteness.RepresentativeDecoder.coset_one_at_image line 192
  17. theorem OAI.PerfectCompleteness.RepresentativeDecoder.coset_product_at_image line 200
  18. theorem OAI.PerfectCompleteness.RepresentativeDecoder.matched_coset_realized_on_W line 211
  19. theorem OAI.PerfectCompleteness.RepresentativeDecoder.raw_selected_output_at_match line 228
  20. theorem OAI.PerfectCompleteness.DenseWitnessRealization.witness_value_attained line 264
  21. abbrev OAI.PerfectCompleteness.DenseWitnessRealization.RepresentativeWitness line 292
  22. theorem OAI.PerfectCompleteness.DenseWitnessRealization.exists_useful_match line 297
  23. theorem OAI.PerfectCompleteness.DenseWitnessRealization.exists_joint_realizer line 311
  24. theorem OAI.PerfectCompleteness.DenseWitnessRealization.selected_side_mem_range line 326
  25. theorem OAI.PerfectCompleteness.DenseWitnessRealization.exists_coset_realizer line 332
  26. theorem OAI.PerfectCompleteness.DenseWitnessRealization.selected_columns_le_annihilator line 353