OAI/Analysis/FreeEntropy/CoordinateMask.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteEntropySeparation.coordinateMask line 11
2. theorem OAI.FiniteEntropySeparation.coordinateMask_sq line 13
3. theorem OAI.FiniteEntropySeparation.coordinateMask_norm_le line 17
4. def OAI.FiniteEntropySeparation.coordinateMaskLinear line 23
5. theorem OAI.FiniteEntropySeparation.coordinateMask_continuous line 27
6. theorem OAI.FiniteEntropySeparation.coordinateMask_norm_sub line 29
7. theorem OAI.FiniteEntropySeparation.normalLaw_coordinateMask_tail line 35