OAI/Probability/BinarySweep/GridBounds/GridProjectedMoment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.GridSplit.junctionAverage line 24
2. def OAI.BinaryCoordinateSweeps.GridSplit.junctionFrame line 27
3. lemma OAI.BinaryCoordinateSweeps.GridSplit.junctionAverage_linear line 30
4. lemma OAI.BinaryCoordinateSweeps.GridSplit.junctionAverage_split line 35
5. lemma OAI.BinaryCoordinateSweeps.GridSplit.projection_commutes_column line 46
6. lemma OAI.BinaryCoordinateSweeps.GridSplit.junction_projected_moment line 53
7. theorem OAI.BinaryCoordinateSweeps.GridSplit.conditional_le_junction line 70
8. def OAI.BinaryCoordinateSweeps.Signed.typeF line 93
9. def OAI.BinaryCoordinateSweeps.Signed.blockLogSize line 95
10. lemma OAI.BinaryCoordinateSweeps.Signed.blockActive_card_exp line 98
11. theorem OAI.BinaryCoordinateSweeps.Signed.grouped_dense_bound line 109