C1 and lipschitz

[IshiguroYoshihiro]

Motivation for this change

tentative definition C1

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[CohenCyril]

I do not think this is the "right definition". In order to define C1 on an open interval you only need
{in `]x, y[, forall x, derivable f x 1} and {within `]a, b[, continuous f^`()} and if you want to define C1 on a closed interval, you actually need more than derivable_oo_continuous_bnd f a b because you need derivability on the border of the interval.
We need to generalize differentiability and derivability to take into account the potential subspace topology of the domain in order to have a general version.
@zstone1 @affeldt-aist

[zstone1]

The subspace problem strikes again. For {within `[a, b], continuous f^`()} to work you need f^`() a to be well defined. That requires differentiable (f : R -> V) a, which you won't generally have here. The characteristic function X_[a,b] being my typical example of a C1([a,b]) function with "bad" behavior at the boundary.

As far as alternatives go, differentiating over subspaces will certainly work. You need to pick a "small enough" neighborhood, in the subspace topology, and consider all the directional derivatives that stay in the neighborhood. Some properties start to fail, though, like "minima have 0 derivative". I hesitate to alter the definition of differentiation to include a sometimes useful subspace parameter. I'd rather build on top of it than edit it.

I see two separate problems.

1. Adding conditions to ensure the limits of f^`() exist on the boundary
2. Actually constructing a the right term for the derivative.

Obviously it's the best case is if f^`() solves both problems, and it does on the open intervals. But an alternative could look like

`[extend U, g]` := fun x => 
  if U x then g x 
  else lim (g @ (within U (nbhs x)) 

then you work with [extend `]a,b[, f^`()]. We can pick a more compact notation if needed. The main observation is that we care mostly about the setting of closure U where U is open. There are also a variety of results like

f : (a,b) -> R is uniformly continuous <-> 
the left and right limits exist, and the extension `f^* : [a,b] -> R` is uniformly continuous

to guarantee that [extend U, g] is well-defined, continuous, etc.

I don't love this alternative. I am just trying to find a way to avoid altering "correct" definitions to account for new requirements.

[CohenCyril]

But will `[extend U, g] be smooth when g is smooth on U?

[CohenCyril]

I'd rather build on top of it than edit it.

I totally agree

You need to pick a "small enough" neighborhood, in the subspace topology, and consider all the directional derivatives that stay in the neighborhood. Some properties start to fail, though, like "minima have 0 derivative".

This is not a problem if some theorems are only valid on open sets...

[zstone1]

A good question. g could smooth in U, and `[extend U, g] could fail to be differentiable in closure U. I saw |1-x| on (-1,0) | (0,1) as a good example of this. Now if g^` is continuous in U, and the limits exist on the boundary, my intuition says you'll get `[extend U, g] is "continuously differentiable in the subspace closure U". But I certainly don't have a proof handy.

[affeldt-aist]

We tried a tentative fix for the definition of C1. We can mostly patch the lemma C1_lipschitz. The only remaining problem is to show:

dfa : derivable_right f a 1 (* cvg (h^-1 *: ((f \o shift a) h%:A - f a) @[h --> 0^'+]) *)
fa : f^`() x @[x --> a^'+] --> f^`() a
============================
(f x - f a) / (x - a) @[x --> a^'+] --> f^`() a

that looks like an exercise but whose solution has eluded us so far. :-(

[CohenCyril]

We tried a tentative fix for the definition of C1. We can mostly patch the lemma C1_lipschitz. The only remaining problem is to show:

dfa : derivable_right f a 1 (* cvg (h^-1 *: ((f \o shift a) h%:A - f a) @[h --> 0^'+]) *)
fa : f^`() x @[x --> a^'+] --> f^`() a
============================
(f x - f a) / (x - a) @[x --> a^'+] --> f^`() a

that looks like an exercise but whose solution has eluded us so far. :-(

It's because it's false. f^`() a is the derivative of f at a only when it is derivable all around a (near a^') here you only suppose derivability on the right of a...
We need either a separate notion of right derivative, or derivability wrt a restricted topology, as @zstone1 said before.