OAI/InformationTheory/SoftChannel/Payment.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.pairH line 13
  2. def OAI.LeanBlast.CourtadeKumar.thinX line 14
  3. def OAI.LeanBlast.CourtadeKumar.thinI line 15
  4. def OAI.LeanBlast.CourtadeKumar.thinJ line 16
  5. lemma OAI.LeanBlast.CourtadeKumar.thinX_mem line 18
  6. lemma OAI.LeanBlast.CourtadeKumar.thinX_add line 26
  7. lemma OAI.LeanBlast.CourtadeKumar.thinX_sub line 27
  8. lemma OAI.LeanBlast.CourtadeKumar.entropy_thinX line 29
  9. lemma OAI.LeanBlast.CourtadeKumar.entropy_thinX_strict line 37
  10. lemma OAI.LeanBlast.CourtadeKumar.thinJ_nonneg line 50
  11. lemma OAI.LeanBlast.CourtadeKumar.thinJ_pos line 61
  12. lemma OAI.LeanBlast.CourtadeKumar.thinning_domain line 70
  13. lemma OAI.LeanBlast.CourtadeKumar.thinJ_le_thinI line 82
  14. lemma OAI.LeanBlast.CourtadeKumar.thinI_lt_ell line 91
  15. lemma OAI.LeanBlast.CourtadeKumar.thinning_entropy_floor line 98
  16. lemma OAI.LeanBlast.CourtadeKumar.thinning_path_window line 110
  17. lemma OAI.LeanBlast.CourtadeKumar.entropy_euler line 123
  18. lemma OAI.LeanBlast.CourtadeKumar.log_pair_defect line 130
  19. lemma OAI.LeanBlast.CourtadeKumar.thinning_defect_nonneg line 141
  20. def OAI.LeanBlast.CourtadeKumar.thinIDeriv line 152
  21. def OAI.LeanBlast.CourtadeKumar.thinJDeriv line 153
  22. def OAI.LeanBlast.CourtadeKumar.thinA line 156
  23. def OAI.LeanBlast.CourtadeKumar.thinK line 157
  24. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_thinX line 159
  25. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_entropy_thinX line 162
  26. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_thinI line 166
  27. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_thinJ line 172
  28. lemma OAI.LeanBlast.CourtadeKumar.thinI_euler line 183
  29. lemma OAI.LeanBlast.CourtadeKumar.thinJ_euler line 190
  30. lemma OAI.LeanBlast.CourtadeKumar.continuous_thinI line 203
  31. lemma OAI.LeanBlast.CourtadeKumar.continuous_thinJ line 208
  32. def OAI.LeanBlast.CourtadeKumar.normalizedDemand line 213
  33. def OAI.LeanBlast.CourtadeKumar.normalizedDemandDeriv line 215
  34. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_normalizedDemand line 219
  35. lemma OAI.LeanBlast.CourtadeKumar.normalizedDemandDeriv_nonneg line 230
  36. lemma OAI.LeanBlast.CourtadeKumar.common_output_payment line 250