OAI/Computability/DepthThree/MarkerMixture.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.markerSelected line 23
  2. theorem OAI.DepthThreeLowerBound.mem_markerSelected line 27
  3. def OAI.DepthThreeLowerBound.markerSample line 36
  4. theorem OAI.DepthThreeLowerBound.markerSample_eq_true line 40
  5. def OAI.DepthThreeLowerBound.markerBad line 45
  6. def OAI.DepthThreeLowerBound.markerActive line 48
  7. def OAI.DepthThreeLowerBound.markerObjects line 51
  8. theorem OAI.DepthThreeLowerBound.markerActive_nonempty line 54
  9. theorem OAI.DepthThreeLowerBound.markerObjects_subset line 64
  10. theorem OAI.DepthThreeLowerBound.markerSample_iff_first_marker line 76
  11. theorem OAI.DepthThreeLowerBound.marker_mixture_ratio line 114
  12. theorem OAI.DepthThreeLowerBound.markerSample_of_all_true line 135
  13. theorem OAI.DepthThreeLowerBound.markerSample_of_isEmpty line 141
  14. theorem OAI.DepthThreeLowerBound.marker_product_mixture_ratio line 147