OAI/Analysis/TracialSplitting/BlockSampling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.PackingStepBounds.mono_quality line 20
2. lemma OAI.CurrentMain.exists_precise_packing_round line 36
3. lemma OAI.CurrentMain.SampledPackingRound.precise_sampled_energy_sum line 91
4. lemma OAI.CurrentMain.SampledPackingRound.inserted_row_energy line 104