Email Gateway (Apr 13 2024 at 15:26): Email Gateway (Apr 13 2024 at 15:26):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
I noticed that the definition of "piecewise_C1_on" in HOL-Analysis is a
bit weaker than what one would expect. Unlike what one finds in the
literature (e.g. [1]), it does not require the one-sided derivatives to
exist at the "cutting points". This also has consequences for the
definition of a "valid_path": a "valid_path" can e.g. oscillate wildly
at a point, like sin(1/x) at 0. This is rather unpleasant and probably
not intended. My version of the definition should have the property that
a path is a "valid_path" (i.e. piecewise C1) if and only if it is a
concatenation of finitely many C1 paths (modulo reparametrisation).
I therefore recommend we try to strengthen these definitions. I hope the
repercussions will not be too great. I attached a file with some
suggestions for how to define piecewise C1 (and in fact Cn for general 0
≤ n ≤ ∞). If anyone considers themselves to have a stake in this, please
comment on it.
Cheers,
Manuel
Email Gateway (Apr 14 2024 at 05:57):From: 伊藤洋介 <glacier345@gmail.com>
Dear Manuel,
Thank you for the suggestion.
I don't have a stake in this, but I agree with you.
By the way, what do you think about the definition of
"piecewise_differentiable_on" in Derivative, HOL-Analysis?
definition piecewise_differentiable_on
(infixr "piecewise'_differentiable'_on" 50)
where "f piecewise_differentiable_on i ≡
continuous_on i f ∧
(∃S. finite S ∧ (∀x ∈ i - S. f differentiable (at x within
i)))"
This definition does not require the existence of the one-sided derivative.
If you change the definition of "C1_differentiable_on" as you show it, it
may be natural to modify "piecewise_differentiable_on" in the same manner.
By doing so, some functions like f(x) = \sqrt(x) (x > 0) (otherwise 0)
will not be piecewise differentiable any more.
I heavily depend on "piecewise_differentiable_on", but the change above is
acceptable.
Best regards,
2024年4月14日(日) 0:26 Manuel Eberl <manuel@pruvisto.org>:
Hello,
I noticed that the definition of "piecewise_C1_on" in HOL-Analysis is a
bit weaker than what one would expect. Unlike what one finds in the
literature (e.g. [1]), it does not require the one-sided derivatives to
exist at the "cutting points". This also has consequences for the
definition of a "valid_path": a "valid_path" can e.g. oscillate wildly
at a point, like sin(1/x) at 0. This is rather unpleasant and probably
not intended. My version of the definition should have the property that
a path is a "valid_path" (i.e. piecewise C1) if and only if it is a
concatenation of finitely many C1 paths (modulo reparametrisation).I therefore recommend we try to strengthen these definitions. I hope the
repercussions will not be too great. I attached a file with some
suggestions for how to define piecewise C1 (and in fact Cn for general 0
≤ n ≤ ∞). If anyone considers themselves to have a stake in this, please
comment on it.Cheers,
Manuel
Email Gateway (Apr 14 2024 at 16:22):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
absolutely. Unlike piecewise_C1_differentiable, it seems that
piecewise_differentiable_on is not widely used in the distribution and
the AFP, so it should be much easier to change the definition.
Just to be clear, none of this will happen before the next release.
There will be repercussions for some AFP entries – nothing major, I
expect, but still far too big a change to do it now right before the
release.
Manuel
Email Gateway (Apr 14 2024 at 23:40):From: 伊藤洋介 <glacier345@gmail.com>
Hello Manuel,
Thank you for the reply.
I acknowledge your plan and the schedule for modification.
I appreciate your announcement in advance.
2024年4月15日(月) 1:22 Manuel Eberl <manuel@pruvisto.org>:
Last updated: May 05 2024 at 01:11 UTC