OAI/Computability/DepthThree/FiniteProbability.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.Restriction line 19
  2. abbrev OAI.DepthThreeLowerBound.Live line 20
  3. def OAI.DepthThreeLowerBound.fill line 22
  4. theorem OAI.DepthThreeLowerBound.fill_live line 25
  5. theorem OAI.DepthThreeLowerBound.fill_fixed line 29
  6. def OAI.DepthThreeLowerBound.finiteAvg line 33
  7. theorem OAI.DepthThreeLowerBound.finiteAvg_congr line 40
  8. theorem OAI.DepthThreeLowerBound.finiteAvg_zero line 46
  9. theorem OAI.DepthThreeLowerBound.finiteAvg_add line 49
  10. theorem OAI.DepthThreeLowerBound.finiteAvg_sub line 53
  11. theorem OAI.DepthThreeLowerBound.finiteAvg_const_mul line 57
  12. theorem OAI.DepthThreeLowerBound.finiteAvg_mul_const line 63
  13. theorem OAI.DepthThreeLowerBound.finiteAvg_sum line 69
  14. theorem OAI.DepthThreeLowerBound.finiteAvg_nonneg line 75
  15. theorem OAI.DepthThreeLowerBound.finiteAvg_mono line 80
  16. theorem OAI.DepthThreeLowerBound.finiteAvg_abs_le line 85
  17. theorem OAI.DepthThreeLowerBound.finiteAvg_const line 92
  18. theorem OAI.DepthThreeLowerBound.finiteAvg_equiv line 98
  19. theorem OAI.DepthThreeLowerBound.finiteAvg_comm line 103
  20. theorem OAI.DepthThreeLowerBound.finiteAvg_product line 114
  21. theorem OAI.DepthThreeLowerBound.finiteAvg_pi_prod line 124
  22. def OAI.DepthThreeLowerBound.restrictionCoordinateWeight line 135
  23. def OAI.DepthThreeLowerBound.restrictionWeight line 139
  24. def OAI.DepthThreeLowerBound.restrictionAvg line 142
  25. theorem OAI.DepthThreeLowerBound.restrictionCoordinateWeight_sum line 146
  26. theorem OAI.DepthThreeLowerBound.restrictionCoordinateWeight_nonneg line 151
  27. theorem OAI.DepthThreeLowerBound.restrictionWeight_nonneg line 157
  28. theorem OAI.DepthThreeLowerBound.restrictionWeight_sum line 162
  29. theorem OAI.DepthThreeLowerBound.restrictionAvg_const line 169
  30. theorem OAI.DepthThreeLowerBound.restrictionAvg_nonneg line 173
  31. theorem OAI.DepthThreeLowerBound.restrictionAvg_mono line 179
  32. theorem OAI.DepthThreeLowerBound.restrictionAvg_add line 185
  33. theorem OAI.DepthThreeLowerBound.restrictionAvg_const_mul line 190
  34. theorem OAI.DepthThreeLowerBound.restrictionAvg_abs_le line 195