OAI/InformationTheory/SoftChannel/Comparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.CourtadeKumar.Comparison_sq_lt_one_of_mem line 15
2. theorem OAI.LeanBlast.CourtadeKumar.Comparison_hasDerivAt_artanh_cubic_gap line 19
3. theorem OAI.LeanBlast.CourtadeKumar.Comparison_exp_neg_log_five line 29