OAI/Probability/RadialTransition/PartitionReplication.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RadialTransition.rawPartition_setIntegral line 14
  2. theorem OAI.RadialTransition.partitionOn_cube line 18
  3. theorem OAI.RadialTransition.partitionOn_nonneg line 28
  4. theorem OAI.RadialTransition.partitionOn_zero line 31
  5. theorem OAI.RadialTransition.rawPartition_mono line 35
  6. theorem OAI.RadialTransition.partitionOn_mono line 48
  7. def OAI.RadialTransition.translateSet line 53
  8. theorem OAI.RadialTransition.measurableSet_translate line 56
  9. theorem OAI.RadialTransition.orderedEnergy_add line 59
  10. theorem OAI.RadialTransition.rawPartition_translate line 63
  11. theorem OAI.RadialTransition.partitionOn_translate line 77
  12. theorem OAI.RadialTransition.partitionOn_biUnion_lower line 81
  13. theorem OAI.RadialTransition.sum_all_subsets_card line 122
  14. theorem OAI.RadialTransition.factorial_choose_cancel line 128
  15. theorem OAI.RadialTransition.partitionOn_union_convolution line 139