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.apply_le_nndist_zero {X : Type u_1} [TopologicalSpace X] (f : BoundedContinuousFunction X NNReal) (x : X) : f x ≤ nndist 0 f

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.measurable_coe_ennreal_comp {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (f : BoundedContinuousFunction X NNReal) : Measurable fun (x : X) => ↑(f x)

theorem BoundedContinuousFunction.lintegral_lt_top_of_nnreal {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X NNReal) : ∫⁻ (x : X), ↑(f x) ∂μ < ⊤

theorem BoundedContinuousFunction.integrable_of_nnreal {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X NNReal) : MeasureTheory.Integrable (NNReal.toReal ∘ ⇑f) μ

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.lintegral_of_real_lt_top {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ) : ∫⁻ (x : X), ENNReal.ofReal (f 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.lintegral_nnnorm_le {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2} [NormedAddCommGroup E] (f : BoundedContinuousFunction X E) : ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ↑‖f‖₊ * μ Set.univ

theorem BoundedContinuousFunction.integrable {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X E) : MeasureTheory.Integrable (⇑f) μ

theorem BoundedContinuousFunction.norm_integral_le_mul_norm {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X E) : ‖∫ (x : X), f x ∂μ‖ ≤ (μ Set.univ).toReal * ‖f‖

theorem BoundedContinuousFunction.norm_integral_le_norm {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℝ E] [MeasureTheory.IsProbabilityMeasure μ] (f : BoundedContinuousFunction X E) : ‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖

theorem BoundedContinuousFunction.isBounded_range_integral {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [NormedSpace ℝ E] {ι : Type u_3} (μs : ι → MeasureTheory.Measure X) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (f : BoundedContinuousFunction X E) : Bornology.IsBounded (Set.range fun (i : ι) => ∫ (x : X), f x ∂μs i)

theorem BoundedContinuousFunction.integral_add_const {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ) (c : ℝ) : ∫ (x : X), (f + BoundedContinuousFunction.const X c) x ∂μ = ∫ (x : X), f x ∂μ + (μ Set.univ).toReal • c

theorem BoundedContinuousFunction.integral_const_sub {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X ℝ) (c : ℝ) : ∫ (x : X), (BoundedContinuousFunction.const X c - f) x ∂μ = (μ Set.univ).toReal • c - ∫ (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 ≤ f → Filter.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 ∂μ))