OAI/Computability/BinPacking/Games/LocalSimulation.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGames.Foundations.Repetition.totalVariation_triangle line 18
  2. def OAI.BinPackingGames.Foundations.Repetition.conditionWeights line 29
  3. theorem OAI.BinPackingGames.Foundations.Repetition.conditionWeights_isProbability line 32
  4. theorem OAI.BinPackingGames.Foundations.Repetition.totalVariation_condition_le line 49
  5. theorem OAI.BinPackingGames.Foundations.Repetition.totalVariation_condition_half_le line 72
  6. theorem OAI.BinPackingGames.Foundations.Repetition.totalVariation_append_kernel line 79
  7. def OAI.BinPackingGames.Foundations.Repetition.kernelPushforward line 92
  8. theorem OAI.BinPackingGames.Foundations.Repetition.totalVariation_kernelPushforward_le line 95
  9. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.pushforward_eq_of_agree_on_support line 120
  10. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.product_pushforward line 135
  11. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.table_row_weight_ne_zero line 152
  12. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.table_repair_pushforward line 162
  13. abbrev OAI.BinPackingGames.Foundations.Games.KernelSampling.Seed line 179
  14. def OAI.BinPackingGames.Foundations.Games.KernelSampling.readLeft line 181
  15. def OAI.BinPackingGames.Foundations.Games.KernelSampling.readRight line 182
  16. def OAI.BinPackingGames.Foundations.Games.KernelSampling.seedLaw line 184
  17. theorem OAI.BinPackingGames.Foundations.Games.KernelSampling.read_joint_pushforward line 191
  18. theorem OAI.BinPackingGames.Foundations.Games.KernelSampling.repaired_joint_pushforward line 204
  19. def OAI.BinPackingGames.Foundations.Games.KernelSampling.completedLeft line 224
  20. def OAI.BinPackingGames.Foundations.Games.KernelSampling.completedRight line 228
  21. theorem OAI.BinPackingGames.Foundations.Games.KernelSampling.completedLeft_coordinate line 232
  22. theorem OAI.BinPackingGames.Foundations.Games.KernelSampling.completedRight_coordinate line 236
  23. theorem OAI.BinPackingGames.Foundations.Games.KernelSampling.update_eq_of_coordinate line 240
  24. theorem OAI.BinPackingGames.Foundations.Games.KernelSampling.completed_joint_pushforward line 245
  25. theorem OAI.BinPackingGames.Foundations.Repetition.min_half_formula line 271
  26. theorem OAI.BinPackingGames.Foundations.Repetition.sum_min_one_sub_tv line 279
  27. theorem OAI.BinPackingGames.Foundations.Repetition.discount_le_self line 288
  28. theorem OAI.BinPackingGames.Foundations.Repetition.discount_loss_le_mul line 293
  29. def OAI.BinPackingGames.Foundations.Repetition.discountedCommonMass line 303
  30. theorem OAI.BinPackingGames.Foundations.Repetition.discounted_common_mass_bounds line 307
  31. def OAI.BinPackingGames.Foundations.Repetition.diagonalWeights line 367
  32. theorem OAI.BinPackingGames.Foundations.Repetition.diagonalWeights_isProbability line 372
  33. theorem OAI.BinPackingGames.Foundations.Repetition.diagonal_overlap_identity line 383
  34. theorem OAI.BinPackingGames.Foundations.Repetition.diagonal_sampler_totalVariation_le line 408
  35. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.weight_eq_probability_singleton line 473
  36. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.pushforward_comp line 478
  37. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.transport_eq_pushforward line 486
  38. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.expectation_pushforward line 494
  39. theorem OAI.BinPackingGames.Foundations.Games.FiniteDistribution.pushforward_mixture line 503
  40. def OAI.BinPackingGames.Foundations.Repetition.TraceSeed line 521
  41. instance OAI.BinPackingGames.Foundations.Repetition.traceSeedFintype line 525
  42. instance OAI.BinPackingGames.Foundations.Repetition.traceSeedUniqueZero line 530
  43. def OAI.BinPackingGames.Foundations.Repetition.traceList line 533
  44. def OAI.BinPackingGames.Foundations.Repetition.traceSeedLaw line 537
  45. theorem OAI.BinPackingGames.Foundations.Repetition.traceSeedLaw_expectation line 543
  46. def OAI.BinPackingGames.Foundations.Repetition.sharedOutputLaw line 560
  47. theorem OAI.BinPackingGames.Foundations.Repetition.sharedOutputLaw_weight line 568
  48. def OAI.BinPackingGames.Foundations.Repetition.samplerLocal line 586
  49. def OAI.BinPackingGames.Foundations.Repetition.samplerOutputLaw line 592
  50. theorem OAI.BinPackingGames.Foundations.Repetition.probability_weight_le_one line 599
  51. theorem OAI.BinPackingGames.Foundations.Repetition.samplerOutputLaw_diagonal line 605
  52. theorem OAI.BinPackingGames.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 636
  53. theorem OAI.BinPackingGames.Foundations.Repetition.samplerOutputLaw_totalVariation line 656
  54. theorem OAI.BinPackingGames.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 678
  55. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.mixture_pushforward_base line 702
  56. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.product_pushforward_eq_mixture_right line 709
  57. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.product_product_pushforward_eq_mixture line 726
  58. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.mixture_totalVariation_le line 738
  59. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.diagonalLaw line 752
  60. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.diagonalLaw_eq_pushforward line 756
  61. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.diagonalLaw_mixture line 770
  62. abbrev OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.Seed line 783
  63. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.seedLaw line 786
  64. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.left line 791
  65. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.right line 794
  66. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.completionKernel line 797
  67. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.outputLaw line 802
  68. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_product_pushforward line 809
  69. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_mixture line 820
  70. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.diagonalLaw_completion_mixture line 849
  71. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.outputLaw_totalVariation_le line 856
  72. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateLeft line 873
  73. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateRight line 877
  74. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateLeft_preserves line 883
  75. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateRight_preserves line 890
  76. def OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw line 895
  77. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_mixture line 903
  78. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_outputLaw line 938
  79. theorem OAI.BinPackingGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_totalVariation_le line 948
  80. theorem OAI.BinPackingGames.Foundations.Repetition.coordinate_probability_le_value_of_local_completion line 972