OAI/Probability/SpanningForest/AllPairIID.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.AllPairIID.raw line 16
  2. theorem OAI.Problem336.AllPairIID.measurable_coordinate_fixed line 19
  3. theorem OAI.Problem336.AllPairIID.measurable_raw_joint line 24
  4. theorem OAI.Problem336.AllPairIID.measurable_raw line 36
  5. theorem OAI.Problem336.AllPairIID.map_keys_raw line 41
  6. theorem OAI.Problem336.AllPairIID.map_raw line 52
  7. def OAI.Problem336.AllPairIID.uniformRule line 61
  8. theorem OAI.Problem336.AllPairIID.measurable_uniformRule line 65
  9. theorem OAI.Problem336.AllPairIID.measurable_uniformRule_uncurried line 74
  10. theorem OAI.Problem336.AllPairIID.measurable_uniformRule_fixed line 80
  11. theorem OAI.Problem336.AllPairIID.raw_relabel line 85
  12. theorem OAI.Problem336.AllPairIID.uniformRule_equivariant line 93
  13. theorem OAI.Problem336.AllPairIID.map_uniformRule line 106
  14. theorem OAI.Problem336.AllPairIID.uniformRule_law line 115
  15. theorem OAI.Problem336.AllPairIID.sampled_uniformRule_law line 127
  16. theorem OAI.Problem336.AllPairIID.exists_equivariant_all_pair_iid_sampler line 149