OAI/Computability/DepthThree/RestrictionCorrelation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.narrowTests line 18
  2. theorem OAI.DepthThreeLowerBound.mem_narrowTests_iff line 22
  3. theorem OAI.DepthThreeLowerBound.eval_mem_narrowTests line 27
  4. theorem OAI.DepthThreeLowerBound.narrowTests_true_mem line 31
  5. theorem OAI.DepthThreeLowerBound.narrowTests_false_mem line 39
  6. theorem OAI.DepthThreeLowerBound.narrowTests_nonempty line 47
  7. def OAI.DepthThreeLowerBound.corr line 50
  8. theorem OAI.DepthThreeLowerBound.abs_table_corr_le line 54
  9. theorem OAI.DepthThreeLowerBound.abs_corr_le line 59
  10. theorem OAI.DepthThreeLowerBound.abs_mean_le_corr line 64
  11. theorem OAI.DepthThreeLowerBound.corr_nonneg line 68
  12. theorem OAI.DepthThreeLowerBound.corr_le_of_forall line 71
  13. theorem OAI.DepthThreeLowerBound.corr_attained line 80
  14. theorem OAI.DepthThreeLowerBound.corr_le_abs_mean line 88
  15. theorem OAI.DepthThreeLowerBound.corr_linearCombination_identity line 98
  16. theorem OAI.DepthThreeLowerBound.abs_corr_linearCombination_le line 114
  17. theorem OAI.DepthThreeLowerBound.abs_corr_convex_mixture_le line 131
  18. theorem OAI.DepthThreeLowerBound.abs_corr_uniform_mixture_le line 144