OAI/InformationTheory/SoftChannel/HighReserve.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.CourtadeKumar.softCutoff line 12
2. def OAI.LeanBlast.CourtadeKumar.centeredRate line 13
3. def OAI.LeanBlast.CourtadeKumar.meanReserve line 15
4. lemma OAI.LeanBlast.CourtadeKumar.softCutoff_pos line 18
5. lemma OAI.LeanBlast.CourtadeKumar.softCutoff_lt_ell line 19
6. lemma OAI.LeanBlast.CourtadeKumar.artanh_77_upper line 21
7. lemma OAI.LeanBlast.CourtadeKumar.softCutoff_lower line 31
8. lemma OAI.LeanBlast.CourtadeKumar.softCutoff_above_center line 36
9. lemma OAI.LeanBlast.CourtadeKumar.centeredRate_cutoff_pos line 39
10. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_centeredRate line 55
11. lemma OAI.LeanBlast.CourtadeKumar.centeredRate_nonneg line 61
12. lemma OAI.LeanBlast.CourtadeKumar.rGap_tangent line 76
13. lemma OAI.LeanBlast.CourtadeKumar.high_information_reserve line 86
14. lemma OAI.LeanBlast.CourtadeKumar.meanReserve_zero_mean line 113