feat: regularity of the pullback of a vector field on a manifold

[sgouezel]

We show that the pullback of a C^m vector field on a manifold under a C^{m+1} map with invertible derivative is C^m.

---

[github-actions]

PR summary 92a1014bb3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ChartedSpace.discreteTopology
+ _root_.ContMDiff.mpullback_vectorField
+ _root_.ContMDiffAt.mpullback_vectorField_preimage
+ _root_.ContMDiffOn.mpullbackWithin_vectorField_inter
+ _root_.ContMDiffOn.mpullback_vectorField_preimage
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField'
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_inter
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq'
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem
+ _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq
+ _root_.ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin
+ _root_.ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq
+ _root_.ContMDiffWithinAt.mpullback_vectorField_preimage
+ _root_.ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq
+ contMDiffWithinAt_mpullbackWithin_extChartAt_symm
+ differentiableAt_of_isInvertible_fderiv
+ differentiableWithinAt_of_isInvertible_fderivWithin
+ eventuallyEq_mpullback_mpullbackWithin_extChartAt
+ eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm
+ isInvertible_zero_iff
+ mdifferentiableAt_of_isInvertible_mfderiv
+ mdifferentiableWithinAt_of_isInvertible_mfderivWithin
+ mdifferentiable_of_subsingleton
+ mpullbackWithin_comp_of_left
+ mpullbackWithin_comp_of_right

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

I have only reviewed the "leaf" parts so far: everything up to the section "ContDiff" in the main file. (Help with that welcome. I will be at a conference next week, so with little time for reviewing.) Only superficial comments.