OAI/Combinatorics/Progressions/Probability/SymmetricCubeMeasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.symmetricCubeMeasure line 13
2. instance OAI.Erdos3.symmetricCubeMeasure_probability line 16
3. theorem OAI.Erdos3.symmetricCubeMeasure_zero line 20
4. theorem OAI.Erdos3.symmetricCubeMeasure_cons line 23
5. theorem OAI.Erdos3.symmetricCubeMeasure_sublevel_succ line 38
6. theorem OAI.Erdos3.symmetricCubeMeasure_sublevel_step line 48