BoundedContinuousFunction.integrable
theorem BoundedContinuousFunction.integrable :
∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
(μ : MeasureTheory.Measure X) {E : Type u_2} [inst_3 : NormedAddCommGroup E] [inst_4 : SecondCountableTopology E]
[inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] [inst_7 : MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction X E), MeasureTheory.Integrable (⇑f) μ
This theorem states that for any measure space `X` with a corresponding topological space and open measurable space structures, along with a measure `μ` on `X`, and any normed additive commutative group `E` with a second countable topology, a measurable space structure, and a Borel space structure, if `μ` is a finite measure, then any bounded continuous function `f` from `X` to `E` is integrable with respect to `μ`. Being integrable means that the function is almost everywhere strongly measurable and has a finite integral.
More concisely: For any finite measure `μ` on a measure space `(X, Σ)` with a corresponding topological space and open measurable space structures, and any second countable normed additive commutative group `(E, +, ||.||)` with a Borel space structure, every bounded continuous function `f : X → E` is integrable with respect to `μ`.
|
BoundedContinuousFunction.lintegral_lt_top_of_nnreal
theorem BoundedContinuousFunction.lintegral_lt_top_of_nnreal :
∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] (μ : MeasureTheory.Measure X)
[inst_2 : MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X NNReal), ∫⁻ (x : X), ↑(f x) ∂μ < ⊤
The theorem `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` states that for any type `X` with structures of a measurable space and a topological space, any measure `μ` on `X` that is finite, and any bounded continuous function `f` from `X` to the nonnegative real numbers (`NNReal`), the Lebesgue integral (also known as the measure-theoretic integral or simply `lintegral`) of the function `f` with respect to the measure `μ` is finite (less than infinity). In other words, the integral over the entire space of a bounded continuous function mapping to nonnegative real numbers, under a finite measure, is guaranteed to be finite.
More concisely: For any measurable space and topological space X with a finite measure μ, and any bounded continuous function f from X to the nonnegative real numbers, the Lebesgue integral of f with respect to μ is finite.
|