OAI/Probability/SpanningForest/CylinderKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.CylinderKernel.cylinder line 13
2. def OAI.Problem336.CylinderKernel.cylinders line 16
3. lemma OAI.Problem336.CylinderKernel.isPiSystem_cylinders line 19
4. lemma OAI.Problem336.CylinderKernel.generateFrom_cylinders line 28
5. theorem OAI.Problem336.CylinderKernel.measurable_probabilityMeasure_of_cylinders line 49
6. theorem OAI.Problem336.CylinderKernel.exists_measurable_probabilityMeasure_of_cylinder_limits line 62
7. def OAI.Problem336.CylinderKernel.positiveCylinders line 80
8. lemma OAI.Problem336.CylinderKernel.isPiSystem_positiveCylinders line 83
9. lemma OAI.Problem336.CylinderKernel.generateFrom_positiveCylinders line 90
10. theorem OAI.Problem336.CylinderKernel.measurable_probabilityMeasure_of_positiveCylinders line 113
11. theorem OAI.Problem336.CylinderKernel.exists_measurable_weakLimit_of_positiveCylinder_limits line 126