OAI/Analysis/JiangSu/Comparison/PrecisePackingRound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectPacking.PackingStepBounds.mono_quality line 16
2. lemma OAI.DirectPacking.exists_precise_packing_round line 32
3. lemma OAI.DirectPacking.SampledPackingRound.precise_sampled_energy_sum line 82
4. lemma OAI.DirectPacking.SampledPackingRound.inserted_row_energy line 95
5. def OAI.DirectPacking.OrthogonalProjectionPair.zero line 115
6. structure OAI.DirectPacking.PackingBounds line 124