On Thu, Jan 9, 2020 at 6:10 PM Benoit <[email protected]> wrote:
> I agree that it's hard to understand. So ( S _D F ) is the derivative of F > restricted to S ? > Yes. By the way, it's strange that in both versions, the product in the second > summand is commuted. I mean: one has (fg)' = f'g + fg' (since \C is > commutative, you can certainly write it as (fg)' = f'g + g'f, but it's > weird). > That's the version I learned in school, it makes a good mnemonic. Since then I've learned about the non-commutative version of this theorem and perhaps it makes more sense to write it as you did, but of course multiplication on CC is commutative so ‾\_(ツ)_/‾ On Thu, Jan 9, 2020 at 6:31 PM Benoit <[email protected]> wrote: > On Thursday, January 9, 2020 at 12:07:11 PM UTC+1, Mario Carneiro wrote: >> >> If you want the function version, look at dvmul. But the relation version >> is the core version, because it isn't good enough to know that the >> derivative equals x if you don't know the function is also differentiable >> at x. Plus the derivative is not unique in certain pathological cases so >> you can't actually recover the relation version from the function version >> with differentiability side conditions. >> > > This worries me because I don't understand this at all... Is it possible > that "the derivative of f at x equals A" (you wrote "equals x") yet the > function is f not differentiable at x ? Is it a side effect of the coding > in set.mm, which makes undefined expressions equal to (/) (so the above > can happen only with A = (/) ) ? > Yes, that's exactly right. If the derivative at x doesn't exist, or has multiple values, then ( ( S _D F ) ` x ) = (/), but more to the point we really shouldn't be relying on the value we get here; this is a "junk" (/) and we should have guarded the application to avoid seeing it in the first place. > Second, you write that the derivative is not unique ? Last time I checked, > \C was Hausdorff. Or are you using a nonstandard definition for the > derivative ? > This is what the S is for. It represents the domain of approximations to f, and the derivative is defined on the interior of the domain of f *relative to S*. When S = RR this means the neighborhoods are open sets in RR and when S = CC these are open in CC, but S can also be something like [0, 1] in order to take the derivative of a function right up to the edge of an interval. It starts to get weird when S has isolated points, because then if f is defined at an isolated point x in S then any line through (x, f(x)) approximates the graph of f vacuously (because there are no points in a punctured neighborhood of x), so every slope is a valid derivative of f at x. The theorem perfdvf proves that if S has no isolated points, then the derivative is unique if it exists. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuQnED7SzqbTK5Oju_zYYV00b9t8b%2BuUPPsdf_-PEfghQ%40mail.gmail.com.
