Theorems · Theorem · measure theory

integral_mulExpNegMulSq_comp_eq

∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P']
  {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)},
  0 < ε →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') →
      ∀ {g : BoundedContinuousFunction E ℝ},
        g ∈ A → ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

Defined in

Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure