OAI/Computability/DirectedFeedback/Games/ChainRule.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Information.firstMarginal line 13
  2. def OAI.DFVSGames.Foundations.Information.secondMarginal line 15
  3. def OAI.DFVSGames.Foundations.Information.product line 17
  4. theorem OAI.DFVSGames.Foundations.Information.firstMarginal_isProbability line 19
  5. theorem OAI.DFVSGames.Foundations.Information.secondMarginal_isProbability line 26
  6. theorem OAI.DFVSGames.Foundations.Information.product_isProbability line 35
  7. theorem OAI.DFVSGames.Foundations.Information.point_le_firstMarginal line 42
  8. theorem OAI.DFVSGames.Foundations.Information.point_le_secondMarginal line 47
  9. theorem OAI.DFVSGames.Foundations.Information.joint_supportedBy_product_marginals line 52
  10. theorem OAI.DFVSGames.Foundations.Information.relativeEntropy_product_reference line 60
  11. theorem OAI.DFVSGames.Foundations.Information.marginal_relativeEntropy_sum_le line 94
  12. def OAI.DFVSGames.Foundations.Information.conditionalKernel line 114
  13. theorem OAI.DFVSGames.Foundations.Information.conditionalKernel_isProbability line 120
  14. theorem OAI.DFVSGames.Foundations.Information.marginal_mul_conditionalKernel line 136
  15. theorem OAI.DFVSGames.Foundations.Information.law_of_total_probability line 153
  16. theorem OAI.DFVSGames.Foundations.Information.kernelProduct_isProbability line 160
  17. theorem OAI.DFVSGames.Foundations.Information.alternativeInput_conditionalProduct_isProbability line 170
  18. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.totalVariation line 189
  19. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.totalVariation_nonnegative line 192
  20. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.totalVariation_comm line 196
  21. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_sub_le_totalVariation line 204
  22. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_abs_sub_le_totalVariation line 220
  23. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_le_add_totalVariation line 230
  24. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.condition line 250
  25. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_condition line 266
  26. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_inter_eq_mul_conditional line 275
  27. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_and_le_left line 283
  28. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_and_le_right line 290
  29. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_and_eq_zero_of_probability_eq_zero line 297
  30. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_condition_given line 304
  31. theorem OAI.DFVSGames.Foundations.Games.Game.selectedWins_insert line 318
  32. def OAI.DFVSGames.Foundations.Games.Game.selectedSuccess line 329
  33. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_nonnegative line 334
  34. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_le_one line 339
  35. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_empty line 344
  36. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_univ line 351
  37. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_antitone line 357
  38. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_insert line 363
  39. theorem OAI.DFVSGames.Foundations.Games.Game.selectedSuccess_insert_eq_zero line 375
  40. theorem OAI.DFVSGames.Foundations.Information.gameLaw_isProbability line 397
  41. def OAI.DFVSGames.Foundations.Information.toGameLaw line 400
  42. def OAI.DFVSGames.Foundations.Information.gameLawEquiv line 405
  43. theorem OAI.DFVSGames.Foundations.Information.totalVariation_gameLaw line 411
  44. def OAI.DFVSGames.Foundations.Information.gameConditionalKernel line 414
  45. theorem OAI.DFVSGames.Foundations.Information.gameConditionalKernel_recombine line 420
  46. def OAI.DFVSGames.Foundations.Information.gameConditionalProduct line 426
  47. theorem OAI.DFVSGames.Foundations.Information.gameConditionalProduct_weight line 433
  48. theorem OAI.DFVSGames.Foundations.Information.gameCondition_weight line 439
  49. theorem OAI.DFVSGames.Foundations.Information.gameCondition_relativeEntropy_le line 446
  50. theorem OAI.DFVSGames.Foundations.Repetition.totalVariation_triangle line 473
  51. def OAI.DFVSGames.Foundations.Repetition.conditionWeights line 484
  52. theorem OAI.DFVSGames.Foundations.Repetition.conditionWeights_isProbability line 487
  53. theorem OAI.DFVSGames.Foundations.Repetition.totalVariation_condition_le line 504
  54. theorem OAI.DFVSGames.Foundations.Repetition.totalVariation_condition_half_le line 527
  55. theorem OAI.DFVSGames.Foundations.Repetition.totalVariation_append_kernel line 533
  56. def OAI.DFVSGames.Foundations.Repetition.kernelPushforward line 546
  57. theorem OAI.DFVSGames.Foundations.Repetition.totalVariation_kernelPushforward_le line 549
  58. theorem OAI.DFVSGames.Foundations.Information.totalVariation_joint_common_weights line 575
  59. theorem OAI.DFVSGames.Foundations.Information.totalVariation_joint_common_kernel line 586
  60. theorem OAI.DFVSGames.Foundations.Information.totalVariation_condition_le line 596
  61. theorem OAI.DFVSGames.Foundations.Information.weighted_coordinate_sum_sq_le line 615
  62. theorem OAI.DFVSGames.Foundations.Repetition.min_half_formula_inline_Overlap line 655
  63. theorem OAI.DFVSGames.Foundations.Repetition.sum_min_one_sub_tv line 663
  64. theorem OAI.DFVSGames.Foundations.Repetition.discount_le_self_inline_Overlap line 672
  65. theorem OAI.DFVSGames.Foundations.Repetition.discount_loss_le_mul_inline_Overlap line 677
  66. def OAI.DFVSGames.Foundations.Repetition.discountedCommonMass line 687
  67. theorem OAI.DFVSGames.Foundations.Repetition.discounted_common_mass_bounds line 691
  68. def OAI.DFVSGames.Foundations.Repetition.diagonalWeights line 751
  69. theorem OAI.DFVSGames.Foundations.Repetition.diagonalWeights_isProbability line 756
  70. theorem OAI.DFVSGames.Foundations.Repetition.diagonal_overlap_identity line 767
  71. theorem OAI.DFVSGames.Foundations.Repetition.diagonal_sampler_totalVariation_le line 792