Documentation

Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Integration of bounded continuous functions #

In this file, some results are collected about integrals of bounded continuous functions. They are mostly specializations of results in general integration theory, but they are used directly in this specialized form in some other files, in particular in those related to the topology of weak convergence of probability measures and finite measures.

theorem BoundedContinuousFunction.lintegral_le_edist_mul {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (f : BoundedContinuousFunction X NNReal) (μ : MeasureTheory.Measure X) :
∫⁻ (x : X), (f x)μ edist 0 f * μ Set.univ
theorem BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ) :
∫ (x : X), f xμ = ∫ (x : X), (f.nnrealPart x)μ - ∫ (x : X), ((-f).nnrealPart x)μ
theorem BoundedContinuousFunction.toReal_lintegral_coe_eq_integral {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (f : BoundedContinuousFunction X NNReal) (μ : MeasureTheory.Measure X) :
(∫⁻ (x : X), (f x)μ).toReal = ∫ (x : X), (f x)μ
theorem BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ιMeasureTheory.Measure X} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ (f : BoundedContinuousFunction X ), 0 fFilter.limsup (fun (i : ι) => ∫ (x : X), f xμs i) L ∫ (x : X), f xμ) (f : BoundedContinuousFunction X ) :
Filter.Tendsto (fun (i : ι) => ∫ (x : X), f xμs i) L (nhds (∫ (x : X), f xμ))
theorem BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ιMeasureTheory.Measure X} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ (f : BoundedContinuousFunction X ), 0 f∫ (x : X), f xμ Filter.liminf (fun (i : ι) => ∫ (x : X), f xμs i) L) (f : BoundedContinuousFunction X ) :
Filter.Tendsto (fun (i : ι) => ∫ (x : X), f xμs i) L (nhds (∫ (x : X), f xμ))