Several (tutoring) students have asked me for a formal definition of amortized time and I've never been able to find one online. All the literature I've found usually outlines the three most common methods for doing the actual analysis and no more. In a few places there are explanations of why the amortized time for $op$ is not $O(f(n))$ by presenting a series of operations whose combined $op$s take $\omega(f(n))$ on average, but nowhere I've looked provides an unambiguous definition.
The definition I've settled on is:
For some data structure $S$ and operation $op$ of $S$, the amortized time for $op$ is $O(f(n))$ if and only if for every sufficiently large $m$ and any series of $m$ operations on $S$, if $k$ of those operations were $op$ then the sum of actual times for those $k$ operations in the series is $O(k\cdot f(n))$.
The amortized time for $op$ is $\Omega(f(n))$ if and only if there exists such a series where the sum of actual times of the $op$s is $\Omega(f(n))$.
The above can be applied to $o(f(n))$ and $\omega(f(n))$ respectively.
My question is whether this is a good definition of amortized time for operations in a data structure and if not, what would a better definition be?