Theorems · Theorem · measure theory

dist_integral_mulExpNegMulSq_comp_le

∀ {ε : ℝ} {E : Type u_2} [inst : MeasurableSpace E] [inst_1 : PseudoEMetricSpace E] [BorelSpace E] [CompleteSpace E]
  [SecondCountableTopology E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P]
  [MeasureTheory.IsFiniteMeasure P'] (f : BoundedContinuousFunction E ℝ)
  {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)},
  (Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ) A).SeparatesPoints →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') →
      0 < ε → |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

If for any g ∈ A the integrals with respect to two finite measures P, P' coincide, then the difference of the integrals of mulExpNegMulSq ε ∘ g with respect to P, P' is bounded by 6 * √ε.

Defined in

Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Cited by

1 results in Mathlib

Foundations

Depth 282 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpacePseudoEMetricSpaceBorelSpaceCompleteSpaceSecondCountableTopologyMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure