OAI/Computability/PerfectCompleteness/Foundations/SourcePhysicalSourceSwapLemmas.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourcePhysicalSourceSwap.Questions line 24
  2. abbrev OAI.PerfectCompleteness.SourcePhysicalSourceSwap.Positions line 25
  3. abbrev OAI.PerfectCompleteness.SourcePhysicalSourceSwap.Raw line 26
  4. abbrev OAI.PerfectCompleteness.SourcePhysicalSourceSwap.ChildSample line 28
  5. theorem OAI.PerfectCompleteness.SourcePhysicalSourceSwap.outside_join line 32
  6. def OAI.PerfectCompleteness.SourcePhysicalSourceSwap.joinedExterior line 39
  7. theorem OAI.PerfectCompleteness.SourcePhysicalSourceSwap.joinedExterior_law line 50
  8. theorem OAI.PerfectCompleteness.SourcePhysicalSourceSwap.expectation_joinedExterior line 61
  9. theorem OAI.PerfectCompleteness.SourcePhysicalSourceSwap.expectation_swap line 74
  10. abbrev OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.Sources line 176
  11. abbrev OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.NativeArrays line 178
  12. def OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.modifiedLaw line 182
  13. def OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.stoppedLaw line 189
  14. theorem OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.conditional_variation line 194
  15. abbrev OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.Observation line 235
  16. def OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.sourceModifiedLaw line 238
  17. def OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.sourceStoppedLaw line 244
  18. theorem OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.source_variation line 248
  19. theorem OAI.PerfectCompleteness.SourcePhysicalStoppedComparison.probability_ge_sub line 260