OAI/InformationTheory/BooleanNoise/CubeVariance.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.binaryRelativeEntropy line 16
  2. theorem OAI.LeanBlast.CourtadeKumar.one_sub_sq_pos_of_interior line 20
  3. theorem OAI.LeanBlast.CourtadeKumar.binaryRelativeEntropy_eq line 24
  4. theorem OAI.LeanBlast.CourtadeKumar.sub_le_mul_log_div line 36
  5. theorem OAI.LeanBlast.CourtadeKumar.binaryRelativeEntropy_nonneg line 44
  6. theorem OAI.LeanBlast.CourtadeKumar.binaryRelativeEntropy_le_sq_div line 54
  7. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_eq_average_psi line 76
  8. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_eq_average_binaryRelativeEntropy line 82
  9. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_nonneg line 104
  10. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_le_variance_div line 109
  11. theorem OAI.LeanBlast.CourtadeKumar.abs_cubeAverage_le line 118
  12. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_pairDomain line 124
  13. theorem OAI.LeanBlast.CourtadeKumar.IsInterior.of_pairDomain_left line 134
  14. theorem OAI.LeanBlast.CourtadeKumar.average_one_sub_sq_pos line 140
  15. theorem OAI.LeanBlast.CourtadeKumar.scaled_informationDeficit_le_variance_gap line 145
  16. theorem OAI.LeanBlast.CourtadeKumar.entropy_product_le_scaled_informationDeficit line 175
  17. theorem OAI.LeanBlast.CourtadeKumar.entropy_product_le_variance_gap line 193