OAI/Analysis/FreeEntropy/BlockEvent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.matrixCoordinatesOfHermitian_continuous line 10
2. theorem OAI.FiniteEntropySeparation.rotateCoordinates_continuous_joint line 18
3. def OAI.FiniteEntropySeparation.blockEvent line 26
4. theorem OAI.FiniteEntropySeparation.blockEvent_isClosed line 29
5. theorem OAI.FiniteEntropySeparation.blockEvent_subset_net line 48
6. theorem OAI.FiniteEntropySeparation.normalLaw_rotated_mask_tail line 64
7. theorem OAI.FiniteEntropySeparation.blockEvent_gaussian_bound line 75