OAI/Computability/DepthThree/RestrictionProbability.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.liveSet line 16
  2. theorem OAI.DepthThreeLowerBound.mem_liveSet line 19
  3. def OAI.DepthThreeLowerBound.maskRestriction line 27
  4. theorem OAI.DepthThreeLowerBound.maskRestriction_live line 30
  5. theorem OAI.DepthThreeLowerBound.maskRestriction_fixed line 38
  6. theorem OAI.DepthThreeLowerBound.liveSet_maskRestriction line 46
  7. theorem OAI.DepthThreeLowerBound.fill_maskRestriction line 51
  8. theorem OAI.DepthThreeLowerBound.maskRestriction_fill line 60
  9. def OAI.DepthThreeLowerBound.restrictionCoordinates line 67
  10. theorem OAI.DepthThreeLowerBound.restrictionCoordinates_injective line 71
  11. theorem OAI.DepthThreeLowerBound.restrictionCoordinates_surjective line 88
  12. def OAI.DepthThreeLowerBound.restrictionCoordinatesEquiv line 94
  13. theorem OAI.DepthThreeLowerBound.restrictionCoordinatesEquiv_apply line 99
  14. theorem OAI.DepthThreeLowerBound.card_live_maskRestriction line 103
  15. theorem OAI.DepthThreeLowerBound.restrictionWeight_maskRestriction line 110
  16. theorem OAI.DepthThreeLowerBound.restriction_mask_joint_weight line 138
  17. theorem OAI.DepthThreeLowerBound.restriction_fill_joint_weight line 159
  18. theorem OAI.DepthThreeLowerBound.restrictionAvg_fill_coupling line 166
  19. theorem OAI.DepthThreeLowerBound.restrictionAvg_fill_reweight line 208
  20. theorem OAI.DepthThreeLowerBound.restrictionAvg_fill line 219
  21. theorem OAI.DepthThreeLowerBound.restrictionAvg_mask_sampler line 227