OAI/Combinatorics/SumProduct/Alignment/RoughFace01.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RoughProductRemoval.badProduct_zero_false line 28
2. lemma OAI.RoughProductRemoval.exceptionalProduct_succ_card line 38
3. theorem OAI.RoughProductRemoval.source_product_decay line 48
4. def OAI.RoughFaceShift.badFace line 134
5. def OAI.RoughFaceShift.exceptionalFace line 145
6. lemma OAI.RoughFaceShift.rectMean_natShift line 164
7. lemma OAI.RoughFaceShift.rectMean_intShift line 194
8. lemma OAI.RoughFaceShift.halfOpenLength_lower line 242
9. lemma OAI.RoughFaceShift.boxMean_translation line 249
10. lemma OAI.RoughFaceShift.residueMean_translation line 278