Here the magic lies in depending on the axiom of choice to get a non-principal ultrafilter. And I believe I see a crack in the above definition of the derivative. f is a function on the non-standard reals, but its derivative is defined to only take standard values, so it will be constant in the infinitesimal range around any standard real. If f(x)=x2, then its derivative should surely be 2x everywhere. The above definition only gives you that for standard values of x.
Yep, the definition is wrong. If f:R→R then let ∗f denote the natural extension of this function to the hyperreals (considering ∗R behaves like R this should work in most cases). Then, I think the derivative should be
f′(x)=st(∗f(x+Δx)−∗f(x)Δx)
W.r.t. what the derivative of ∗f should be, I imagine you can describe it similarly in terms of ∗∗R, which by the transfer principle should exist (which applies because of Łoś′s theorem, which I don’t claim to fully understand).
Yep, the definition is wrong. If f:R→R then let ∗f denote the natural extension of this function to the hyperreals (considering ∗R behaves like R this should work in most cases). Then, I think the derivative should be
f′(x)=st(∗f(x+Δx)−∗f(x)Δx)
W.r.t. what the derivative of ∗f should be, I imagine you can describe it similarly in terms of ∗∗R, which by the transfer principle should exist (which applies because of Łoś′s theorem, which I don’t claim to fully understand).
For f(x)=x2, the derivative then is:
f′(x)=st((x+Δx)2−x2Δx),=st(2x+Δx),=2x.