OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseSamplingWork.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.EditApproximation.symbolicComputedExecutionCoarseSamplingWork_integrableline 23 - theorem
OAI.EditApproximation.symbolicComputedExecutionCoarseSamplingWork_boundline 42 - theorem
OAI.EditApproximation.computedExecutionCoarseSamplingWork_integrableline 60 - theorem
OAI.EditApproximation.computedExecutionCoarseSamplingWork_boundline 65 - theorem
OAI.EditApproximation.computedExecutionCoarseSamplingWork_expected_near_linearline 72