OAI/InformationTheory/SoftChannel/Production.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LeanBlast.CourtadeKumar.IsInterior.neg_soft line 14
2. lemma OAI.LeanBlast.CourtadeKumar.dissipation_neg_soft line 19
3. lemma OAI.LeanBlast.CourtadeKumar.IsInterior.information_lt_entropy line 30
4. lemma OAI.LeanBlast.CourtadeKumar.IsInterior.information_mem line 35
5. lemma OAI.LeanBlast.CourtadeKumar.r_pooled_child_information line 39
6. lemma OAI.LeanBlast.CourtadeKumar.ordered_positive_joining line 47
7. lemma OAI.LeanBlast.CourtadeKumar.positive_joining line 79
8. lemma OAI.LeanBlast.CourtadeKumar.all_soft_meanReserve line 92
9. theorem OAI.LeanBlast.CourtadeKumar.all_soft_sharp_production line 99
10. theorem OAI.LeanBlast.CourtadeKumar.all_soft_max_production line 131