OAI/Probability/RadialTransition/ClusterWeights.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RadialTransition.configurationMultiset_card line 13
  2. lemma OAI.RadialTransition.configurationMultiset_sum_map line 18
  3. lemma OAI.RadialTransition.configurationMultiset_prod_map line 23
  4. def OAI.RadialTransition.nearCube line 28
  5. def OAI.RadialTransition.nearMask line 31
  6. def OAI.RadialTransition.regionMask line 33
  7. def OAI.RadialTransition.starWeight line 35
  8. def OAI.RadialTransition.emptyWeight line 38
  9. def OAI.RadialTransition.cellClusterWeight line 40
  10. lemma OAI.RadialTransition.measurable_regionMask line 43
  11. lemma OAI.RadialTransition.measurable_nearMask line 46
  12. lemma OAI.RadialTransition.measurable_multiset_prod line 55
  13. lemma OAI.RadialTransition.measurable_starWeight line 64
  14. lemma OAI.RadialTransition.measurable_emptyWeight line 93
  15. lemma OAI.RadialTransition.measurable_cellClusterWeight line 99