OAI/Probability/SpanningForest/WeightedTreeBorel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.WeightedTree.Field line 11
  2. def OAI.Problem336.WeightedTree.weight line 13
  3. def OAI.Problem336.WeightedTree.partition line 16
  4. def OAI.Problem336.WeightedTree.numerator line 19
  5. def OAI.Problem336.WeightedTree.inclusion line 23
  6. theorem OAI.Problem336.WeightedTree.weight_pos line 26
  7. theorem OAI.Problem336.WeightedTree.partition_nonneg line 29
  8. theorem OAI.Problem336.WeightedTree.partition_pos line 33
  9. theorem OAI.Problem336.WeightedTree.numerator_nonneg line 38
  10. theorem OAI.Problem336.WeightedTree.numerator_le_partition line 43
  11. theorem OAI.Problem336.WeightedTree.inclusion_mem_Icc line 49
  12. theorem OAI.Problem336.WeightedTree.measurable_weight line 57
  13. theorem OAI.Problem336.WeightedTree.measurable_partition line 61
  14. theorem OAI.Problem336.WeightedTree.measurable_numerator line 65
  15. theorem OAI.Problem336.WeightedTree.measurable_inclusion line 70
  16. theorem OAI.Problem336.WeightedTree.measurable_partition_joint line 74
  17. theorem OAI.Problem336.WeightedTree.measurable_inclusion_joint line 78
  18. def OAI.Problem336.WeightedTree.finiteField line 83
  19. theorem OAI.Problem336.WeightedTree.measurable_finiteField line 86
  20. theorem OAI.Problem336.WeightedTree.measurable_finiteField_joint line 99
  21. theorem OAI.Problem336.WeightedTree.measurable_finiteTilt_joint line 104
  22. def OAI.Problem336.WeightedTree.extendField line 112
  23. theorem OAI.Problem336.WeightedTree.extendField_apply line 115
  24. theorem OAI.Problem336.WeightedTree.measurable_extendField line 119
  25. theorem OAI.Problem336.WeightedTree.measurable_edgeFiniteTilt_joint line 128
  26. theorem OAI.Problem336.WeightedTree.inclusion_zero_field line 140
  27. theorem OAI.Problem336.WeightedTree.inclusion_zero_field_eq_ustCylinder line 147
  28. theorem OAI.Problem336.WeightedTree.ofReal_inclusion_zero_field line 153
  29. theorem OAI.Problem336.WeightedTree.inclusion_eq_zero_of_not_mem line 163
  30. theorem OAI.Problem336.WeightedTree.weight_image line 174