OAI/InformationTheory/SoftChannel/Contraction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.IsClosedSoft line 12
  2. lemma OAI.LeanBlast.CourtadeKumar.closed_information_mem line 14
  3. lemma OAI.LeanBlast.CourtadeKumar.soft_noise_interior line 23
  4. lemma OAI.LeanBlast.CourtadeKumar.soft_flow_interior line 33
  5. lemma OAI.LeanBlast.CourtadeKumar.soft_model_domain line 38
  6. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_soft_model line 46
  7. theorem OAI.LeanBlast.CourtadeKumar.all_soft_flow_contraction line 54
  8. theorem OAI.LeanBlast.CourtadeKumar.all_soft_nonnegative_contraction line 81
  9. def OAI.LeanBlast.CourtadeKumar.antipodeEquiv line 105
  10. lemma OAI.LeanBlast.CourtadeKumar.cubeAverage_antipode line 111
  11. lemma OAI.LeanBlast.CourtadeKumar.information_antipode line 116
  12. lemma OAI.LeanBlast.CourtadeKumar.kernel_negative_correlation line 121
  13. lemma OAI.LeanBlast.CourtadeKumar.information_negative_correlation line 129
  14. theorem OAI.LeanBlast.CourtadeKumar.all_soft_contraction line 136