OAI/Computability/DirectedFeedback/Games/ProfileCorrection.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal line 12
  2. theorem OAI.DFVSGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_isProbability line 15
  3. theorem OAI.DFVSGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_first line 26
  4. theorem OAI.DFVSGames.Foundations.Repetition.ProfileCorrection.totalVariation_triangle line 31
  5. theorem OAI.DFVSGames.Foundations.Repetition.ProfileCorrection.left_profile_correction line 40
  6. def OAI.DFVSGames.Foundations.Repetition.revealEndpoint line 94
  7. def OAI.DFVSGames.Foundations.Repetition.revealLaw line 97
  8. theorem OAI.DFVSGames.Foundations.Repetition.revealLaw_weight line 102
  9. def OAI.DFVSGames.Foundations.Repetition.revealFirstLaw line 112
  10. theorem OAI.DFVSGames.Foundations.Repetition.revealFirstLaw_weight line 117
  11. def OAI.DFVSGames.Foundations.Repetition.revealFallback line 121
  12. def OAI.DFVSGames.Foundations.Repetition.revealProfile line 127
  13. theorem OAI.DFVSGames.Foundations.Repetition.revealProfile_inl_support line 131
  14. theorem OAI.DFVSGames.Foundations.Repetition.revealProfile_inr_support line 143
  15. def OAI.DFVSGames.Foundations.Repetition.revealInputLaw line 155
  16. theorem OAI.DFVSGames.Foundations.Repetition.revealInputLaw_weight line 158
  17. theorem OAI.DFVSGames.Foundations.Repetition.reveal_profile_recombination line 164
  18. theorem OAI.DFVSGames.Foundations.Repetition.reveal_profile_inl_recombination line 171
  19. theorem OAI.DFVSGames.Foundations.Repetition.reveal_profile_inr_recombination line 178
  20. theorem OAI.DFVSGames.Foundations.Repetition.revealInputLaw_inl line 185
  21. theorem OAI.DFVSGames.Foundations.Repetition.revealInputLaw_inr line 194
  22. theorem OAI.DFVSGames.Foundations.Repetition.revealProfile_inl_diagonal line 201
  23. theorem OAI.DFVSGames.Foundations.Repetition.revealProfile_inr_diagonal line 223
  24. theorem OAI.DFVSGames.Foundations.Repetition.revealLaw_sum_left line 249
  25. theorem OAI.DFVSGames.Foundations.Repetition.revealLaw_sum_right line 254
  26. theorem OAI.DFVSGames.Foundations.Repetition.revealLaw_forget line 259
  27. theorem OAI.DFVSGames.Foundations.Repetition.reveal_product_factorization line 268
  28. theorem OAI.DFVSGames.Foundations.Repetition.reveal_product_forget line 278
  29. theorem OAI.DFVSGames.Foundations.Repetition.reveal_product_expectation line 295
  30. def OAI.DFVSGames.Foundations.Information.hellingerSquared line 318
  31. theorem OAI.DFVSGames.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 321
  32. theorem OAI.DFVSGames.Foundations.Information.hellingerSquared_le_relativeEntropy line 346
  33. theorem OAI.DFVSGames.Foundations.Information.totalVariation_sq_le_hellingerSquared line 354
  34. theorem OAI.DFVSGames.Foundations.Information.totalVariation_sq_le_relativeEntropy line 379
  35. theorem OAI.DFVSGames.Foundations.Information.posterior_totalVariation_sq_le_log line 385
  36. def OAI.DFVSGames.Foundations.Information.coordinateMarginal line 401
  37. def OAI.DFVSGames.Foundations.Information.independentProduct line 405
  38. theorem OAI.DFVSGames.Foundations.Information.coordinateMarginal_isProbability line 407
  39. theorem OAI.DFVSGames.Foundations.Information.point_le_coordinateMarginal line 421
  40. theorem OAI.DFVSGames.Foundations.Information.marginal_expectation line 429
  41. theorem OAI.DFVSGames.Foundations.Information.independentProduct_isProbability line 438
  42. theorem OAI.DFVSGames.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 446
  43. theorem OAI.DFVSGames.Foundations.Information.relativeEntropy_independent_reference line 454
  44. theorem OAI.DFVSGames.Foundations.Information.coordinate_relativeEntropy_sum_le line 497
  45. theorem OAI.DFVSGames.Foundations.Information.coordinate_totalVariation_sq_sum_le line 507
  46. theorem OAI.DFVSGames.Foundations.Information.posterior_coordinate_supportedBy line 516
  47. theorem OAI.DFVSGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 531
  48. theorem OAI.DFVSGames.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 544
  49. theorem OAI.DFVSGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 570
  50. theorem OAI.DFVSGames.Foundations.Information.normalize_isProbability line 588
  51. theorem OAI.DFVSGames.Foundations.Information.relativeEntropy_normalize_right line 596
  52. theorem OAI.DFVSGames.Foundations.Information.neg_relativeEntropy_le_log_mass line 610
  53. theorem OAI.DFVSGames.Foundations.Information.posterior_weighted_log_inverse_le line 620
  54. def OAI.DFVSGames.Foundations.Information.posteriorOrOriginal line 657
  55. theorem OAI.DFVSGames.Foundations.Information.posteriorOrOriginal_isProbability line 662
  56. theorem OAI.DFVSGames.Foundations.Information.mass_mul_posteriorOrOriginal line 673
  57. theorem OAI.DFVSGames.Foundations.Information.weighted_coordinate_posterior_recombine line 693
  58. theorem OAI.DFVSGames.Foundations.Information.side_information_bound line 715
  59. theorem OAI.DFVSGames.Foundations.Information.finite_side_information_bound line 783