OAI/Computability/PerfectCompleteness/Reduction/FixedStoppedMeetingEquality.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.expectation_congr_on_support line 30
  2. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.nodeDirection_val_heq line 41
  3. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.familyMeetingProbability_eq_of_useful line 49
  4. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.flag_eq line 84
  5. abbrev OAI.PerfectCompleteness.FixedStoppedMeetingEquality.OriginalRaw line 96
  6. def OAI.PerfectCompleteness.FixedStoppedMeetingEquality.familyMeetingOnRaw line 101
  7. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.familyMeetingOnRaw_eq line 123
  8. def OAI.PerfectCompleteness.FixedStoppedMeetingEquality.nativeMeetingProbability line 185
  9. def OAI.PerfectCompleteness.FixedStoppedMeetingEquality.physicalMeetingProbability line 199
  10. def OAI.PerfectCompleteness.FixedStoppedMeetingEquality.cleanMeetingProbability line 209
  11. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.direction_heq line 226
  12. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.cleanMeetingProbability_eq_familyOnRaw line 252
  13. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.cleanMeetingProbability_eq_physical line 303
  14. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.cleanMeetingProbability_eq_native line 310
  15. abbrev OAI.PerfectCompleteness.FixedStoppedMeetingEquality.expectedMeeting line 328
  16. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.native_probability_eq_expectation line 336
  17. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.native_expectation_eq_cleanMeeting line 348
  18. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.physical_expectation_eq_expectedMeeting line 360
  19. theorem OAI.PerfectCompleteness.FixedStoppedMeetingEquality.meeting_probability_eq_expectedMeeting line 375