OAI/Probability/BinarySweep/Conditional/AugmentedBlock.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.augmentedFrame line 22
2. def OAI.BinaryCoordinateSweeps.augmentedRepresentation line 26
3. lemma OAI.BinaryCoordinateSweeps.augmented_subgroup_perm line 29
4. lemma OAI.BinaryCoordinateSweeps.placementBlock_expectation line 42
5. theorem OAI.BinaryCoordinateSweeps.augmented_block_average line 70
6. lemma OAI.BinaryCoordinateSweeps.placementBijection_index line 122
7. lemma OAI.BinaryCoordinateSweeps.placementKernel_ratio line 130
8. lemma OAI.BinaryCoordinateSweeps.placementKernel_output_pos line 137
9. lemma OAI.BinaryCoordinateSweeps.placementBlock_zero line 148
10. lemma OAI.BinaryCoordinateSweeps.placementBlock_moment line 164
11. lemma OAI.BinaryCoordinateSweeps.placementBlock_moment_root line 178