feat: add SpecialFunction MulExpNegMulSq and properties

[JakobStiefel]

add SpecialFunction MulExpNegMulSq, important tool in the proof of separation of finite measures by subalgebras of functions

---

• depends on: feat: results on inner regularity of finite measures #19780

[github-actions]

PR summary 27de0f3652

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Measure.RegularityCompacts (new file)	1358
Mathlib.Analysis.SpecialFunctions.MulExpNegSq (new file)	2060

---

Declarations diff

+ ENNReal.exists_seq_pos_eq
+ ENNReal.exists_seq_pos_lt
+ FiniteMeasure.tendstoIntegral_of_eventually_boundedPointwise
+ InnerRegularCompactLTTop_of_complete_countable
+ NNReal.exists_seq_pos_summable_eq
+ PolishSpace.innerRegular_isCompact_measurableSet
+ _root_.MeasurableSet.ball
+ _root_.MeasureTheory.measure_compl_interUnionBalls_le
+ bounded_of_expSeq
+ dist_integral_mulExpNegMulSq_le
+ dist_triangle8
+ emul_le_exp
+ exists_isCompact_closure_measure_lt_of_complete_countable
+ exists_measure_iInter_lt
+ exists_mem_subalgebra_near_continuous_on_compact_of_separatesPoints
+ expNegSq_deriv
+ expNegSq_differentiable
+ expNegSq_differentiableAt
+ ext_of_forall_integral_eq
+ innerRegularWRT_isCompact_closure_iff
+ innerRegularWRT_isCompact_closure_of_complete_countable
+ innerRegularWRT_isCompact_closure_of_univ
+ innerRegularWRT_isCompact_isClosed_iff
+ innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure
+ innerRegularWRT_isCompact_isClosed_isOpen_of_complete_countable
+ innerRegularWRT_isCompact_isClosed_of_complete_countable
+ innerRegularWRT_isCompact_isOpen_of_complete_countable
+ innerRegularWRT_isCompact_of_complete_countable
+ innerRegularWRT_of_exists_compl_lt
+ innerRegular_isCompact_isClosed_measurableSet_of_complete_countable
+ integral_mulExpNegMulSq_eq
+ integral_mulExpNegMulSq_le_mul_measure
+ integral_mulExpNegMulSq_lt
+ integral_mulExpNegMulSq_tendsto
+ interUnionBalls
+ isCompact_closure_interUnionBalls
+ mulExpNegMulSq
+ mulExpNegMulSq_abs_le
+ mulExpNegMulSq_abs_le_norm
+ mulExpNegMulSq_bounded
+ mulExpNegMulSq_eq_sqrt_mul_mulExpNegSq
+ mulExpNegMulSq_lipschitz
+ mulExpNegMulSq_tendsto
+ mulExpNegSq
+ mulExpNegSq_apply
+ mulExpNegSq_bounded
+ mulExpNegSq_bounded_above
+ mulExpNegSq_deriv
+ mulExpNegSq_deriv_le_one
+ mulExpNegSq_lipschitz1
+ mulExpNegSq_symm
+ mul_le_one_of_le_inv
+ norm_integral_sub_setIntegral_le
+ tendsto_atTop_zero_iff_le_of_antitone
+ tendsto_atTop_zero_iff_lt_of_antitone
+ tendsto_integral_expSeq_mulExpNegMulSq
+ totallyBounded_interUnionBalls
+ zero_le_one_sub_div

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: results on inner regularity of finite measures #19780
  By Dependent Issues (🤖). Happy coding!

[sgouezel]

The file Mathlib/Analysis/SpecialFunctions/MulExpNegSq.lean that you are introducing contains a bunch of results, in many directions and with a log of imports. It would probably be a good idea to have one basic file containing just the basic properties of the function (without any measure theory, say), and another file devoted to its properties wrt integration.

Do you think you could do such a split, and extract a PR just devoted to the first file, i.e., basic properties of the function? This would be easier and quicker to review -- in general, aiming for PRs of less than 200 lines if possible is a good idea, as reviewers will be more inclined to review it.