OAI/InformationTheory/SoftChannel/Wall.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.wallA line 12
  2. def OAI.LeanBlast.CourtadeKumar.wallC line 13
  3. def OAI.LeanBlast.CourtadeKumar.wallADeriv line 14
  4. def OAI.LeanBlast.CourtadeKumar.entropySlopeAux line 16
  5. lemma OAI.LeanBlast.CourtadeKumar.artanh_neg_interior line 18
  6. lemma OAI.LeanBlast.CourtadeKumar.entropySlopeAux_neg line 24
  7. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_entropySlopeAux line 27
  8. lemma OAI.LeanBlast.CourtadeKumar.monotoneOn_entropySlopeAux line 34
  9. lemma OAI.LeanBlast.CourtadeKumar.wall_domain line 46
  10. lemma OAI.LeanBlast.CourtadeKumar.wallA_nonneg line 49
  11. lemma OAI.LeanBlast.CourtadeKumar.wallC_nonneg line 58
  12. lemma OAI.LeanBlast.CourtadeKumar.wallADeriv_lower line 64
  13. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_wallA_d line 80
  14. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_pairH_d line 87
  15. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_pairH_m line 93
  16. lemma OAI.LeanBlast.CourtadeKumar.pairH_antitone_d line 100
  17. lemma OAI.LeanBlast.CourtadeKumar.pairH_le_entropy line 112
  18. lemma OAI.LeanBlast.CourtadeKumar.rate_entropy_slope line 118
  19. def OAI.LeanBlast.CourtadeKumar.wallDemand line 153
  20. def OAI.LeanBlast.CourtadeKumar.wallDemandDeriv line 154
  21. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_wallDemand line 157
  22. lemma OAI.LeanBlast.CourtadeKumar.pairH_antitone_m line 169
  23. lemma OAI.LeanBlast.CourtadeKumar.wall_comparison line 181