OAI/Computability/PerfectCompleteness/Foundations/CutContinuationAveraging.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CutContinuationAveraging.sigmaLaw_pushforward line 17
  2. theorem OAI.PerfectCompleteness.CutContinuationAveraging.product_mixture_pushforward line 28
  3. theorem OAI.PerfectCompleteness.CutContinuationAveraging.sigma_product_observe line 43
  4. def OAI.PerfectCompleteness.CutContinuationAveraging.originalArrayLaw line 62
  5. theorem OAI.PerfectCompleteness.CutContinuationAveraging.observed_sourceLaw_eq_mixture line 68
  6. theorem OAI.PerfectCompleteness.CutContinuationAveraging.originalArrayLaw_eq line 90
  7. theorem OAI.PerfectCompleteness.CutContinuationAveraging.originalArrayLaw_eq_sigma line 107