OAI/Probability/RadialTransition/StarIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialTransition.measurableSet_nearCube line 11
2. lemma OAI.RadialTransition.nearCube_translate line 17
3. lemma OAI.RadialTransition.volume_nearCube line 24
4. lemma OAI.RadialTransition.nearMask_self line 28
5. lemma OAI.RadialTransition.lintegral_nearMask_prod line 33
6. lemma OAI.RadialTransition.lintegral_rootStar line 45
7. lemma OAI.RadialTransition.lintegral_starWeight line 70