OAI/Probability/SpanningForest/IntrinsicTreeDrift.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.GraphTreePosterior.innerMean line 13
  2. def OAI.Problem336.GraphTreePosterior.drift line 18
  3. theorem OAI.Problem336.GraphTreePosterior.innerMean_mem_Icc line 23
  4. theorem OAI.Problem336.GraphTreePosterior.drift_mem_Icc line 30
  5. theorem OAI.Problem336.GraphTreePosterior.measurable_innerMean line 37
  6. theorem OAI.Problem336.GraphTreePosterior.measurable_drift line 42
  7. theorem OAI.Problem336.GraphTreePosterior.innerMean_eq_of_tendsto line 47
  8. theorem OAI.Problem336.GraphTreePosterior.drift_response_of_finite line 52
  9. theorem OAI.Problem336.GraphTreePosterior.finiteBallMean_of_not_adj line 66
  10. theorem OAI.Problem336.GraphTreePosterior.drift_of_not_adj line 73
  11. theorem OAI.Problem336.GraphTreePosterior.measurable_drift_joint line 79
  12. theorem OAI.Problem336.GraphTreePosterior.measurable_drift_fixed line 84
  13. theorem OAI.Problem336.GraphTreePosterior.abs_drift_le_one line 94
  14. theorem OAI.Problem336.GraphTreePosterior.finiteBallMean_congr_on_edges line 99
  15. theorem OAI.Problem336.GraphTreePosterior.drift_congr_on_edges line 108