OAI/Probability/RadialTransition/CroppedCells.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.measurable_cellOf line 14
2. def OAI.RadialTransition.gridRegion line 19
3. lemma OAI.RadialTransition.measurableSet_gridRegion line 21
4. abbrev OAI.RadialTransition.CroppedCell line 24
5. def OAI.RadialTransition.croppedCellMeasure line 26
6. def OAI.RadialTransition.gridOrigin line 29
7. lemma OAI.RadialTransition.gridRegion_subset_box line 31
8. lemma OAI.RadialTransition.volume_gridRegion_le line 40
9. lemma OAI.RadialTransition.croppedCellMeasure_univ line 47
10. lemma OAI.RadialTransition.croppedCellMeasure_finite line 52
11. lemma OAI.RadialTransition.croppedCellMeasure_volume line 58
12. lemma OAI.RadialTransition.croppedCellMeasure_map line 65
13. lemma OAI.RadialTransition.croppedCell_diameter line 69
14. lemma OAI.RadialTransition.croppedCell_partition line 73