OAI/InformationTheory/BooleanNoise/ArtanhBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.CourtadeKumar.self_le_artanh line 7
2. theorem OAI.LeanBlast.CourtadeKumar.artanh_le_div_one_sub_sq line 10
3. theorem OAI.LeanBlast.CourtadeKumar.one_sub_sq_mul_artanh_le_self line 29