OAI/Analysis/FreeEntropy/GaussianEntropyEvent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.entropy_subprobability_bound line 10
2. def OAI.FiniteEntropySeparation.eventTilt line 27
3. theorem OAI.FiniteEntropySeparation.eventTilt_expand line 29
4. theorem OAI.FiniteEntropySeparation.eventTilt_log line 33
5. theorem OAI.FiniteEntropySeparation.entropy_event_bound line 45