Commit 2025-02-14 10:46 0efc5f65

View on Github →

feat: Properties of the Integral of MulExpNegMulSq (#19781) Show convergence properties of the Integral of MulExpNegMulSq wrt finite measures, important for the proof of separation of finite measures by subalgebras of functions

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

added theorem abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt

added theorem abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure

added theorem dist_integral_mulExpNegMulSq_comp_le

added theorem integrable_mulExpNegMulSq_comp

added theorem integrable_mulExpNegMulSq_comp_restrict_of_isCompact

added theorem integral_mulExpNegMulSq_comp_eq

added theorem tendsto_integral_mulExpNegMulSq_comp

added theorem tendsto_integral_mul_one_plus_inv_smul_sq_pow

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

added theorem MeasureTheory.tendsto_integral_filter_of_norm_le_const

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem MeasureTheory.norm_integral_sub_setIntegral_le

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.ext_of_forall_integral_eq

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

added theorem ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

added theorem dist_triangle8