OAI/Analysis/JiangSu/CentralSequences/MatrixCompressionCentrality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectPacking.hom_maps_projection line 17
2. lemma OAI.DirectPacking.projection_overlap_gap line 23
3. lemma OAI.DirectPacking.MatrixPackingCertificate.compress_projection_energy line 41