OAI/InformationTheory/SoftChannel/Canonical.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.bose line 14
  2. def OAI.LeanBlast.CourtadeKumar.canonicalQ line 16
  3. def OAI.LeanBlast.CourtadeKumar.normalizedEntropy line 18
  4. lemma OAI.LeanBlast.CourtadeKumar.bose_pos line 25
  5. lemma OAI.LeanBlast.CourtadeKumar.exp_neg_lt_one line 28
  6. lemma OAI.LeanBlast.CourtadeKumar.bose_eq_exp_neg line 31
  7. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_bose line 38
  8. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_canonicalQ line 46
  9. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_canonicalQ_deriv line 57
  10. lemma OAI.LeanBlast.CourtadeKumar.canonicalQ_second_pos line 65
  11. lemma OAI.LeanBlast.CourtadeKumar.convexOn_canonicalQ line 80
  12. def OAI.LeanBlast.CourtadeKumar.canonicalGroup line 92
  13. lemma OAI.LeanBlast.CourtadeKumar.exp_pair line 97
  14. lemma OAI.LeanBlast.CourtadeKumar.geom_positive_sum line 103
  15. lemma OAI.LeanBlast.CourtadeKumar.canonicalGroup_eq line 110
  16. lemma OAI.LeanBlast.CourtadeKumar.hasSum_canonicalGroup line 126
  17. lemma OAI.LeanBlast.CourtadeKumar.log_bose line 143
  18. lemma OAI.LeanBlast.CourtadeKumar.log_bose_add_one line 148
  19. lemma OAI.LeanBlast.CourtadeKumar.log_one_add_bose_add_bose line 155
  20. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropy_series_identity line 173
  21. lemma OAI.LeanBlast.CourtadeKumar.hasSum_normalizedEntropy line 184
  22. lemma OAI.LeanBlast.CourtadeKumar.canonicalExp_jensen line 190
  23. lemma OAI.LeanBlast.CourtadeKumar.canonicalGroup_jensen line 198
  24. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropy_jensen line 212
  25. def OAI.LeanBlast.CourtadeKumar.normalizedEntropyDz line 230
  26. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropy_symm line 234
  27. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropyDz_neg line 240
  28. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_normalizedEntropy_comp line 251
  29. lemma OAI.LeanBlast.CourtadeKumar.positive_line line 271
  30. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropy_tangent line 277
  31. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropyDz_order line 300
  32. lemma OAI.LeanBlast.CourtadeKumar.hasDerivAt_bose_deriv line 308
  33. lemma OAI.LeanBlast.CourtadeKumar.convexOn_bose line 313
  34. lemma OAI.LeanBlast.CourtadeKumar.bose_tangent line 326
  35. def OAI.LeanBlast.CourtadeKumar.canonicalPrice line 339
  36. def OAI.LeanBlast.CourtadeKumar.canonicalGamma line 341
  37. lemma OAI.LeanBlast.CourtadeKumar.canonicalPrice_pos line 344
  38. lemma OAI.LeanBlast.CourtadeKumar.canonicalPrice_gradient line 349
  39. lemma OAI.LeanBlast.CourtadeKumar.canonicalGamma_nonneg line 356
  40. lemma OAI.LeanBlast.CourtadeKumar.canonicalGamma_gradient line 366
  41. lemma OAI.LeanBlast.CourtadeKumar.canonicalGamma_self line 374
  42. lemma OAI.LeanBlast.CourtadeKumar.canonical_support_normalized line 378
  43. lemma OAI.LeanBlast.CourtadeKumar.entropy_degree line 393
  44. def OAI.LeanBlast.CourtadeKumar.joiningZ line 405
  45. def OAI.LeanBlast.CourtadeKumar.joiningW line 406
  46. def OAI.LeanBlast.CourtadeKumar.joiningCost line 407
  47. lemma OAI.LeanBlast.CourtadeKumar.joiningZ_pos line 409
  48. lemma OAI.LeanBlast.CourtadeKumar.joiningW_pos line 414
  49. lemma OAI.LeanBlast.CourtadeKumar.bose_joiningZ line 419
  50. lemma OAI.LeanBlast.CourtadeKumar.bose_joiningW line 427
  51. lemma OAI.LeanBlast.CourtadeKumar.joining_order line 435
  52. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropy_actual line 441
  53. lemma OAI.LeanBlast.CourtadeKumar.joiningCost_coordinates line 471
  54. lemma OAI.LeanBlast.CourtadeKumar.joiningCost_nonneg line 479
  55. def OAI.LeanBlast.CourtadeKumar.coreKappa line 488
  56. lemma OAI.LeanBlast.CourtadeKumar.normalizedEntropy_nonneg line 491
  57. lemma OAI.LeanBlast.CourtadeKumar.coreKappa_pos line 505
  58. lemma OAI.LeanBlast.CourtadeKumar.canonical_support line 512
  59. lemma OAI.LeanBlast.CourtadeKumar.canonical_core_contact line 535
  60. lemma OAI.LeanBlast.CourtadeKumar.averaged_canonical_support line 546
  61. lemma OAI.LeanBlast.CourtadeKumar.canonical_core_lower line 557
  62. def OAI.LeanBlast.CourtadeKumar.onecornerX line 572
  63. def OAI.LeanBlast.CourtadeKumar.onecornerY line 573
  64. def OAI.LeanBlast.CourtadeKumar.onecornerEntropy line 574
  65. def OAI.LeanBlast.CourtadeKumar.reflectedEntropy line 577
  66. lemma OAI.LeanBlast.CourtadeKumar.onecorner_domain line 579
  67. lemma OAI.LeanBlast.CourtadeKumar.onecorner_means line 593
  68. lemma OAI.LeanBlast.CourtadeKumar.onecorner_entropy_left line 598
  69. lemma OAI.LeanBlast.CourtadeKumar.onecorner_entropy_right line 606
  70. lemma OAI.LeanBlast.CourtadeKumar.continuousOn_onecornerEntropy line 611
  71. lemma OAI.LeanBlast.CourtadeKumar.exists_onecorner_entropy line 621
  72. lemma OAI.LeanBlast.CourtadeKumar.exists_reflected_entropy line 628
  73. lemma OAI.LeanBlast.CourtadeKumar.onecorner_cost_lower line 652
  74. lemma OAI.LeanBlast.CourtadeKumar.reflected_cost_lower line 668