OAI/Combinatorics/SumProduct/Alignment/RoughArray02.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RoughArrayFace.source_face_translation line 29
2. def OAI.RoughArrayFace.actualData line 73
3. theorem OAI.RoughArrayFace.source_raw_array_own_face_decay line 100
4. def OAI.RoughArrayCoordinates.affine line 176
5. def OAI.RoughArrayCoordinates.endpoint line 178
6. lemma OAI.RoughArrayCoordinates.coordinate_injective line 189
7. lemma OAI.RoughArrayCoordinates.mem_physical line 197
8. lemma OAI.RoughArrayCoordinates.affine_residue_iff line 203
9. lemma OAI.RoughArrayCoordinates.physical_image line 210
10. theorem OAI.RoughArrayCoordinates.mean_affine_nested line 257