OAI/Probability/SpanningForest/PosteriorIndependentExtension.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.Observation.fieldRectangles line 12
2. theorem OAI.Problem336.Observation.fieldRectangles_pi line 15
3. theorem OAI.Problem336.Observation.generateFrom_fieldRectangles line 23
4. theorem OAI.Problem336.Observation.setIntegral_eq_on_sup_of_rectangles line 38
5. theorem OAI.Problem336.Observation.setIntegral_of_independent_field line 60
6. theorem OAI.Problem336.Observation.condExp_sup_independent line 72
7. theorem OAI.Problem336.Observation.condExp_pair_of_indep line 101
8. theorem OAI.Problem336.Observation.comap_eq_of_mutual_reconstruction line 121
9. theorem OAI.Problem336.Observation.condExp_reconstructed_observation line 131