OAI/Probability/BinarySweep/Conditional/ConditionalAverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.conditionalGroupLaw line 15
2. lemma OAI.BinaryCoordinateSweeps.conditionalGroupLaw_nonneg line 19
3. lemma OAI.BinaryCoordinateSweeps.conditionalGroupLaw_sum line 27
4. lemma OAI.BinaryCoordinateSweeps.groupAverage_conditional line 36
5. lemma OAI.BinaryCoordinateSweeps.groupAverage_conditional_grid line 48
6. lemma OAI.BinaryCoordinateSweeps.conditionalOperator_groupAverage line 73
7. lemma OAI.BinaryCoordinateSweeps.conditionalMoment_evenMoment line 80