OAI/InformationTheory/BooleanNoise/LambdaScalars.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.CourtadeKumar.lambda line 14
2. theorem OAI.LeanBlast.CourtadeKumar.lambda_zero line 16
3. theorem OAI.LeanBlast.CourtadeKumar.lambda_of_ne_zero line 18
4. theorem OAI.LeanBlast.CourtadeKumar.mul_lambda line 21
5. theorem OAI.LeanBlast.CourtadeKumar.hasSum_lambda line 27
6. theorem OAI.LeanBlast.CourtadeKumar.summable_lambda line 43
7. theorem OAI.LeanBlast.CourtadeKumar.monotoneOn_lambda line 47
8. theorem OAI.LeanBlast.CourtadeKumar.one_le_lambda line 53
9. theorem OAI.LeanBlast.CourtadeKumar.lambda_nonneg line 56