OAI/Computability/PerfectCompleteness/Sampling/OriginalUsefulPairLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalUsefulPairLaw.product_mixture_pushforward line 20
  2. theorem OAI.PerfectCompleteness.OriginalUsefulPairLaw.nested_sigma_product_pushforward line 35
  3. theorem OAI.PerfectCompleteness.OriginalUsefulPairLaw.transportPair_law line 62
  4. theorem OAI.PerfectCompleteness.OriginalUsefulPairLaw.record_fresh_pair_law line 77
  5. abbrev OAI.PerfectCompleteness.OriginalUsefulPairLaw.Descriptor line 123
  6. def OAI.PerfectCompleteness.OriginalUsefulPairLaw.externalLaw line 130
  7. def OAI.PerfectCompleteness.OriginalUsefulPairLaw.background line 137
  8. def OAI.PerfectCompleteness.OriginalUsefulPairLaw.scalarLaw line 142
  9. theorem OAI.PerfectCompleteness.OriginalUsefulPairLaw.useful_pairLaw_eq_mixture line 149
  10. theorem OAI.PerfectCompleteness.OriginalUsefulPairLaw.actual_pair_law line 173