Commit 2025-03-19 10:47 c2fb8f07

View on Github →

feat: separation of FiniteMeasure by StarSubalgebra (#19782) A StarSubalgebra of bounded continuous functions separates finite measures if it separates points. Important result in probability

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.lipschitzWith_ofReal

Created Mathlib/Analysis/RCLike/BoundedContinuous.lean

added theorem RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Created Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean

added theorem MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_polish

added theorem MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

added theorem MeasureTheory.ext_of_forall_integral_eq_of_IsFiniteMeasure

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

modified theorem BoundedContinuousFunction.add_compContinuous

modified def BoundedContinuousFunction.coeFnAddHom

added theorem BoundedContinuousFunction.coe_toContinuousMapₐ

added theorem BoundedContinuousFunction.comp_apply

modified theorem BoundedContinuousFunction.mkOfCompact_add

modified def BoundedContinuousFunction.toContinuousMapAddHom

added def BoundedContinuousFunction.toContinuousMapₐ

Modified Mathlib/Topology/ContinuousMap/Bounded/Star.lean

added theorem BoundedContinuousFunction.coe_toContinuousMapStarₐ

added def BoundedContinuousFunction.toContinuousMapStarₐ