Sg param i

[sgouezel]

---

[github-actions]

PR summary 69fc0048aa

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Calculus.ParametricIntegral	2212	2218	+6 (+0.27%)
Mathlib.Analysis.Calculus.ParametricIntervalIntegral	2213	2219	+6 (+0.27%)

Import changes for all files

Files	Import difference
4 files Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Geometry.Manifold.BumpFunction	1
Mathlib.Analysis.Convolution	3
Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral	6

---

Declarations diff

+ ContDiff.parametric_integral
+ ContDiff.parametric_intervalIntegral
+ ContDiffOn.parametric_intervalIntegral
+ Continuous.aestronglyMeasurable_of_compactSpace
+ Continuous.parametric_integral
+ ContinuousOn.parametric_integral
+ _root_.ContinuousOn.parametric_intervalIntegral
+ continuousOn_closure_inter_setOf
+ continuousWithinAt_parametric_integral
+ mem_nhdsSetWithin_iff_forall
+ restrict_inter_toMeasurable
++ ContDiffOn.parametric_integral
++ hasFDerivAt_integral_of_contDiffOn
++ hasFDerivAt_integral_of_continuousOn_fderiv

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

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"