Some problems are formulated in terms of finding a good/optimal asymptotic formulation for a given function, and are often formalised as e.g.
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?
Some problems are formulated in terms of finding a good/optimal asymptotic formulation for a given function, and are often formalised as e.g.
where
baris 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 byanswer(sorry). Are there better ways of formalising this?