OAI/InformationTheory/SoftChannel/RateSlope.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.CourtadeKumar.slopeT line 12
2. def OAI.LeanBlast.CourtadeKumar.slopePolynomial line 13
3. def OAI.LeanBlast.CourtadeKumar.RateSlope_slopeBernstein line 15
4. lemma OAI.LeanBlast.CourtadeKumar.RateSlope_slopeBernstein_pos line 27
5. lemma OAI.LeanBlast.CourtadeKumar.slopePolynomial_bernstein line 30
6. lemma OAI.LeanBlast.CourtadeKumar.slopePolynomial_pos line 38
7. lemma OAI.LeanBlast.CourtadeKumar.slopeT_lower line 44
8. lemma OAI.LeanBlast.CourtadeKumar.r_slope_bound_psi line 49
9. lemma OAI.LeanBlast.CourtadeKumar.r_slope_bound line 77