OAI/Combinatorics/EditApproximation/Refinement/ComputedLocalKernelWork.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.localKernelPowerExponent line 10
2. def OAI.EditApproximation.computedLocalKernelBudget line 12
3. def OAI.EditApproximation.computedLocalKernelExponent line 16
4. theorem OAI.EditApproximation.computedLocalKernelExponent_tendsto line 21
5. theorem OAI.EditApproximation.localKernelBudget_exp_scalar line 31
6. theorem OAI.EditApproximation.computedLocalKernelBudget_exp_bound line 47
7. theorem OAI.EditApproximation.computedLocalKernelBudget_subpolynomial line 56
8. theorem OAI.EditApproximation.computedLocalKernelBudget_envelope_near_linear line 62
9. theorem OAI.EditApproximation.computedLocalKernelBudget_widthWork_near_linear line 70
10. theorem OAI.EditApproximation.computedLocalKernelBudget_requests_near_linear line 84