OAI/Computability/DepthThree/RestrictionTails.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.restrictionAvg_pow_card_live line 20
  2. theorem OAI.DepthThreeLowerBound.restrictionAvg_two_pow_live line 36
  3. theorem OAI.DepthThreeLowerBound.restrictionAvg_two_neg_pow_live line 44
  4. theorem OAI.DepthThreeLowerBound.one_add_pow_le_exp line 51
  5. theorem OAI.DepthThreeLowerBound.one_sub_half_pow_le_exp line 58
  6. theorem OAI.DepthThreeLowerBound.lower_tail_exponent line 67
  7. theorem OAI.DepthThreeLowerBound.upper_tail_exponent line 76
  8. theorem OAI.DepthThreeLowerBound.restrictionAvg_lower_tail line 85
  9. theorem OAI.DepthThreeLowerBound.restrictionAvg_upper_tail line 112
  10. theorem OAI.DepthThreeLowerBound.restrictionAvg_outside_window line 139