OAI/InformationTheory/BooleanNoise/LargeCurvature.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.CourtadeKumar.large_parameter_gt_81 line 12
2. theorem OAI.LeanBlast.CourtadeKumar.large_artanh_gt_eleven_tenths line 19
3. theorem OAI.LeanBlast.CourtadeKumar.entropy_eq_large_parameter_form line 34
4. theorem OAI.LeanBlast.CourtadeKumar.large_parameter_polynomial_bound line 45
5. theorem OAI.LeanBlast.CourtadeKumar.large_curvature_bound line 62