minor additions and generalizations

[affeldt-aist]

Motivation for this change

The lemmas proposed by this PR are slight generalizations (e.g., parameters of derivable_cst, derive_cst that generalized derive1_cst) or lemmas that are specialized variants of
already existing lemmas (e.g., deriveX_id, deriveMr, derive_id). Specialized variants might
look superfluous at first sight but they do save several micro steps in practical examples and
moreover since we have a naming convention (this PR documents it) for the file derive.v
these variants are expected results of Search. Certainly, there is more to do in this file but
that might already be a useful step.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Thanks, I totally forgot about this notation.

[CohenCyril]

Why suffix _id?

[affeldt-aist]

As a special case of:

Lemma deriveX f n (x v : V) : derivable f x v ->
  'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x.

[CohenCyril]

This reminds me of mul_continuous and cvgM (and continuousM).
In fact these are all equivalent and the bridge is composition.
We should come up with a consistent naming scheme if we are going that way and I do not think id is very informative here...

[affeldt-aist]

In lebesgue_measure.v, we did that:

Lemma measurable_exprn D n : measurable_fun D (fun x => x ^+ n).
(* coming first *)

Lemma measurable_fun_pow D f n : measurable_fun D f ->
  measurable_fun D (fun x => f x ^+ n).
(* proved using measurable_comp *)

[CohenCyril]

Oh, this is bad... the head symbol's name is exp in both case and pow is now booked for the power function R -> R -> R (which in fairness should probably swapped, but that's a completely different question).
Anyway we should not solve the problem by introducing duplicate names for existing symbols (let's not have prod as an alternative for mul nor plus as an alternative for add 😉), but by finding a uniform naming scheme which encompasses all the cases for continuity, measurability and various notions of derivability.

My suggestion is we align with the conventions for continuity with the following rationale:

• when a lemma is about a composite, like the current cvgM, continuousM, deriveX or measurable_fun_pow, we use the single letter suffix (when it exists) as in cvgM, continuousM, deriveX, or measurable_funX
• when a lemma is about applied function, we use the multi-letter prefix instead as in mul_continuous, exp_derive or exp_measurable_fun.

[affeldt-aist]

I think that we chose to use measurable instead of measurable_fun when the suffix suggests a function.

[affeldt-aist]

I guess this shortcut is only acceptable when it does not cause ambiguity, I'll try your proposal fixes asap.

[CohenCyril]

when the prefix is a function name I guess it makes sense indeed

[affeldt-aist]

So maybe use X for the cardinal product and Xn for GRing.exp?

[affeldt-aist]

(well funX is clear enough maybe)

[affeldt-aist]

@CohenCyril ok to merge in the current state?

[CohenCyril]

Aside from my (minor) comment. LGTM