WIP: generalize or comment parts of FDeriv/Basic.lean

[eric-wieser]

---

[github-actions]

PR summary 9ffe92940e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Calculus.TangentCone.Basic	1443	1195	-248 (-17.19%)
Mathlib.Analysis.Calculus.TangentCone.Prod	1443	1199	-244 (-16.91%)
Mathlib.Analysis.Calculus.TangentCone.Pi	1444	1239	-205 (-14.20%)
Mathlib.Analysis.Calculus.TangentCone.Real	1510	1363	-147 (-9.74%)
Mathlib.Analysis.Calculus.TangentCone.DimOne	1444	1316	-128 (-8.86%)
Mathlib.Analysis.Calculus.TangentCone.Defs	1172	1174	+2 (+0.17%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Calculus.TangentCone.Basic	-248
Mathlib.Analysis.Calculus.TangentCone.Prod	-244
Mathlib.Analysis.Calculus.TangentCone.Pi	-205
Mathlib.Analysis.Calculus.TangentCone.Real	-147
Mathlib.Analysis.Calculus.TangentCone.DimOne	-128
Mathlib.Analysis.Calculus.TangentCone	-98
Mathlib.Analysis.RCLike.TangentCone	-20
Mathlib.Analysis.Calculus.TangentCone.Defs	2
Mathlib.Analysis.Calculus.TangentCone.Seq (new file)	1506

---

Declarations diff

+ AccPt.of_mem_tangentConeAt_ne_zero
+ ClusterPt.top
+ Filter.HasBasis.tangentConeAt_eq_biInter_closure
+ NNReal.isEmbedding_coe
+ NNReal.isUniformEmbedding_coe
+ exists_fun_of_mem_tangentConeAt
+ map_coe_nhdsGE
+ map_coe_nhdsGT
+ mem_closure_of_nonempty_tangentConeAt
+ mem_tangentConeAt_iff_exists_seq
+ mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop
+ mem_tangentConeAt_of_add_smul_mem
+ mem_tangentConeAt_of_frequently
+ mem_tangentConeAt_of_seq
+ sub_mem_posTangentConeAt_of_openSegment_subset
+ tangentConeAt_eq_biInter_closure
+ zero_mem_tangentConeAt_iff
- Asymptotics.IsBigO.hasFDerivAt
- Asymptotics.IsBigO.hasFDerivWithinAt
- Differentiable.continuous
- DifferentiableAt.comp_semilinear₂
- DifferentiableAt.continuousAt
- DifferentiableAt.isBigO_sub
- DifferentiableOn.continuousOn
- DifferentiableWithinAt.continuousWithinAt
- DifferentiableWithinAt.isBigO_sub
- HasFDerivAt.comp_semilinear
- HasFDerivAt.continuousAt
- HasFDerivAt.isBigO_sub
- HasFDerivAt.le_of_lip'
- HasFDerivAt.le_of_lipschitz
- HasFDerivAt.le_of_lipschitzOn
- HasFDerivAt.lim
- HasFDerivAtFilter.isBigO_sub
- HasFDerivAtFilter.isBigO_sub_rev
- HasFDerivAtFilter.tendsto_nhds
- HasFDerivWithinAt.continuousWithinAt
- HasFDerivWithinAt.isBigO_sub
- HasStrictFDerivAt.continuousAt
- HasStrictFDerivAt.exists_lipschitzOnWith
- HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt
- HasStrictFDerivAt.isBigO_sub
- HasStrictFDerivAt.isBigO_sub_rev
- hasFDerivAtFilter_iff_tendsto
- hasFDerivAt_iff_isLittleO_nhds_zero
- hasFDerivAt_iff_tendsto
- hasFDerivWithinAt_iff_tendsto
- norm_fderiv_le_of_lip'
- norm_fderiv_le_of_lipschitz
- norm_fderiv_le_of_lipschitzOn
- tangentConeAt

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