OAI/Computability/PerfectCompleteness/Foundations/HeterogeneousPairAdvice.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.append_totalVariation line 20
  2. abbrev OAI.PerfectCompleteness.HeterogeneousPairAdvice.PairSample line 62
  3. abbrev OAI.PerfectCompleteness.HeterogeneousPairAdvice.AdviceSample line 64
  4. def OAI.PerfectCompleteness.HeterogeneousPairAdvice.appendLaw line 67
  5. def OAI.PerfectCompleteness.HeterogeneousPairAdvice.observe line 72
  6. def OAI.PerfectCompleteness.HeterogeneousPairAdvice.observedLaw line 75
  7. def OAI.PerfectCompleteness.HeterogeneousPairAdvice.referencePairLaw line 79
  8. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.observed_sigmaLaw line 87
  9. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.reference_observe_sigmaLaw line 104
  10. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.reference_observe_law line 125
  11. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.appendLaw_totalVariation line 136
  12. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.observed_totalVariation_le line 140
  13. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.observed_totalVariation_le_of_bound line 154
  14. theorem OAI.PerfectCompleteness.HeterogeneousPairAdvice.original_totalVariation_le_of_observed line 165