Difference between formal and classical math

[Filip Cernatescu]

Why the statement of dvmulbr is so different from classical math (derivative of product of functions)?

[fl]

There's no difference. He used a notation based on relationships rather than functions.

That's unfortunate in my opinion. The usual semantics should be retained.

-- 

FL

[Mario Carneiro]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4746e0aa-8b89-4689-b6f9-a9d7d58dc55d%40googlegroups.com.

[David A. Wheeler]

On Thu, 9 Jan 2020 06:06:59 -0500, Mario Carneiro <di....@gmail.com> 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.

I've created a pull request to put this information into set.mm:
https://github.com/metamath/set.mm/pull/1397

--- David A. Wheeler

[Benoit]

I agree that it's hard to understand. So ( S _D F ) is the derivative of F restricted to S ?

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).

Benoît

[Benoit]

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 = (/) ) ?  I had proposed solutions (with of course some drawbacks) so that nonsensical expressions could not be written, or at least not be used, and this situation could be avoided (if I understand it correctly).

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 ?

Thanks,

Benoît

[Mario Carneiro]

On Thu, Jan 9, 2020 at 6:10 PM Benoit <benoit...@gmail.com> 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 <benoit...@gmail.com> 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

[fl]

The kind of totally hermetic, untraditional, unreferenced, undocumented kind of thing, where the coder has enjoyed himself and 

then it takes the reader three hours to understand what it is all about.

-- 

FL

[Benoit]

On Friday, January 10, 2020 at 1:52:20 AM UTC+1, Mario Carneiro wrote:

we should have guarded the application to avoid seeing it in the first place.

How would you do that ? (I gave some ideas some time ago on this group, but the drawbacks were deemed to outweigh the benefits.)

Thanks,

Benoît

[Mario Carneiro]

Nothing special; I just mean that any theorem using the expression ( ( S _D F ) ` x ) should have x e. dom ( S _D F ) in the context or derivable from it. It's the same way we currently treat division by zero: if you write ( A / B ) then you should be able to prove that B is nonzero, otherwise the statement is nonsense. This is ZFC so we can't prevent such statements from being formed, and what the context is exactly is not well defined, but in practice it works well enough.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e905a8c5-271d-4f28-b9fc-7ac39688e544%40googlegroups.com.

[David A. Wheeler]

On Friday, January 10, 2020 at 1:52:20 AM UTC+1, Mario Carneiro wrote:
> >> we should have guarded the application to avoid seeing it in the first
> >> place.

On Fri, Jan 10, 2020 at 5:40 PM Benoit <benoit...@gmail.com> wrote:
> > How would you do that ? (I gave some ideas some time ago on this group,
> > but the drawbacks were deemed to outweigh the benefits.)

On Fri, 10 Jan 2020 22:18:58 -0500, Mario Carneiro <di....@gmail.com> wrote:
> Nothing special; I just mean that any theorem using the expression ( ( S _D
> F ) ` x ) should have x e. dom ( S _D F ) in the context or derivable from it.

(Mario: I realize you already know this.
Benoit: I don't know if you had this in mind.)

Another approach for guarding is to use
"(New usage is discouraged.)". E.g., add some definition df-XYZ
with a construction that's marked "(New usage is discouraged.)",
then prove specific properties of it & add them to the "discouraged" file
(as permitted uses). From then on, you can depend on the proven
properties, but you can't depend on the discouraged details of the
construction without specially adding it as a new use
(which triggers additional human review).

--- David A. Wheeler

[Benoit]

Thanks.  Yes, Mario's and David's suggestions are two possibilities I had in mind, with other, more strict ones, with the drawbacks alluded to above.  I'll try to list them in a separate thread.

Benoît