OAI/Analysis/FreeEntropy/EntropyDeficit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteEntropySeparation.Model.cumulantConstant_pos line 9
2. theorem OAI.FiniteEntropySeparation.Model.fisherDeficit_tail_integrable line 12
3. theorem OAI.FiniteEntropySeparation.Model.fisherDeficit_tail_nonneg line 15
4. theorem OAI.FiniteEntropySeparation.Model.fisherDeficit_tail_le line 20
5. theorem OAI.FiniteEntropySeparation.Model.chiStar_tail_formula line 32
6. theorem OAI.FiniteEntropySeparation.Model.entropy_deficit_le line 36