OAI/Computability/PerfectCompleteness/Sampling/RationalFiniteLawLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.RationalFiniteLaw.RationalLaw line 18
  2. def OAI.PerfectCompleteness.RationalFiniteLaw.uniform line 24
  3. def OAI.PerfectCompleteness.RationalFiniteLaw.pi line 37
  4. def OAI.PerfectCompleteness.RationalFiniteLaw.product line 51
  5. def OAI.PerfectCompleteness.RationalFiniteLaw.sigma line 64
  6. def OAI.PerfectCompleteness.RationalFiniteLaw.transport line 84
  7. theorem OAI.PerfectCompleteness.RationalFiniteLaw.real_positive line 92
  8. def OAI.PerfectCompleteness.RecursiveSamplerBiasProducts.pairTapeEquiv line 107
  9. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasProducts.pairTape_law line 123
  10. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasProducts.expectation_pairs line 137
  11. theorem OAI.PerfectCompleteness.RecursiveSamplerBiasProducts.expectation_product_mul line 151
  12. theorem OAI.PerfectCompleteness.FiniteProduct.pushforward_map line 179
  13. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward_id line 197
  14. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.product_pushforward_snd line 204