OAI/Geometry/TranslativeCovering/Blocks.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Blocks.first_budget_point line 30
2. lemma OAI.Blocks.loss_bound line 44
3. lemma OAI.Blocks.anchors line 58
4. def OAI.Blocks.weight line 70
5. theorem OAI.Blocks.block_estimates line 73