OAI/Combinatorics/SharpThreshold/Probability.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem313.boolReal_nonneg line 8
  2. theorem OAI.Problem313.boolReal_le_one line 11
  3. theorem OAI.Problem313.boolReal_sq line 14
  4. theorem OAI.Problem313.graphWeight_sum line 17
  5. theorem OAI.Problem313.graphWeight_nonneg line 25
  6. theorem OAI.Problem313.graphWeight_pos line 32
  7. theorem OAI.Problem313.graphMean_nonneg line 39
  8. theorem OAI.Problem313.graphMean_le_one line 46
  9. theorem OAI.Problem313.graphMean_mem_Icc line 56
  10. theorem OAI.Problem313.graphVariance_eq_mean_mul line 60
  11. theorem OAI.Problem313.boolReal_not line 78
  12. theorem OAI.Problem313.graphMean_not line 81
  13. theorem OAI.Problem313.graphMean_pos line 87
  14. theorem OAI.Problem313.graphMean_lt_one line 97
  15. theorem OAI.Problem313.graphMean_mem_Ioo line 105
  16. theorem OAI.Problem313.graphVariance_nonneg line 110
  17. theorem OAI.Problem313.graphVariance_le_quarter line 115
  18. theorem OAI.Problem313.edgeInfluence_nonneg line 120
  19. theorem OAI.Problem313.totalInfluence_nonneg line 129