Theorems · Theorem · measure theory

abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt

∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (f : C(E, ℝ)) {K : Set E},
  MeasurableSet K →
    0 < ε → P Kᶜ < ↑ε.toNNReal → |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε

Defined in

Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasure