OAI/Computability/PerfectCompleteness/Foundations/DummyEliminationWeighted.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.DummyElimination.Slice.uniform_probability_card line 17
  2. theorem OAI.PerfectCompleteness.DummyElimination.Slice.expectation_condition line 31
  3. def OAI.PerfectCompleteness.DummyElimination.Slice.dummyLikelihood line 49
  4. def OAI.PerfectCompleteness.DummyElimination.Slice.dummyConstant line 52
  5. theorem OAI.PerfectCompleteness.DummyElimination.Slice.dummyConstant_pos line 56
  6. theorem OAI.PerfectCompleteness.DummyElimination.Slice.dummyLikelihood_eq_card line 61
  7. theorem OAI.PerfectCompleteness.DummyElimination.Slice.dummyLikelihood_eq line 68
  8. theorem OAI.PerfectCompleteness.DummyElimination.Slice.dummy_restricted_expectation line 79
  9. theorem OAI.PerfectCompleteness.DummyElimination.Slice.weighted_restricted_expectation line 95
  10. theorem OAI.PerfectCompleteness.DummyElimination.Slice.padded_probability line 112
  11. theorem OAI.PerfectCompleteness.DummyElimination.Slice.padded_probability_pos_iff line 120
  12. theorem OAI.PerfectCompleteness.DummyElimination.Slice.padded_probability_pos line 128
  13. theorem OAI.PerfectCompleteness.DummyElimination.Slice.conditioned_expectation_projected line 135
  14. theorem OAI.PerfectCompleteness.DummyElimination.Slice.conditioned_probability_projected line 148