OAI/Probability/SKBarriers/Calculus/CubeMeasures.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SK.Analytic.parameterMeasurable line 19
2. instance OAI.SK.Analytic.parameterBorel line 23
3. instance OAI.SK.Analytic.parameterSecondCountable line 27
4. def OAI.SK.Analytic.fiberMeasure line 31
5. instance OAI.SK.Analytic.fiberSigmaFinite line 35
6. def OAI.SK.Analytic.cubeMeasure line 39
7. instance OAI.SK.Analytic.cubeFiniteMeasure line 43
8. def OAI.SK.Analytic.cubeSupport line 48
9. theorem OAI.SK.Analytic.cubeSupport_compact line 52
10. theorem OAI.SK.Analytic.ae_mem_cubeSupport line 57
11. theorem OAI.SK.Analytic.integrable_cubeMeasure line 67
12. theorem OAI.SK.Analytic.cubeIntegral_eq_measureIntegral line 74
13. def OAI.SK.Analytic.cubeSet line 87
14. theorem OAI.SK.Analytic.cubeSet_measurable line 91
15. theorem OAI.SK.Analytic.cubeMeasure_eq_restrict line 96