OAI/Computability/DirectedFeedback/Games/ProductLaw.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Clean.ProductLaw.splitCoordinates line 17
  2. theorem OAI.DFVSGames.Clean.ProductLaw.table_split line 21
  3. theorem OAI.DFVSGames.Clean.ProductLaw.probability_product_and line 45
  4. theorem OAI.DFVSGames.Clean.ProductLaw.probability_product_right line 62
  5. theorem OAI.DFVSGames.Clean.ProductLaw.table_inside_outside line 67
  6. theorem OAI.DFVSGames.Clean.ProductLaw.table_outside line 78
  7. theorem OAI.DFVSGames.Clean.ProductLaw.conditioned_inside line 84
  8. theorem OAI.DFVSGames.Clean.ProductLaw.seeded_inside_outside line 102
  9. theorem OAI.DFVSGames.Clean.ProductLaw.conditioned_seed_inside line 122
  10. theorem OAI.DFVSGames.Clean.ProductLaw.table_reindex line 137
  11. theorem OAI.DFVSGames.Clean.ProductLaw.conditioned_incidence_reindex line 146
  12. theorem OAI.DFVSGames.Clean.ProductLaw.conditioned_incidence_distribution line 173
  13. theorem OAI.DFVSGames.Clean.ProductLaw.clean_mask_independent line 205
  14. def OAI.DFVSGames.Clean.WeightedPartition.fibre line 224
  15. theorem OAI.DFVSGames.Clean.WeightedPartition.sum_fibre_inter line 227
  16. theorem OAI.DFVSGames.Clean.WeightedPartition.sum_fibre_bound line 238
  17. theorem OAI.DFVSGames.Clean.WeightedPartition.probability_le_conditional_bounds line 251
  18. theorem OAI.DFVSGames.Clean.WeightedPartition.probability_le_of_conditional_le line 267
  19. instance OAI.DFVSGames.Soundness.ConditionalSimulation.firstInputFintype line 288
  20. instance OAI.DFVSGames.Soundness.ConditionalSimulation.secondInputFintype line 297
  21. def OAI.DFVSGames.Soundness.ConditionalSimulation.incidenceGame line 307
  22. def OAI.DFVSGames.Soundness.ConditionalSimulation.actualLocalSimulation line 312
  23. theorem OAI.DFVSGames.Soundness.ConditionalSimulation.actual_conditioned_strategy_success_le_repeated_value line 350
  24. theorem OAI.DFVSGames.Soundness.ConditionalGameLaw.uniform_probability_decide line 385
  25. abbrev OAI.DFVSGames.Soundness.ConditionalGameLaw.OuterStrategy line 403
  26. def OAI.DFVSGames.Soundness.ConditionalGameLaw.actualWin line 407
  27. def OAI.DFVSGames.Soundness.ConditionalGameLaw.conditionedWinProbability line 413
  28. def OAI.DFVSGames.Soundness.ConditionalGameLaw.reconstructedEvent line 423
  29. theorem OAI.DFVSGames.Soundness.ConditionalGameLaw.actualWin_iff_reconstructedEvent line 435
  30. theorem OAI.DFVSGames.Soundness.ConditionalGameLaw.conditionedWinProbability_eq_fresh line 452
  31. def OAI.DFVSGames.Soundness.ConditionalGameLaw.incidenceLaw line 474
  32. theorem OAI.DFVSGames.Soundness.ConditionalGameLaw.reconstructed_success_eq_fresh_average line 477
  33. theorem OAI.DFVSGames.Soundness.ConditionalGameLaw.conditioned_probability_le_repeated_value line 512
  34. def OAI.DFVSGames.Clean.UpperBound.fixedAdviceSuccess line 545
  35. theorem OAI.DFVSGames.Clean.UpperBound.reference_of_positive_inline_UpperBound line 553
  36. theorem OAI.DFVSGames.Clean.UpperBound.conditioned_success_le_repeated_value_with_reference line 571
  37. theorem OAI.DFVSGames.Clean.UpperBound.conditioned_success_le_repeated_value line 629
  38. theorem OAI.DFVSGames.Clean.UpperBound.fixed_advice_success_le_repeated_value line 650
  39. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.pushforward_eq_of_agree_on_support line 675
  40. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.product_pushforward line 690
  41. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.table_row_weight_ne_zero line 707
  42. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.table_repair_pushforward line 717
  43. abbrev OAI.DFVSGames.Foundations.Games.KernelSampling.Seed line 734
  44. def OAI.DFVSGames.Foundations.Games.KernelSampling.readLeft line 736
  45. def OAI.DFVSGames.Foundations.Games.KernelSampling.readRight line 737
  46. def OAI.DFVSGames.Foundations.Games.KernelSampling.seedLaw line 739
  47. theorem OAI.DFVSGames.Foundations.Games.KernelSampling.read_joint_pushforward line 746
  48. theorem OAI.DFVSGames.Foundations.Games.KernelSampling.repaired_joint_pushforward line 759
  49. def OAI.DFVSGames.Foundations.Games.KernelSampling.completedLeft line 779
  50. def OAI.DFVSGames.Foundations.Games.KernelSampling.completedRight line 783
  51. theorem OAI.DFVSGames.Foundations.Games.KernelSampling.completedLeft_coordinate line 787
  52. theorem OAI.DFVSGames.Foundations.Games.KernelSampling.completedRight_coordinate line 791
  53. theorem OAI.DFVSGames.Foundations.Games.KernelSampling.update_eq_of_coordinate_inline_KernelSampling line 795
  54. theorem OAI.DFVSGames.Foundations.Games.KernelSampling.completed_joint_pushforward line 800