OAI/InformationTheory/BooleanNoise/EntropyBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.psiSeries line 13
  2. theorem OAI.LeanBlast.CourtadeKumar.norm_psiSeries_term_le line 15
  3. theorem OAI.LeanBlast.CourtadeKumar.summable_psi_closed line 22
  4. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_psiSeries line 26
  5. theorem OAI.LeanBlast.CourtadeKumar.psiSeries_eq_psi line 34
  6. theorem OAI.LeanBlast.CourtadeKumar.hasSum_psi_closed line 43
  7. theorem OAI.LeanBlast.CourtadeKumar.hasSum_psiCoeff line 48
  8. theorem OAI.LeanBlast.CourtadeKumar.tsum_psiCoeff line 51
  9. theorem OAI.LeanBlast.CourtadeKumar.half_sq_le_psi line 53
  10. theorem OAI.LeanBlast.CourtadeKumar.psi_le_ell_mul_sq line 59
  11. theorem OAI.LeanBlast.CourtadeKumar.ell_mul_one_sub_sq_le_entropy line 69