OAI/InformationTheory/BooleanNoise/EntropySeries.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.psiCoeff line 13
  2. theorem OAI.LeanBlast.CourtadeKumar.psiCoeff_pos line 15
  3. theorem OAI.LeanBlast.CourtadeKumar.psiCoeff_nonneg line 17
  4. theorem OAI.LeanBlast.CourtadeKumar.psiCoeff_zero line 19
  5. theorem OAI.LeanBlast.CourtadeKumar.hasSum_artanh line 21
  6. theorem OAI.LeanBlast.CourtadeKumar.hasSum_mul_artanh line 30
  7. theorem OAI.LeanBlast.CourtadeKumar.psi_eq_mul_artanh_add_log line 42
  8. theorem OAI.LeanBlast.CourtadeKumar.hasSum_psi line 54
  9. theorem OAI.LeanBlast.CourtadeKumar.sum_range_artanh_le line 75
  10. theorem OAI.LeanBlast.CourtadeKumar.sum_range_psi_le line 81
  11. theorem OAI.LeanBlast.CourtadeKumar.summable_psiCoeff line 88