`answer(sorry)` and asymptotic problems

Some problems are formulated in terms of finding a good/optimal asymptotic formulation for a given function, and are often formalised as e.g.
```lean
theorem foo : bar =0[atTop] answer(sorry) := by
sorry
```
where `bar` is the function of interest (possibly using other asymptotic notations of course, depending on the context!). One issue here is that this formulation is not really saying anything about the optimality of the function provided by `answer(sorry)`. Are there better ways of formalising this?