OAI/Geometry/UnitDistances/Information.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.FiniteInformation.KL line 9
  2. def OAI.PlanarUnitDistances.FiniteInformation.TV line 12
  3. lemma OAI.PlanarUnitDistances.FiniteInformation.hellinger_pointwise line 15
  4. theorem OAI.PlanarUnitDistances.FiniteInformation.hellinger_le_KL line 36
  5. theorem OAI.PlanarUnitDistances.FiniteInformation.TV_sq_le_KL line 44
  6. theorem OAI.PlanarUnitDistances.FiniteInformation.KL_nonneg line 69
  7. lemma OAI.PlanarUnitDistances.FiniteInformation.KL_term_chain line 75
  8. lemma OAI.PlanarUnitDistances.FiniteInformation.sum_ac line 87
  9. theorem OAI.PlanarUnitDistances.FiniteInformation.KL_chain line 98
  10. theorem OAI.PlanarUnitDistances.FiniteInformation.KL_fst_le line 122
  11. def OAI.PlanarUnitDistances.FiniteInformation.push line 148
  12. lemma OAI.PlanarUnitDistances.FiniteInformation.push_nonneg line 152
  13. lemma OAI.PlanarUnitDistances.FiniteInformation.push_sum line 161
  14. lemma OAI.PlanarUnitDistances.FiniteInformation.push_ac line 167
  15. lemma OAI.PlanarUnitDistances.FiniteInformation.KL_graph line 175
  16. theorem OAI.PlanarUnitDistances.FiniteInformation.KL_push_le line 187
  17. theorem OAI.PlanarUnitDistances.FiniteInformation.KL_push_chain line 198
  18. theorem OAI.PlanarUnitDistances.FiniteInformation.expectation_TV line 211
  19. def OAI.PlanarUnitDistances.FiniteInformation.row line 223
  20. def OAI.PlanarUnitDistances.FiniteInformation.cond line 226
  21. lemma OAI.PlanarUnitDistances.FiniteInformation.row_nonneg line 229
  22. lemma OAI.PlanarUnitDistances.FiniteInformation.row_ac line 232
  23. lemma OAI.PlanarUnitDistances.FiniteInformation.cond_nonneg line 237
  24. lemma OAI.PlanarUnitDistances.FiniteInformation.cond_sum line 241
  25. lemma OAI.PlanarUnitDistances.FiniteInformation.cond_ac line 246
  26. lemma OAI.PlanarUnitDistances.FiniteInformation.cond_KL_nonneg line 257
  27. theorem OAI.PlanarUnitDistances.FiniteInformation.conditional_TV_sq line 264
  28. lemma OAI.PlanarUnitDistances.FiniteInformation.row_expectation line 290
  29. theorem OAI.PlanarUnitDistances.FiniteInformation.conditional_centered_bound line 302
  30. lemma OAI.PlanarUnitDistances.FiniteInformation.push_expectation line 327
  31. lemma OAI.PlanarUnitDistances.FiniteInformation.push_comp line 338
  32. lemma OAI.PlanarUnitDistances.FiniteInformation.push_id line 357
  33. lemma OAI.PlanarUnitDistances.FiniteInformation.push_equiv line 362
  34. lemma OAI.PlanarUnitDistances.FiniteInformation.KL_push_equiv line 369
  35. lemma OAI.PlanarUnitDistances.FiniteInformation.push_pair line 374
  36. lemma OAI.PlanarUnitDistances.FiniteInformation.push_fst line 389
  37. lemma OAI.PlanarUnitDistances.FiniteInformation.row_refinement line 396
  38. lemma OAI.PlanarUnitDistances.FiniteInformation.KL_refinement_nonneg line 407
  39. def OAI.PlanarUnitDistances.FiniteInformation.mean line 421
  40. lemma OAI.PlanarUnitDistances.FiniteInformation.norm_mean_le line 425
  41. lemma OAI.PlanarUnitDistances.FiniteInformation.centered_mean line 443
  42. def OAI.PlanarUnitDistances.FiniteInformation.paired line 451
  43. lemma OAI.PlanarUnitDistances.FiniteInformation.paired_row line 455
  44. lemma OAI.PlanarUnitDistances.FiniteInformation.paired_cond line 460
  45. lemma OAI.PlanarUnitDistances.FiniteInformation.paired_centered line 465
  46. theorem OAI.PlanarUnitDistances.FiniteInformation.feature_increment line 485
  47. def OAI.PlanarUnitDistances.FiniteInformation.observation line 514
  48. lemma OAI.PlanarUnitDistances.FiniteInformation.product_observation line 518
  49. lemma OAI.PlanarUnitDistances.FiniteInformation.observation_row line 533
  50. lemma OAI.PlanarUnitDistances.FiniteInformation.observation_entropy line 537
  51. theorem OAI.PlanarUnitDistances.FiniteInformation.observation_covariance line 546
  52. def OAI.PlanarUnitDistances.FiniteInformation.wedge line 580
  53. theorem OAI.PlanarUnitDistances.FiniteInformation.wedge_square line 583
  54. lemma OAI.PlanarUnitDistances.FiniteInformation.wedge_nonneg line 602
  55. lemma OAI.PlanarUnitDistances.FiniteInformation.wedge_sum line 606
  56. theorem OAI.PlanarUnitDistances.FiniteInformation.weighted_inner_bound line 614
  57. def OAI.PlanarUnitDistances.FiniteInformation.History line 638
  58. instance OAI.PlanarUnitDistances.FiniteInformation.historyFintype line 642
  59. instance OAI.PlanarUnitDistances.FiniteInformation.historyDecidableEq line 648
  60. lemma OAI.PlanarUnitDistances.FiniteInformation.history_card line 653
  61. def OAI.PlanarUnitDistances.FiniteInformation.transcript line 665
  62. def OAI.PlanarUnitDistances.FiniteInformation.transcriptKL line 669
  63. lemma OAI.PlanarUnitDistances.FiniteInformation.transcriptKL_zero line 674
  64. lemma OAI.PlanarUnitDistances.FiniteInformation.transcriptKL_mono line 679
  65. theorem OAI.PlanarUnitDistances.FiniteInformation.transcript_budget line 691
  66. def OAI.PlanarUnitDistances.FiniteInformation.marginal line 706
  67. lemma OAI.PlanarUnitDistances.FiniteInformation.marginal_nonneg line 710
  68. lemma OAI.PlanarUnitDistances.FiniteInformation.marginal_sum line 714
  69. lemma OAI.PlanarUnitDistances.FiniteInformation.wedge_ac line 723
  70. lemma OAI.PlanarUnitDistances.FiniteInformation.average_sq_le line 744
  71. lemma OAI.PlanarUnitDistances.FiniteInformation.average_sqrt_le line 757
  72. def OAI.PlanarUnitDistances.FiniteInformation.residual line 771
  73. def OAI.PlanarUnitDistances.FiniteInformation.discrepancy line 775
  74. theorem OAI.PlanarUnitDistances.FiniteInformation.frozen_prediction line 779
  75. def OAI.PlanarUnitDistances.FiniteInformation.posterior line 850
  76. lemma OAI.PlanarUnitDistances.FiniteInformation.row_push_pair line 854
  77. lemma OAI.PlanarUnitDistances.FiniteInformation.mean_posterior line 860
  78. lemma OAI.PlanarUnitDistances.FiniteInformation.fresh_integral line 877
  79. lemma OAI.PlanarUnitDistances.FiniteInformation.average_integral_bound line 899
  80. instance OAI.PlanarUnitDistances.FiniteInformation.historyMeasurable line 917
  81. lemma OAI.PlanarUnitDistances.FiniteInformation.transcript_congr line 924
  82. lemma OAI.PlanarUnitDistances.FiniteInformation.measurable_transcript line 933
  83. lemma OAI.PlanarUnitDistances.FiniteInformation.prefix_independent line 945
  84. lemma OAI.PlanarUnitDistances.FiniteInformation.norm_convex_sum_le line 980
  85. def OAI.PlanarUnitDistances.FiniteInformation.testDiscrepancy line 989
  86. lemma OAI.PlanarUnitDistances.FiniteInformation.testDiscrepancy_bound line 994
  87. theorem OAI.PlanarUnitDistances.FiniteInformation.random_prediction line 1024
  88. lemma OAI.PlanarUnitDistances.FiniteInformation.sqrt_sqrt_eq_quarter line 1062
  89. theorem OAI.PlanarUnitDistances.FiniteInformation.exists_prediction_history line 1066