OAI/Computability/PerfectCompleteness/Algebra/BucketMatrixResampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.BucketMatrixResampling.Matrix line 17
2. def OAI.PerfectCompleteness.BucketMatrixResampling.assembledMatrix line 19
3. theorem OAI.PerfectCompleteness.BucketMatrixResampling.assembledMatrix_update line 22
4. theorem OAI.PerfectCompleteness.BucketMatrixResampling.pushforward_id line 35
5. theorem OAI.PerfectCompleteness.BucketMatrixResampling.matrix_difference_law line 44
6. theorem OAI.PerfectCompleteness.BucketMatrixResampling.resampled_matrix_pair_law line 58
7. theorem OAI.PerfectCompleteness.BucketMatrixResampling.uniform_assembledMatrix_law line 73
8. theorem OAI.PerfectCompleteness.BucketMatrixResampling.uniform_matrix_difference_law line 78
9. theorem OAI.PerfectCompleteness.BucketMatrixResampling.uniform_resampled_matrix_pair_law line 85
10. theorem OAI.PerfectCompleteness.BucketMatrixResampling.uniform_resampled_event_probability line 95