feat: separation of FiniteMeasure by StarSubalgebra or characteristic functions

[JakobStiefel]

A StarSubalgebra of bounded continuous functions separates finite measures if it separates points. The special case where the subalgebra consists of characteristic functions is an important result in probability

---

• depends on: [Merged by Bors] - feat: results on inner regularity of finite measures #19780
• depends on: feat: add SpecialFunction MulExpNegMulSq and properties #19781
• depends on: feat: separation of FiniteMeasure by StarSubalgebra #19782
• depends on: feat: definition and properties of characteristic functions #19783

[github-actions]

PR summary 3876d51d18

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
79 files Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Analysis.NormedSpace.RCLike Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.Cardinality Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.RingTheory.Polynomial.Tower Mathlib.Algebra.Vertex.VertexOperator Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.RingTheory.Polynomial.Dickson Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Central.Defs Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.Compact Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Polynomial.RingDivision Mathlib.Analysis.Normed.Field.Basic Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Polynomial.Taylor Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.NumberTheory.PellMatiyasevic Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.Analysis.Normed.Group.Tannery Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Analysis.SumOverResidueClass Mathlib.Topology.ContinuousMap.Units Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Algebra.Algebra.Spectrum Mathlib.RingTheory.Binomial Mathlib.Algebra.Polynomial.Laurent Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.RingTheory.Algebraic.Pi Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Analysis.RCLike.Basic Mathlib.NumberTheory.Dioph Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.RingTheory.HahnSeries.Summable Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.CStarAlgebra.Basic Mathlib.NumberTheory.Pell Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Analysis.NormedSpace.Extend Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.Convex.Gauge Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Central.Basic Mathlib.Algebra.Polynomial.Lifts Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Central.Matrix Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Algebra.Polynomial.Roots Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.FieldTheory.IntermediateField.Basic Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Algebra.Star.Unitary Mathlib.Topology.ContinuousMap.Ideals Mathlib.Algebra.Polynomial.Smeval Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps	1
Mathlib.MeasureTheory.Measure.RegularityCompacts (new file)	1356
Mathlib.Analysis.SpecialFunctions.MulExpNegSq (new file)	2058
Mathlib.MeasureTheory.Measure.FiniteMeasureExt (new file)	2063
Mathlib.MeasureTheory.Measure.FiniteMeasureCharFun (new file)	2068

---

Declarations diff

+ ENNReal.exists_seq_pos_eq
+ ENNReal.exists_seq_pos_lt
+ FiniteMeasure.ext_of_charFun_eq
+ FiniteMeasure.tendstoIntegral_of_eventually_boundedPointwise
+ InnerRegularCompactLTTop_of_complete_countable
+ NNReal.exists_seq_pos_summable_eq
+ PolishSpace.innerRegular_isCompact_measurableSet
+ StarSubalgebra.of_span_submonoid
+ Subalgebra.of_span_submonoid_starmem
+ _root_.MeasurableSet.ball
+ _root_.MeasureTheory.measure_compl_interUnionBalls_le
+ bounded_of_expSeq
+ continuous_dotProduct
+ continuous_probFourierChar
+ dist_integral_mulExpNegMulSq_le
+ dist_triangle8
+ dotProduct
+ 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_charFun_eq
+ ext_of_forall_integral_eq
+ ext_of_forall_mem_subalgebra_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
+ of_span_set
+ of_span_submonoid
+ probChar
+ probChar_SeparatesPoints
+ probChar_StarSubalgebra_separatesPoints
+ probChar_abs_one
+ probChar_apply
+ probChar_dist_le_two
+ probChar_eq
+ probChar_mul_mem
+ probChar_one_mem
+ probChar_starSubalgebra
+ probChar_starSubalgebra_bounded
+ probChar_starSubalgebra_integrable
+ probChar_star_mem
+ probChar_submonoid
+ probChar_submonoid_dist_le_two
+ probFourierChar
+ probFourierChar_apply
+ 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).

[RemyDegenne]

Nice! This PR is very large (hence hard to review) and contains many things that could be PRed independently.
Could you open several small PRs which each contain a coherent subset of this, and mark this PR as depending on the others?

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: results on inner regularity of finite measures #19780
• feat: add SpecialFunction MulExpNegMulSq and properties #19781
• feat: separation of FiniteMeasure by StarSubalgebra #19782
• feat: definition and properties of characteristic functions #19783
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

This PR has the same title as #19782 but is apparently bigger (more lines of code changed). Can you rename one of them? Also there's a typo FiniteMeasaure in both titles.

I also changed the two spaces between [] in the "depend on" lines to one space, so that they display as boxes.