OAI/InformationTheory/BooleanNoise/MediumCurvature.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.CourtadeKumar.curvatureNumeratorCoeff line 13
2. theorem OAI.LeanBlast.CourtadeKumar.curvatureNumeratorCoeff_nonneg line 16
3. theorem OAI.LeanBlast.CourtadeKumar.curvatureNumeratorCoeff_antitone line 20
4. theorem OAI.LeanBlast.CourtadeKumar.hasSum_artanh_div line 27
5. theorem OAI.LeanBlast.CourtadeKumar.hasSum_curvatureNumerator line 36
6. theorem OAI.LeanBlast.CourtadeKumar.curvatureT_lower line 58
7. theorem OAI.LeanBlast.CourtadeKumar.curvatureP_upper line 65
8. theorem OAI.LeanBlast.CourtadeKumar.curvatureNumerator_upper line 77
9. theorem OAI.LeanBlast.CourtadeKumar.medium_curvature_bound line 105