OAI/Probability/RadialTransition/MacroRegions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialTransition.macroRegion line 16
  2. def OAI.RadialTransition.macroOrigin line 18
  3. lemma OAI.RadialTransition.measurableSet_macroRegion line 20
  4. lemma OAI.RadialTransition.macroRegion_translate line 23
  5. lemma OAI.RadialTransition.volume_macroRegion line 50
  6. lemma OAI.RadialTransition.macroRegion_subset_halfCube line 54
  7. lemma OAI.RadialTransition.halfCube_macro_cover line 65
  8. lemma OAI.RadialTransition.halfCube_macro_union line 72
  9. def OAI.RadialTransition.regionMeasure line 79
  10. lemma OAI.RadialTransition.regionMeasure_map line 81
  11. lemma OAI.RadialTransition.regionMeasure_univ line 84
  12. lemma OAI.RadialTransition.regionMeasure_finite line 89
  13. lemma OAI.RadialTransition.macroRegion_partition line 92
  14. lemma OAI.RadialTransition.pairGrand_within line 110
  15. lemma OAI.RadialTransition.pairGrand_map line 114
  16. lemma OAI.RadialTransition.grandOn_halfCube line 125
  17. lemma OAI.RadialTransition.deletedPair_macro_factorization line 131