OAI/Combinatorics/Progressions/Probability/RelativeSliceFiniteLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.ResidueBoxSlice.fiberIntegerPoint_mem_integerBox line 18
2. theorem OAI.Erdos3.ResidueBoxSlice.fiberIntegerPoint_injective line 32
3. def OAI.Erdos3.ResidueBoxSlice.fiberPointInBox line 48
4. def OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw line 54
5. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_mean line 63
6. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_weight line 73
7. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_score line 84
8. theorem OAI.Erdos3.RelativePatchSliceConclusion.exists_fiber_law line 106
9. theorem OAI.Erdos3.RelativePatchSliceConclusion.exists_fiber_law_with_slice line 138