feat: separation of FiniteMeasure by StarSubalgebra

[JakobStiefel]

A StarSubalgebra of bounded continuous functions separates finite measures if it separates points. Important result in probability

---

• depends on: feat: results on inner regularity of finite measures #19780
• depends on: feat: add SpecialFunction MulExpNegMulSq and properties #19781

[github-actions]

PR summary cc463d7f9c

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)	1360
Mathlib.Analysis.SpecialFunctions.MulExpNegSq (new file)	2038
Mathlib.MeasureTheory.Measure.FiniteMeasureExt (new file)	2043

---

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
+ ext_of_forall_mem_subalgebra_integral_eq_of_polishSpace
+ ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetricSpace
+ 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
• feat: add SpecialFunction MulExpNegMulSq and properties #19781
  By Dependent Issues (🤖). Happy coding!

[sgouezel]

Instead of [PseudoEMetricSpace E] [CompleteSpace E] [SecondCountableTopology E], can you assume [TopologicalSpace E] [PolishSpace E] which doesn't fix a distance? Since the result below does not involve the distance, it is probably a better formulation.

I see this relies on other results of the PR, but the same goes probably with the other results in the PR, all the way up to the results on the regularity of the measure.

[JakobStiefel]

This can be done, but we lose some generality then (some metric space structure instead of pseudoemetric space). Would you nevertheless prefer this formulation?

[sgouezel]

Do you have an application in mind which is not separated? Typically, probability theory is done with polish spaces (often without a metric, so the current version would not be applicable), but if you have a use for the non-separated situation we could consider introducing a pseudoPolish class or whatever.

[JakobStiefel]

There are situations in probability where non-separated spaces appear, one usually modifies the space or metric then. I don't have a specific application in mind where this leads to a problem. Anyway, how about we state the theorem in the more general setting as it is now, and add the theorem on Polish spaces as an easy corollary (two line proof)? I just added this result