OAI/Combinatorics/SumProduct/Alignment/RoughSplit01.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RoughCommonKernelCover.common_kernel_cover line 31
2. theorem OAI.RoughCommonKernelDiscrepancy.source_common_kernel_discrepancy line 113
3. lemma OAI.RoughSplitBlockReduction.spatial_affine line 194
4. def OAI.RoughSplitBlockReduction.metricIdentity line 216
5. theorem OAI.RoughSplitBlockReduction.reduce_split_blocks line 226