OAI/Probability/SphericalField/Cascade/FocusedShapes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SphericalPerceptron.focusedShapeProbability line 17
2. def OAI.SphericalPerceptron.focusedShapeNumerator line 27
3. lemma OAI.SphericalPerceptron.focusedShapeProbability_cons line 33
4. lemma OAI.SphericalPerceptron.markedBlockProbability_map_measurable line 44
5. lemma OAI.SphericalPerceptron.focusedShapeProbability_measurable line 52
6. lemma OAI.SphericalPerceptron.focusedShapeNumerator_pos line 78
7. theorem OAI.SphericalPerceptron.focusedShapeProbability_integral line 103
8. lemma OAI.SphericalPerceptron.descendant_transform_independent line 187
9. lemma OAI.SphericalPerceptron.stableIntensity_normalized_mark_projection line 195
10. lemma OAI.SphericalPerceptron.stableIntensity_descendant_transform line 207