OAI/Combinatorics/SumProduct/Alignment/RoughPhysical01.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.RoughBadBlock.Block line 31
2. def OAI.RoughBadBlock.Block.affine line 59
3. def OAI.RoughBadBlock.Block.restrict line 99
4. theorem OAI.RoughBlockRationalization.rationalized_block line 131
5. lemma OAI.RoughPhysicalSelection.mem_physical line 196
6. lemma OAI.RoughPhysicalSelection.physical_image line 202
7. lemma OAI.RoughPhysicalSelection.physical_mean line 207
8. lemma OAI.RoughPhysicalSelection.affine_mod line 214
9. lemma OAI.RoughPhysicalSelection.affine_zero_one line 220
10. lemma OAI.RoughPhysicalSelection.physical_fiber_image line 226
11. lemma OAI.RoughPhysicalSelection.physical_fiber_mean line 266
12. lemma OAI.RoughPhysicalSelection.mean_congr line 277
13. theorem OAI.RoughPhysicalSelection.physical_frozen_selection line 294