OAI/Probability/SpanningForest/GraphTreePosterior.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.GraphTreePosterior.energy line 12
  2. def OAI.Problem336.GraphTreePosterior.weight line 17
  3. def OAI.Problem336.GraphTreePosterior.partition line 20
  4. def OAI.Problem336.GraphTreePosterior.numerator line 24
  5. def OAI.Problem336.GraphTreePosterior.mean line 29
  6. theorem OAI.Problem336.GraphTreePosterior.weight_pos line 32
  7. theorem OAI.Problem336.GraphTreePosterior.partition_nonneg line 35
  8. theorem OAI.Problem336.GraphTreePosterior.partition_pos line 39
  9. theorem OAI.Problem336.GraphTreePosterior.numerator_nonneg line 43
  10. theorem OAI.Problem336.GraphTreePosterior.numerator_le_partition line 47
  11. theorem OAI.Problem336.GraphTreePosterior.mean_mem_Icc line 54
  12. theorem OAI.Problem336.GraphTreePosterior.measurable_energy line 63
  13. theorem OAI.Problem336.GraphTreePosterior.measurable_weight line 77
  14. theorem OAI.Problem336.GraphTreePosterior.measurable_partition line 81
  15. theorem OAI.Problem336.GraphTreePosterior.measurable_numerator line 85
  16. theorem OAI.Problem336.GraphTreePosterior.measurable_mean line 89
  17. theorem OAI.Problem336.GraphTreePosterior.measurable_mean_joint line 93
  18. theorem OAI.Problem336.GraphTreePosterior.mean_zero line 100
  19. theorem OAI.Problem336.GraphTreePosterior.mean_of_not_mem line 105
  20. def OAI.Problem336.GraphTreePosterior.edgeCodes line 116
  21. theorem OAI.Problem336.GraphTreePosterior.mem_edgeCodes line 119
  22. theorem OAI.Problem336.GraphTreePosterior.measurable_edgeCodes line 122
  23. theorem OAI.Problem336.GraphTreePosterior.mean_congr_field line 124
  24. def OAI.Problem336.GraphTreePosterior.finiteBallMean line 135
  25. theorem OAI.Problem336.GraphTreePosterior.finiteBallMean_mem_Icc line 139
  26. theorem OAI.Problem336.GraphTreePosterior.measurable_finiteBallMean line 144
  27. theorem OAI.Problem336.GraphTreePosterior.eventually_mem_observedEdges line 164