feat (WIP): formalize Moreira's version of Sard's theorem

[urkud]

---

[github-actions]

PR summary 5fa2eac3e2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Calculus.Moreira2001 (new file)	1937

---

Declarations diff

+ Chart
+ ContDiffAt.eventually_contDiffOn
+ ContDiffHolder
+ ContDiffWithinAt.contDiffOn_inter_isOpen_subset
+ ContDiffWithinAt.eventually_contDiffOn
+ ContDiffWithinAt.hasFTaylorSeriesUpToOn_subset_of_eventually
+ comp
+ dist_iteratedFDerivWithin_one
+ dist_iteratedFDerivWithin_zero
+ exists_one
+ ftaylorSeriesWithin_insert
+ injOn
+ instCoeFun
+ isBigO_dist_mul_of_fderiv
+ isBigO_of_le
+ iteratedFDerivWithin_comp
+ iteratedFDerivWithin_comp_of_eventually
+ iteratedFDerivWithin_congr_set'
+ iteratedFDerivWithin_insert
+ iteratedFDeriv_comp
+ main
+ mkOne
+ norm_applyOrderedFinpartition_le
+ norm_compAlongOrderedFinpartitionL_apply_le
+ norm_compAlongOrderedFinpartitionL_le
+ norm_compAlongOrderedFinpartition_le
+ norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le
+ norm_iteratedFDerivWithin_one
+ rpow_le_rpow_of_exponent_ge_of_imp
+ rpow_le_self_of_le_one
+ rpow_le_self_of_one_le
+ rpow_lt_self_of_lt_one
+ rpow_lt_self_of_one_lt
+ self_le_rpow_of_le_one
+ self_le_rpow_of_one_le
+ self_lt_rpow_of_lt_one
+ self_lt_rpow_of_one_lt
+ subset_left
+ subset_right
+ theorem_2_1
++ HasFTaylorSeriesUpToOn.congr_series

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