OAI/Probability/BinarySweep/Conditional/AugmentedComplement.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.augmentedOutputIndex line 20
  2. lemma OAI.BinaryCoordinateSweeps.augmentedOutputIndex_physical line 23
  3. def OAI.BinaryCoordinateSweeps.augmentationInputComplement line 36
  4. def OAI.BinaryCoordinateSweeps.augmentationOutputComplement line 41
  5. lemma OAI.BinaryCoordinateSweeps.augmentationInputComplement_val line 46
  6. lemma OAI.BinaryCoordinateSweeps.augmentationOutputComplement_val line 49
  7. lemma OAI.BinaryCoordinateSweeps.augmentedOutputIndex_event line 53
  8. lemma OAI.BinaryCoordinateSweeps.augmented_event line 68
  9. lemma OAI.BinaryCoordinateSweeps.augmentation_complement_square line 73
  10. def OAI.BinaryCoordinateSweeps.augmentedInputBasis line 87
  11. def OAI.BinaryCoordinateSweeps.augmentedOutputBasis line 90
  12. lemma OAI.BinaryCoordinateSweeps.augmented_subgroup_bijection line 94
  13. def OAI.BinaryCoordinateSweeps.Young.subPlacement line 122
  14. lemma OAI.BinaryCoordinateSweeps.Young.subPlacement_move line 126
  15. def OAI.BinaryCoordinateSweeps.Young.placementMoveEquiv line 129
  16. lemma OAI.BinaryCoordinateSweeps.Young.move_sub_eq_iff line 133
  17. def OAI.BinaryCoordinateSweeps.Young.placementMarginal line 144
  18. lemma OAI.BinaryCoordinateSweeps.Young.placementMarginal_intertwines line 162
  19. theorem OAI.BinaryCoordinateSweeps.Young.spechtPlacement_marginal_zero line 178