MeasureTheory.integral_const
theorem MeasureTheory.integral_const :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
{m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : E), ∫ (x : α), c ∂μ = (↑↑μ Set.univ).toReal • c
The theorem `MeasureTheory.integral_const` states that for any type `α` and a normed additive commutative group `E` that is also a normed space over the real numbers and a complete space, given any measurable space over `α`, a measure `μ` on that measurable space, and a constant `c` of type `E`, the integral of the constant function that assigns `c` to every `α` with respect to the measure `μ` is equal to the real part of the measure of the universal set, scaled by `c`. In mathematical notation, this can be represented as ∫ c dμ = μ(Univ) * c.
More concisely: For any measurable space `(α, Σ, μ)` over a real normed space `E`, the integral of the constant function `c : E` is equal to `c * μ(Univ)`, where `Univ` denotes the universal set.
|
MeasureTheory.integral_congr_ae
theorem MeasureTheory.integral_congr_ae :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {f g : α → G}, μ.ae.EventuallyEq f g → ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
This theorem, named "MeasureTheory.integral_congr_ae", establishes that for any types `α` and `G`, given `G` is a normed additive commutative group and a normed space over the reals, and given a measurable space `α` and a measure `μ` on this space, if we have two functions `f` and `g` from `α` to `G` that are equal almost everywhere (which means they are equal except on a set of `α` with measure zero), then the integral of `f` with respect to `μ` is equal to the integral of `g` with respect to `μ`. This means, the difference between functions on a set of measure zero does not change the value of their integrals.
More concisely: If `f` and `g` are almost everywhere equal measurable functions from a measurable space `(α, μ)` to a normed additive commutative group and normed space over the reals, then they have equal integrals with respect to the measure `μ`.
|
MeasureTheory.integral_mono_measure
theorem MeasureTheory.integral_mono_measure :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {ν : MeasureTheory.Measure α},
μ ≤ ν → ν.ae.EventuallyLE 0 f → MeasureTheory.Integrable f ν → ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
The theorem `MeasureTheory.integral_mono_measure` states that for any measurable space `α`, and any two measures `μ` and `ν` on `α`, if `μ` is less than or equal to `ν`, and a function `f` from `α` to the real numbers is non-negative almost everywhere with respect to `ν` and is integrable with respect to `ν`, then the integral of `f` with respect to `μ` is less than or equal to the integral of `f` with respect to `ν`. In other words, if a measure increases, then the integral with respect to that measure does not decrease, as long as the function being integrated is non-negative almost everywhere.
More concisely: If `μ` is a measure less than or equal to `ν` on measurable space `α`, and `f` is a non-negative integrable function with respect to `ν`, then `∫f dμ ≤ ∫f dν`.
|
MeasureTheory.integral_sum_measure
theorem MeasureTheory.integral_sum_measure :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {ι : Type u_7}
{x : MeasurableSpace α} {f : α → G} {μ : ι → MeasureTheory.Measure α},
MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) →
∫ (a : α), f a ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫ (a : α), f a ∂μ i
This theorem states that, for any type `α`, a type `G` that forms a normed addition commutative group and also a normed space over real numbers, a type `ι` (which is used as an index type for a family of measures), a measurable space `x`, a function `f` from `α` to `G`, and a family of measures `μ` indexed by `ι`: if the function `f` is integrable with respect to the sum of the measures `μ`, then the integral of `f` with respect to the sum of the measures `μ` is equal to the sum (taken over all `i` in `ι`) of the integral of `f` with respect to each measure `μ i`. In other words, the integral of a function over a sum of measures is equal to the sum of integrals of the function over each measure, as long as the function is integrable over the sum of measures.
More concisely: If `f` is an integrable function from a type `α` to a normed additive commutative group `G` over real numbers, and `μ` is a family of measures indexed by `ι`, then the integral of `f` with respect to the sum of `μ` equals the sum of integrals of `f` with respect to each `μ_i`.
|
MeasureTheory.integral_undef
theorem MeasureTheory.integral_undef :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {f : α → G}, ¬MeasureTheory.Integrable f μ → ∫ (a : α), f a ∂μ = 0
The theorem `MeasureTheory.integral_undef` states that for any types `α` and `G`, where `G` is a normed additive commutative group and also a normed space over the real numbers `ℝ`, given a measurable space `m` on `α`, a measure `μ` on this measurable space, and a function `f` from `α` to `G`, if `f` is not integrable with respect to the measure `μ` (i.e., `f` is not measurable or the integral `∫⁻ a, ‖f a‖ ∂μ` is not finite), then the integral of `f` with respect to the measure `μ` is equal to zero. This theorem basically says that the integral of a function that is not integrable is defined to be zero.
More concisely: If a function from a measurable space to a normed additive commutative group over the real numbers is not integrable with respect to a given measure, then its integral is equal to the zero element of the group.
|
MeasureTheory.lintegral_coe_eq_integral
theorem MeasureTheory.lintegral_coe_eq_integral :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → NNReal),
MeasureTheory.Integrable (fun x => ↑(f x)) μ → ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)
This theorem, `MeasureTheory.lintegral_coe_eq_integral`, states that for any type `α`, a measurable space `m` of type `α`, a measure `μ` on this measurable space, and a function `f` from `α` to nonnegative real numbers, if the function obtained by taking the nonnegative real number output of `f` and considering it as a real number is integrable (i.e., it is measurable and has a finite integral), then the Lebesgue integral of the function `f` (after considering its output as a real number) with respect to the measure `μ` equals to the extended nonnegative real number obtained by considering the real number integral of the function `f` (after considering its output as a real number) with respect to the measure `μ`. If the real number integral is negative, it will be considered as zero.
More concisely: For any measurable function `f` from a measurable space `(α, m)` to nonnegative real numbers, if the real number integral of `|f|` with respect to the measure `μ` is finite, then `∫(f dμ) = ‛{∫(x dμ) : x ∈ ℝ | x = ∥f(x)∥}‛`, where `∥f(x)∥` denotes the nonnegative real number output of `f` at `x`.
|
MeasureTheory.integral_add
theorem MeasureTheory.integral_add :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {f g : α → G},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ → ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ
The theorem `MeasureTheory.integral_add` states that for any measure space `α` and any normed add commutative group `G` together with its normed space over the reals, given a measure `μ` on the space `α` and two functions `f` and `g` from `α` to `G`, if both `f` and `g` are integrable with respect to the measure `μ`, then the integral of the sum of `f` and `g` with respect to `μ` is equal to the sum of the integrals of `f` and `g` with respect to `μ`. In mathematical terms, this can be written as $\int (f(a) + g(a)) d\mu = \int f(a) d\mu + \int g(a) d\mu$ for all `a` in `α` when `f` and `g` are integrable. This is a statement of linearity of the integral in the space of integrable functions.
More concisely: For any measure space and normed add commutative group, if two integrable functions from the space to the group are given, then their integrals with respect to the measure are equal to the sum of their individual integrals.
|
MeasureTheory.weightedSMul_union
theorem MeasureTheory.weightedSMul_union :
∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (s t : Set α),
MeasurableSet s →
MeasurableSet t →
↑↑μ s ≠ ⊤ →
↑↑μ t ≠ ⊤ →
s ∩ t = ∅ →
MeasureTheory.weightedSMul μ (s ∪ t) =
MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul μ t
The theorem `MeasureTheory.weightedSMul_union` states that, given a measure space `α`, a normed add commutative group `F` over the real numbers, and a measure `μ` over `α`, for any two measurable sets `s` and `t` within `α` such that their measures are not infinite and they have no common elements (i.e., their intersection is empty), then the weighted sum of the measure of the union of `s` and `t` (which is calculated by applying the continuous linear map `MeasureTheory.weightedSMul`) is equal to the sum of the weighted sums of the measures of `s` and `t` individually. The weighting in this context is performed by the measure function `μ`.
More concisely: For measurable sets `s` and `t` in a measure space `α` with finite, non-empty, disjoint measures under a measure function `μ` over `α` and a normed add commutative group `F` over the real numbers, `MeasureTheory.weightedSMul (μ, s ∪ t) = MeasureTheory.weightedSMul (μ, s) + MeasureTheory.weightedSMul (μ, t)`.
|
MeasureTheory.SimpleFunc.integral_congr
theorem MeasureTheory.SimpleFunc.integral_congr :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_1 : NormedSpace ℝ E] {f g : MeasureTheory.SimpleFunc α E},
MeasureTheory.Integrable (↑f) μ →
μ.ae.EventuallyEq ↑f ↑g → MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.integral μ g
The theorem `MeasureTheory.SimpleFunc.integral_congr` states that for any two simple functions `f` and `g` mapping from a measurable space `α` into a normed add commutative group `E`, and a measure `μ` on the measurable space `α`, if `f` is integrable with respect to `μ` and `f` equals `g` almost everywhere (i.e., except on a set of measure zero) with respect to `μ`, then the Bochner integral of `f` with respect to `μ` equals the Bochner integral of `g` with respect to `μ`. This theorem ensures that the Bochner integral is well-defined even when we change the function on a set of measure zero.
More concisely: If simple functions `f` and `g` on measurable space `α` with values in a normed add commutative group `E`, and measure `μ` are such that `f` is integrable, `f = g` almost everywhere with respect to `μ`, then `∫(f dμ) = ∫(g dμ)`.
|
MeasureTheory.integral_toReal
theorem MeasureTheory.integral_toReal :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ → (∀ᵐ (x : α) ∂μ, f x < ⊤) → ∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal
This theorem states that for any measure space `α` with measure `μ` and for any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if `f` is almost everywhere measurable and `f` is finite almost everywhere, then the integral of the real part of `f` with respect to `μ` is equal to the real part of the integral of `f` with respect to `μ`. In other words, we can interchange the operation of taking the real part of a function with the operation of integrating that function, under certain conditions.
More concisely: If `f` is an almost everywhere finite and measurable function from a measure space `(α, μ)` to the extended nonnegative real numbers `ENNReal`, then the real parts of `∫(f dμ)` and `∫(Re(f) dμ)` are equal.
|
MeasureTheory.integral_zero_measure
theorem MeasureTheory.integral_zero_measure :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
(f : α → G), ∫ (x : α), f x ∂0 = 0
This theorem states that for any type `α` and normed additive commutative group `G`, if we have a function `f` mapping from `α` to `G` and `m` as a measurable space of `α`, then the integral of the function `f` with respect to the zero measure is always zero. Here the integral is defined over a measure theory space.
More concisely: For any type `α`, normed additive commutative group `G`, measurable space `m` over `α`, and function `f` from `α` to `G`, the integral of `f` over `m` is zero if the measure of `m` is zero.
|
MeasureTheory.weightedSMul_apply
theorem MeasureTheory.weightedSMul_apply :
∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
(μ : MeasureTheory.Measure α) (s : Set α) (x : F), (MeasureTheory.weightedSMul μ s) x = (↑↑μ s).toReal • x
The theorem `MeasureTheory.weightedSMul_apply` states that for any measurable space `α`, any normed add commutative group `F` that is also a normed space over real numbers, any measure `μ` on `α`, any set `s` of type `α`, and any element `x` of the group `F`, the application of the function `MeasureTheory.weightedSMul μ s` to `x` is equal to the scalar multiplication of `x` by the real-valued measure of the set `s` under measure `μ`. In mathematical terms, if `μ` is a measure on a measurable space and `s` is a set in that space, then, for each `x` in a normed add commutative group that is a normed space over the reals, applying the continuous linear map given by `MeasureTheory.weightedSMul μ s` to `x` results in the same output as scaling `x` by the real value of the measure of `s` under `μ`.
More concisely: For any measurable space `α`, normed add commutative group `F` over real numbers, measure `μ` on `α`, set `s` of `α`, and `x` in `F`, `MeasureTheory.weightedSMul μ s x = μ(s) * x`.
|
MeasureTheory.integral_nonneg
theorem MeasureTheory.integral_nonneg :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ}, 0 ≤ f → 0 ≤ ∫ (a : α), f a ∂μ
The theorem `MeasureTheory.integral_nonneg` states that for any measurable space `α`, any measure `μ` on that space, and any function `f` from `α` to the real numbers, if `f` is nonnegative (i.e., `f(a) ≥ 0` for all `a` in `α`), then the integral of `f` with respect to the measure `μ` is also nonnegative. In other words, if a function is nonnegative everywhere in a measurable space, then its integral over that space (under any measure) cannot be negative.
More concisely: If `μ` is a measure on the measurable space `α` and `f: α → ℝ` is a nonnegative measurable function, then `∫f dμ ≥ 0`.
|
MeasureTheory.integral_smul
theorem MeasureTheory.integral_smul :
∀ {α : Type u_1} {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] {G : Type u_5} [inst_1 : NormedAddCommGroup G]
[inst_2 : NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : NormedSpace 𝕜 G]
[inst_4 : SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G), ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ
This theorem, `MeasureTheory.integral_smul`, states that for any type `α`, a type `𝕜` which is a non-trivially normed field, a type `G` which is a normed commutative add group, and where `G` is a normed space over both `ℝ` (the real numbers) and `𝕜`, given a measurable space `m`, a measure `μ` on that space, and given that `G` is a scalar multiplication commutative class under `ℝ` and `𝕜`, then for any scalar constant `c` from `𝕜` and any function `f` from `α` to `G`, the integral of the scaled function `c • f` with respect to measure `μ` is equal to `c` scaled by the integral of function `f` with respect to measure `μ`. In mathematical notation, ∫ c • f dμ = c • ∫ f dμ.
More concisely: For any normed field `𝕜`, normed commutative add group `G` over `𝕜` and `ℝ`, measurable space `(m, μ)`, and scalar multiplication commutative class `G` under `𝕜` and `ℝ`, the integral of `c • f` with respect to `μ` equals `c` times the integral of `f` with respect to `μ` for any scalar `c` in `𝕜` and measurable function `f` from a type `α` to `G`.
|
MeasureTheory.integral_trim
theorem MeasureTheory.integral_trim :
∀ {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {β : Type u_7} {m m0 : MeasurableSpace β}
{μ : MeasureTheory.Measure β} (hm : m ≤ m0) {f : β → G},
MeasureTheory.StronglyMeasurable f → ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
This theorem, `MeasureTheory.integral_trim`, states that for any type `G` that is a normed additive commutative group and a normed space over the real numbers, any types `β`, any measurable spaces `m` and `m0` for the type `β`, and any measure `μ` on this measurable space, whenever `m` is a sub-measurable space of `m0`, the integral of a strongly measurable function `f` (a function that is the limit of simple functions) with respect to `μ` is equal to the integral of `f` with respect to the measure `μ` trimmed over `m` (i.e., restricted to the smaller measurable space `m`). Effectively, the theorem is saying that for these specific function and space types, integrating over a whole space or a subspace doesn't change the value of the integral if the function is strongly measurable.
More concisely: For any normed additive commutative group `G` and normed space over the real numbers, any measurable spaces `m` and `m0`, any measure `μ` on `m0`, and any strongly measurable function `f` on `m`, the integral of `f` with respect to `μ` equals the integral of `f` with respect to the trimmed measure `μ` on the sub-measurable space `m`.
|
MeasureTheory.integral_non_aestronglyMeasurable
theorem MeasureTheory.integral_non_aestronglyMeasurable :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {f : α → G}, ¬MeasureTheory.AEStronglyMeasurable f μ → ∫ (a : α), f a ∂μ = 0
The theorem `MeasureTheory.integral_non_aestronglyMeasurable` states that for any type `α`, and for any `G` which is a normed add commutative group and a normed space over the real numbers, given a measurable space `m` and a measure `μ` on `α`, and a function `f` from `α` to `G`, if `f` is not almost everywhere strongly measurable with respect to measure `μ`, then the integral of `f` with respect to `μ` is zero. In other words, if a function cannot be approximated almost everywhere by a sequence of simple functions, its integral is zero.
More concisely: If a function from a measurable space to a normed add commutative group, with respect to a given measure, is not almost everywhere strongly measurable, then its integral with respect to that measure is zero.
|
MeasureTheory.integral_eq_zero_iff_of_nonneg_ae
theorem MeasureTheory.integral_eq_zero_iff_of_nonneg_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE 0 f → MeasureTheory.Integrable f μ → (∫ (x : α), f x ∂μ = 0 ↔ μ.ae.EventuallyEq f 0)
This theorem states that for a given measurable space `α` and a measure `μ` on that space, if a function `f : α → ℝ` is nonnegative almost everywhere (with respect to `μ`) and is integrable with respect to `μ`, then the integral of `f` with respect to `μ` is equal to zero if and only if `f` is zero almost everywhere (with respect to `μ`). In other words, under these conditions, the integral being zero is equivalent to the function being zero almost everywhere.
More concisely: For a measurable space `(α, Σ, μ)` and a nonnegative, integrable function `f : α → ℝ` with respect to `μ`, the equality of their integrals, `∫(α, Σ, μ, f) = 0`, holds if and only if `f` is almost everywhere equal to zero.
|
MeasureTheory.SimpleFunc.integral_eq_lintegral
theorem MeasureTheory.SimpleFunc.integral_eq_lintegral :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ℝ},
MeasureTheory.Integrable (↑f) μ →
μ.ae.EventuallyLE 0 ↑f →
MeasureTheory.SimpleFunc.integral μ f = (∫⁻ (a : α), ENNReal.ofReal (↑f a) ∂μ).toReal
The theorem `MeasureTheory.SimpleFunc.integral_eq_lintegral` states that for any measurable space `α`, measure `μ` on `α`, and simple function `f` from `α` to the non-negative real numbers `ℝ`, if `f` is integrable with respect to `μ` and is almost everywhere less than or equal to zero, then the Bochner integral of `f` with respect to `μ` is equal to the integral of `f` as a function into the extended non-negative real numbers `ℝ≥0∞`, coerced back into the real numbers using the function `ENNReal.ofReal`. This theorem essentially bridges the gap between two types of integrals: the Bochner integral and the Lebesgue integral, under certain conditions.
More concisely: For any measurable space, measure, and simple measurable function satisfying certain conditions, the Bochner integral of the function equals the Lebesgue integral treated as a function into the extended non-negative real numbers and coerced back into the real numbers.
|
MeasureTheory.integral_dirac'
theorem MeasureTheory.integral_dirac' :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
[inst_2 : MeasurableSpace α] (f : α → E) (a : α),
MeasureTheory.StronglyMeasurable f → ∫ (x : α), f x ∂MeasureTheory.Measure.dirac a = f a
The theorem `MeasureTheory.integral_dirac'` states that for any given type `α` and `E`, where `E` is a normed additive commutative group and a normed space over the reals `ℝ`, and where `E` is a complete space, and `α` is a measurable space, if we have a function `f` from `α` to `E` that is strongly measurable (that is, it is the limit of a sequence of simple functions), then the integral of `f` with respect to the Dirac measure at any point `a` in `α` is equal to the value of `f` at `a`. In other words, the integral of a strongly measurable function over the Dirac measure centered at a point is simply the value of the function at that point.
More concisely: If `α` is a measurable space, `E` is a complete, normed additive commutative group and normed space over the reals, `f: α → E` is strongly measurable, then ∫₡α(ds) f(s) = f(s) for all s in α. (The integral represents the integral of `f` with respect to the Dirac measure at point `s`.)
|
MeasureTheory.norm_integral_le_integral_norm
theorem MeasureTheory.norm_integral_le_integral_norm :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (f : α → G), ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ
The theorem `MeasureTheory.norm_integral_le_integral_norm` states that for any normed additive commutative group `G` and any normed space `G` over the reals `ℝ`, given a measurable space `α` and a measure `μ` on that space, the norm of the integral of a function `f` from `α` to `G` with respect to `μ` is less than or equal to the integral of the norm of `f` with respect to `μ`. This is a formal statement of the inequality of integrals in the context of measure theory, and it is a specific instance of the more general principle that the "size" of the integral (as measured by the norm) is controlled by the integral of the "sizes" (norms) of the function values.
More concisely: For any measurable space `(α, Σ, μ)`, normed additive commutative group `G` over the reals `ℝ`, and measurable function `f : α → G`, the integral of the norm of `f` with respect to `μ` is greater than or equal to the norm of the integral of `f` with respect to `μ`. (The theorem in the given statement is actually the negative of this, which is why the inequality is reversed.)
|
MeasureTheory.integral_exp_pos
theorem MeasureTheory.integral_exp_pos :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [hμ : NeZero μ],
MeasureTheory.Integrable (fun x => (f x).exp) μ → 0 < ∫ (x : α), (f x).exp ∂μ
The theorem `MeasureTheory.integral_exp_pos` states that for any measurable space `α`, measure `μ` on that space, and function `f` from `α` to real numbers, assuming `μ` is not a zero measure, if the function `exp(f(x))` is integrable with respect to measure `μ`, then the integral of `exp(f(x))` with respect to `μ` is always strictly greater than zero. In other words, the integral of the exponential of a function over a non-zero measure space is always positive if that exponential function is integrable.
More concisely: If `μ` is a non-zero measure on measurable space `α` and `exp(∫(f(x) dμ(x)))` is integrable with respect to `μ`, then `∫(exp(f(x)) dμ(x)) > 0`.
|
MeasureTheory.dominatedFinMeasAdditive_weightedSMul
theorem MeasureTheory.dominatedFinMeasAdditive_weightedSMul :
∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x : MeasurableSpace α}
(μ : MeasureTheory.Measure α), MeasureTheory.DominatedFinMeasAdditive μ (MeasureTheory.weightedSMul μ) 1
The theorem `MeasureTheory.dominatedFinMeasAdditive_weightedSMul` states that for any measurable space `α` and any normed additive commutative group `F` that is a normed space over the real numbers, given a measure `μ` on `α`, the function `weightedSMul μ` is `DominatedFinMeasAdditive` with respect to `μ` and constant 1. In other words, the `weightedSMul` function, which scales elements of `F` by the real measure of a given set, respects the addition of measurable sets and the norm of the result for any measurable set is less than or equal to the measure of the set itself.
More concisely: For any measurable space (α, Σ), normed additive commutative group (F, +) as a real normed space, and measure μ on Σ, the weighted scaling function weightedSMul μ : Σ → F is dominated finitely additive with respect to μ and constant 1.
|
MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg
theorem MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : ℝ},
p.IsConjExponent q →
∀ {f g : α → ℝ},
μ.ae.EventuallyLE 0 f →
μ.ae.EventuallyLE 0 g →
MeasureTheory.Memℒp f (ENNReal.ofReal p) μ →
MeasureTheory.Memℒp g (ENNReal.ofReal q) μ →
∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
This theorem is a version of Hölder's inequality for real-valued functions on a measure space. It states that for any measure space `α`, and any two nonnegative functions `f` and `g` on that space, if `p` and `q` are conjugate exponents (`p.IsConjExponent q`), then the integral of the product of `f` and `g` is bounded above by the product of the `ℒp` seminorm of `f` and the `ℒq` seminorm of `g`.
More specifically, if `f` and `g` are almost everywhere nonnegative with respect to measure `μ` and belong to the spaces `ℒp` and `ℒq` respectively, then the integral of `f * g` with respect to `μ` is less than or equal to `(∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)`. Here `ℒp` and `ℒq` are spaces of functions that are almost everywhere strongly measurable and the `ℒp` (or `ℒq`) seminorm of the function is finite.
More concisely: For any measure space, and two nonnegative, almost everywhere defined functions with finite `ℒp` and `ℒq` seminorms, their product's integral is bounded above by the product of their `ℒp` and `ℒq` seminorms, with `p` and `q` being conjugate exponents.
|
MeasureTheory.integral_add_measure
theorem MeasureTheory.integral_add_measure :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α} {f : α → G},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable f ν → ∫ (x : α), f x ∂(μ + ν) = ∫ (x : α), f x ∂μ + ∫ (x : α), f x ∂ν
The theorem `MeasureTheory.integral_add_measure` states that for any given types `α` and `G` where `G` is a normed additive commutative group and also a normed space over real numbers, and `α` is endowed with a measurable space structure `m`, given two measures `μ` and `ν` on `α`, and for any function `f` from `α` to `G`, if `f` is integrable with respect to both `μ` and `ν`, then the integral of `f` with respect to the sum of measures `μ` and `ν` is equal to the sum of the integral of `f` with respect to `μ` and the integral of `f` with respect to `ν`. In other words, the integral of `f` over the sum measure is the sum of the integrals over the individual measures.
More concisely: For measurable functions between a normed additive commutative group endowed with two measures, the integral of the function with respect to the sum of the measures equals the sum of the integrals with respect to each measure.
|
MeasureTheory.SimpleFunc.integral_eq_lintegral'
theorem MeasureTheory.SimpleFunc.integral_eq_lintegral' :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
{f : MeasureTheory.SimpleFunc α E} {g : E → ENNReal},
MeasureTheory.Integrable (↑f) μ →
g 0 = 0 →
(∀ (b : E), g b ≠ ⊤) →
MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map (ENNReal.toReal ∘ g) f) =
(∫⁻ (a : α), g (↑f a) ∂μ).toReal
This theorem states that for any measurable space `α`, any type `E` that forms a normed additive commutative group, and any measure `μ` on `α`, if we have a simple function `f` from `α` to `E` and a function `g` from `E` to the extended nonnegative real numbers (`ENNReal`), then the Bochner integral of the simple function obtained by applying the function `g` (followed by the coercion from `ENNReal` to the real numbers) to `f` is equal to the Lebesgue integral of the function `g ∘ f`, provided that `f` is integrable, `g` of zero is zero, and `g` never takes the value `∞`. In mathematical terms, it states that
\[
\int f dμ = \int g(f) dμ,
\]
where the left-hand side is the Bochner integral and the right-hand side is the Lebesgue integral. This provides a connection between these two different types of integrals.
More concisely: The Bochner integral of a measurable, integrable simple function from a measurable space to a normed additive commutative group, when composed with a real-valued function satisfying certain conditions, equals the Lebesgue integral of the composed function.
|
MeasureTheory.integral_sub
theorem MeasureTheory.integral_sub :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {f g : α → G},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ → ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ
The theorem `MeasureTheory.integral_sub` states that for any type `α`, and any normed additive commutative group `G` which is also a normed space over the real numbers, given a measure space `m`, a measure `μ` on that space, and two functions `f` and `g` which are both integrable with respect to `μ`, the integral of the difference between `f` and `g` with respect to `μ` is equal to the difference between the integral of `f` and the integral of `g` with respect to `μ`. In mathematical terms, this can be written as: for all `α`, `G`, `m`, `μ`, `f`, and `g`, if `f` and `g` are both integrable functions, then ∫(f(a) - g(a))dμ = ∫f(a)dμ - ∫g(a)dμ.
More concisely: For any normed additive commutative group `G` over the real numbers, measure space `m`, measure `μ`, and integrable functions `f` and `g` on `m` with values in `G`, we have ∫(f(a) - g(a))dμ = ∫f(a)dμ - ∫g(a)dμ.
|
MeasureTheory.integral_pos_iff_support_of_nonneg
theorem MeasureTheory.integral_pos_iff_support_of_nonneg :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
0 ≤ f → MeasureTheory.Integrable f μ → (0 < ∫ (x : α), f x ∂μ ↔ 0 < ↑↑μ (Function.support f))
The theorem `MeasureTheory.integral_pos_iff_support_of_nonneg` states that for any measurable space `α`, measure `μ` on `α`, and a real-valued function `f` on `α` that is nonnegative (i.e., `f`'s value is greater than or equal to zero for all `x` in `α`), if `f` is integrable with respect to `μ`, then the integral of `f` with respect to `μ` is positive if and only if the measure of the support of `f` is positive. The "support" of a function is defined as the set of points where the function does not equal zero.
More concisely: For a measurable space `(α, Σ, μ)`, a nonnegative measurable function `f` on `α`, and if the integral of `f` with respect to `μ` is finite, then the integral is positive if and only if the measure of the support of `f` is positive.
|
MeasurableEmbedding.integral_map
theorem MeasurableEmbedding.integral_map :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {β : Type u_7} {x : MeasurableSpace β} {f : α → β},
MeasurableEmbedding f → ∀ (g : β → G), ∫ (y : β), g y ∂MeasureTheory.Measure.map f μ = ∫ (x : α), g (f x) ∂μ
The theorem `MeasurableEmbedding.integral_map` states that for any types `α`, `G`, and `β`, where `G` is a normed additive commutative group and also a normed space over real numbers, and `α` and `β` are associated with measurable spaces, given a measure `μ` over the measurable space `α`, a measurable embedding function `f` from `α` to `β`, and a function `g` from `β` to `G`, the integral of `g` with respect to the measure induced by `f` and `μ` on `β` is equal to the integral of the composition of `g` and `f` with respect to the measure `μ` on `α`. Here, integration is defined in the sense of measure theory.
More concisely: For measurable spaces `α`, `β`, a normed additive commutative group and normed space `G` over real numbers, measure `μ` on `α`, measurable embedding function `f: α → β`, and function `g: β → G`, the integral of `g` with respect to the measure induced by `f` and `μ` on `β` equals the integral of `g ∘ f` with respect to `μ` on `α`.
|
MeasureTheory.ofReal_integral_norm_eq_lintegral_nnnorm
theorem MeasureTheory.ofReal_integral_norm_eq_lintegral_nnnorm :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {P : Type u_7} [inst : NormedAddCommGroup P]
{f : α → P}, MeasureTheory.Integrable f μ → ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
This theorem states that for any measurable space `α`, any measure `μ` on `α`, any normed additively commutative group `P`, and any function `f` from `α` to `P` that is integrable with respect to `μ`, the extended non-negative real number obtained by applying the `ofReal` function to the integral (over `α`) of the norm of `f` is equal to the integral (over `α`) of the non-negative part of the norm of `f`. In other words, when you integrate the norm of `f` and then apply the `ofReal` function, it is the same as if you first apply the non-negative part function to the norm of `f` and then integrate.
More concisely: For any measurable space `α`, measure `μ`, normed additively commutative group `P`, integrable function `f` from `α` to `P`, the integral of the norm of `f` with respect to `μ` equals the integral of the non-negative part of the norm of `f` with respect to `μ`, when considered as real numbers using `ofReal`.
|
MeasureTheory.SimpleFunc.map_integral
theorem MeasureTheory.SimpleFunc.map_integral :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
(f : MeasureTheory.SimpleFunc α E) (g : E → F),
MeasureTheory.Integrable (↑f) μ →
g 0 = 0 →
MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map g f) =
f.range.sum fun x => (↑↑μ (↑f ⁻¹' {x})).toReal • g x
The theorem `MeasureTheory.SimpleFunc.map_integral` states that for any measure space `α`, and any normed additive commutative groups `E` and `F` (which are also normed spaces over `ℝ`), given a measurable space `m`, a measure `μ` on that space, a simple function `f` mapping from `α` to `E`, and a function `g` mapping from `E` to `F`, if `f` is integrable with respect to `μ` and `g` at `0` is `0`, then the integral of the function `g ∘ f` (which maps from `α` to `F`) is equal to the sum, over the range of `f`, of the product of real-valued measure of the preimage of each value in the range under `f`, and the value of `g` at that point. This sum is calculated using the `Finset.sum` function in Lean, which sums up the values of a given function over a finite set.
More concisely: For any measurable function `f: α -> E` from a measure space `(α, μ)` to a normed additive commutative group `E` over `ℝ`, and any function `g: E -> F` mapping from `E` to another normed space `F` over `ℝ` with `g(0) = 0`, the integral of `g ∘ f` over `α` with respect to `μ` equals the sum, over the range of `f`, of the product of the measure of `f^(-1)(x)` and `g(x)`.
|
MeasureTheory.integral_mono
theorem MeasureTheory.integral_mono :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → f ≤ g → ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
The theorem `MeasureTheory.integral_mono` states that for any two real-valued functions `f` and `g` defined on a measurable space `α` and with a given measure `μ`, if both `f` and `g` are integrable (which means they are measurable and their integral over the measure space is finite), and if `f` is pointwise less than or equal to `g`, then the integral of `f` with respect to `μ` is less than or equal to the integral of `g` with respect to `μ`. In other words, this theorem ensures the monotonicity property of the integral: if `f` is less than or equal to `g` everywhere, then the area under the graph of `f` is less than or equal to the area under the graph of `g`.
More concisely: If two real-valued, measurable functions `f` and `g` on a measurable space `(α, μ)` are integrable and `f ≤ g` pointwise, then ∫(α, μ, f) ≤ ∫(α, μ, g).
|
MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero
theorem MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {ι : Type u_6} {f : α → G},
MeasureTheory.HasFiniteIntegral f μ →
∀ {l : Filter ι} {s : ι → Set α},
Filter.Tendsto (↑↑μ ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (nhds 0)
The theorem `MeasureTheory.HasFiniteIntegral.tendsto_set_integral_nhds_zero` states that if a function `f` has a finite integral with respect to a measure `μ`, then the integral of `f` over a set `s`, denoted as `∫ x in s, f x ∂μ`, is absolutely continuous in `s`. In more detail, it means that as the measure of the set `s` tends to zero, the integral of `f` over `s` also tends to zero. This is true for any sequence of sets `s` whose measures converge to zero in some filter `l`. The integral is taken with respect to the function `f` and the measure `μ`, both of which are assumed to satisfy certain conditions, including that `f` has a finite integral.
More concisely: If a function has a finite integral with respect to a measure, then the integral over any set of zero measure tends to zero as the set shrinks in any filter.
|
MeasureTheory.integral_mul_norm_le_Lp_mul_Lq
theorem MeasureTheory.integral_mul_norm_le_Lp_mul_Lq :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_7} [inst : NormedAddCommGroup E]
{f g : α → E} {p q : ℝ},
p.IsConjExponent q →
MeasureTheory.Memℒp f (ENNReal.ofReal p) μ →
MeasureTheory.Memℒp g (ENNReal.ofReal q) μ →
∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)
The theorem `MeasureTheory.integral_mul_norm_le_Lp_mul_Lq` is a statement of Hölder's inequality in the context of measure theory. It states that for two functions `f` and `g` from a measurable space `α` to a normed additive commutative group `E`, and two real numbers `p` and `q` that are conjugate exponents, if `f` is in the `ℒp` space and `g` is in the `ℒq` space under a measure `μ`, then the integral of the product of their norms is less than or equal to the product of their `ℒp` and `ℒq` seminorms. More formally, if `f` and `g` are almost everywhere strongly measurable and their seminorms are finite, then `∫ ‖f(a)‖ * ‖g(a)‖ dμ ≤ (∫ ‖f(a)‖^p dμ)^(1/p) * (∫ ‖g(a)‖^q dμ)^(1/q)`.
More concisely: For two almost everywhere strongly measurable functions \(f, g : \alpha \to E\) on a measurable space \((\alpha, \mu)\) with finite seminorns, and conjugate exponents \(p, q > 1\), the integral of their product's norms is less than or equal to the product of their \(L^p\) and \(L^q\) seminorms: \(\int \| f(a) \| * \| g(a) \| d\mu \leq \| f \|_{L^p} * \| g \|_{L^q}\).
|
MeasureTheory.integral_eq_lintegral_of_nonneg_ae
theorem MeasureTheory.integral_eq_lintegral_of_nonneg_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE 0 f →
MeasureTheory.AEStronglyMeasurable f μ → ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
The theorem `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` states that for any type `α`, a measure space `m` over `α`, a measure `μ` on that measure space, and a function `f` mapping from `α` to real numbers, if the function `f` is nonnegative almost everywhere with respect to the measure `μ` and `f` is "almost everywhere strongly measurable" with respect to `μ`, then the integral of `f` with respect to `μ` is equal to the real part of the extended nonnegative real (ENNReal) integral of `f` with respect to `μ`.
In more intuitive terms, this theorem relates two types of integrals: the regular integral and the "extended nonnegative real" integral, asserting that under specific conditions, they yield the same result. The conditions specified are that the function being integrated is nonnegative almost everywhere (i.e., except on a set of measure zero) and that it is "almost everywhere strongly measurable", meaning it is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: If a real-valued function on a measure space is nonnegative almost everywhere and almost everywhere strongly measurable, then its regular integral and extended nonnegative real integral equal each other.
|
MeasureTheory.integral_nonpos_of_ae
theorem MeasureTheory.integral_nonpos_of_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE f 0 → ∫ (a : α), f a ∂μ ≤ 0
This theorem states that for any type `α`, measurable space `m`, measure `μ` on that measurable space, and any real-valued function `f` defined on `α`, if `f` is less than or equal to zero almost everywhere (i.e., except possibly on a set of measure zero) with respect to measure `μ`, then the integral of `f` with respect to `μ` is less than or equal to zero. Essentially, it posits that if a function is non-positive almost everywhere, then its integral can't be positive.
More concisely: If a real-valued function defined on a measurable space is almost everywhere non-positive with respect to a given measure, then its integral with respect to that measure is less than or equal to zero.
|
MeasureTheory.integral_neg
theorem MeasureTheory.integral_neg :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (f : α → G), ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ
This theorem, `MeasureTheory.integral_neg`, states that for any measure space `α`, any normed add commutative group `G`, any normed space over reals `ℝ` with `G` as the base set, any measurable space `m`, and any measure `μ`, the integral of the negative of a function `f` over the measure `μ` is equal to the negative of the integral of the function `f` over the measure `μ`. In mathematical terms, it says that ∫ -f dμ = -∫ f dμ.
More concisely: For any measurable function `f` on a measure space `(α, Σ, μ)` over a normed add commutative group `G` with normed space `ℝ`, the integral of `-f` with respect to `μ` equals the negative of the integral of `f` with respect to `μ`, that is, ∫ -`f` d`μ` = -∫ `f` d`μ`.
|
MeasureTheory.integral_sub'
theorem MeasureTheory.integral_sub' :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {f g : α → G},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ → ∫ (a : α), (f - g) a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ
The theorem `MeasureTheory.integral_sub'` states that for any measurable space `α`, normed additively commutative group `G`, normed space over reals `ℝ` and `G`, measure `μ` on the measurable space `α`, and two functions `f` and `g` from `α` to `G`, if both `f` and `g` are integrable with respect to measure `μ`, then the integral of the difference function `(f - g)` with respect to measure `μ` is equal to the difference of the integrals of `f` and `g` with respect to measure `μ`. In mathematical terms, this is stating that ∫ (f - g) dμ = ∫ f dμ - ∫ g dμ, given that both `f` and `g` are integrable.
More concisely: If measurable functions `f` and `g` from a measurable space to a normed additively commutative group, integrable with respect to a measure `μ`, then ∫(f - g) dμ = ∫fdμ - ∫gdμ.
|
MeasureTheory.integral_nonneg_of_ae
theorem MeasureTheory.integral_nonneg_of_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE 0 f → 0 ≤ ∫ (a : α), f a ∂μ
This theorem, `MeasureTheory.integral_nonneg_of_ae`, states that for any measurable space `α` and a measure `μ` on this space, if a function `f` from `α` to the real numbers is nonnegative almost everywhere (with respect to the measure `μ`), then the integral of `f` with respect to `μ` is also nonnegative. In more mathematical terms, it says that if `0 ≤ f` almost everywhere in the measure space `(α, μ)`, then `0 ≤ ∫ f dμ`.
More concisely: If `f: α → ℝ` is a measurable and nonnegative almost everywhere function on the measurable space `(α, μ)`, then `∫ f dμ ≥ 0`.
|
MeasureTheory.integral_mono_ae
theorem MeasureTheory.integral_mono_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ → μ.ae.EventuallyLE f g → ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
This theorem, named `MeasureTheory.integral_mono_ae`, asserts that for any measurable space `α` and any measure `μ` on `α`, if two real-valued functions `f` and `g` on `α` are both integrable with respect to `μ`, and `f` is less than or equal to `g` almost everywhere with respect to `μ`, then the integral of `f` with respect to `μ` is less than or equal to the integral of `g` with respect to `μ`. In other words, if `f` and `g` are both measurable and have finite integrals, and `f` is almost always less than or equal to `g`, then the area under the graph of `f` is less than or equal to the area under the graph of `g`.
More concisely: If `μ` is a measure on the measurable space `α`, `f` and `g` are integrable real-valued functions on `α` with respect to `μ`, and `f(x) ≤ g(x)` almost everywhere on `α` with respect to `μ`, then `∫f dμ ≤ ∫g dμ`.
|
MeasureTheory.integral_pos_iff_support_of_nonneg_ae
theorem MeasureTheory.integral_pos_iff_support_of_nonneg_ae :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE 0 f → MeasureTheory.Integrable f μ → (0 < ∫ (x : α), f x ∂μ ↔ 0 < ↑↑μ (Function.support f))
This theorem states that for any measurable space `α` with a measure `μ` and a function `f : α → ℝ`, if the function `f` is non-negative almost everywhere (i.e., except on a set of measure zero), and if `f` is integrable with respect to `μ`, then the value of the integral of `f` over `α` is positive if and only if the measure of the support of `f` (the set of points where `f` is not zero) is positive. In other words, this theorem relates the positivity of the integral of a non-negative, integrable function to the positivity of the measure of its support.
More concisely: A non-negative, integrable function on a measurable space with respect to a measure has a positive integral if and only if its support has positive measure.
|
MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part
theorem MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ →
∫ (a : α), f a ∂μ =
(∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
The theorem `MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part` states that for any measurable space `α`, any measure `μ` on `α`, and any real-valued function `f : α → ℝ` that is measurable with a finite integral, the Bochner integral of `f` with respect to `μ` is equal to the difference between the integral of the nonnegative part of `f` and the integral of the nonnegative part of the negation of `f`. Here, the nonnegative part of a real number `x` is `x` itself if `x` is nonnegative, and `0` otherwise. The integral of a function's nonnegative part considers only the contributions from the regions where the function is nonnegative.
More concisely: For any measurable space `α`, measure `μ` on `α`, and measurable real-valued function `f` with finite integral, the Bochner integral of `f` equals the difference between the integrals of its nonnegative part and the nonnegative part of `-f`.
|
MeasureTheory.L1.integral_def
theorem MeasureTheory.L1.integral_def :
∀ {α : Type u_5} {E : Type u_6} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
MeasureTheory.L1.integral f = MeasureTheory.L1.integralCLM f
This theorem states that for any normed additive commutative group `E`, measurable space `α`, measure `μ` on `α`, and for any function `f` in the L1 space (i.e., the space of Lebesgue-integrable functions), the Bochner integral of `f` (calculated using the `MeasureTheory.L1.integral` function) is equal to the value of `f` under the continuous linear map `MeasureTheory.L1.integralCLM`. In other words, it confirms that the Bochner integral in L1 space can be computed as a continuous linear map over the real numbers.
More concisely: For any normed additive commutative group `E`, measurable space `α`, measure `μ` on `α`, and `f` in the L1 space, the Bochner integral of `f` equals the value of the continuous linear map `MeasureTheory.L1.integralCLM` applied to `f`.
|
MeasureTheory.integral_mul_left
theorem MeasureTheory.integral_mul_left :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [inst : RCLike L] (r : L)
(f : α → L), ∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ
This theorem, `MeasureTheory.integral_mul_left`, states that for any type `α`, measurable space `m` on `α`, measure `μ` on `m`, type `L` that behaves like the real numbers, and a real number `r`, the integral of the function `f` (from `α` to `L`) multiplied by `r` with respect to the measure `μ` is equal to `r` multiplied by the integral of `f` with respect to `μ`. Essentially, this theorem is expressing the property of integrals where the integral of a constant times a function is equal to the constant times the integral of the function, often known as the "linearity" property of integrals.
More concisely: For any measurable space `(α, m)`, measure `μ` on `m`, type `L` of real numbers, and function `f : α → L` that is integrable with respect to `μ`, the integral of `r * f` with respect to `μ` equals `r * (∫(f)dμ)`.
|
MeasureTheory.integral_mono_of_nonneg
theorem MeasureTheory.integral_mono_of_nonneg :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
μ.ae.EventuallyLE 0 f →
MeasureTheory.Integrable g μ → μ.ae.EventuallyLE f g → ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
The theorem `MeasureTheory.integral_mono_of_nonneg` states that for any measurable space `α` with a measure `μ`, and any two functions `f` and `g` from `α` to the real numbers such that `f` is almost everywhere nonnegative with respect to `μ` and `g` is integrable with respect to `μ`, if `f` is almost everywhere less than or equal to `g` with respect to `μ`, then the integral of `f` with respect to `μ` is less than or equal to the integral of `g` with respect to `μ`. In simpler terms, this theorem is about the monotonicity of the integral for almost everywhere nonnegative functions.
More concisely: If `f` is a measurable, almost everywhere nonnegative function and integrable with respect to measure `μ` on measurable space `α`, and `f ≤ g` almost everywhere with respect to `μ` for another integrable function `g`, then `∫(f dμ) ≤ ∫(g dμ)`.
|
MeasureTheory.integral_smul_measure
theorem MeasureTheory.integral_smul_measure :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (f : α → G) (c : ENNReal), ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ
This theorem, `MeasureTheory.integral_smul_measure`, states that for any type `α`, a normed additively commutative group `G`, a normed space over the reals, a measurable space `m` defined on `α`, a measure `μ` defined on `α`, a function `f : α → G`, and an extended nonnegative real number `c`, the integral of `f` with respect to the measure `c` times `μ` is equal to `c` (converted to a real number) times the integral of `f` with respect to `μ`. This is a key result that ensures the stability of integration under multiplication by an extended nonnegative real number.
More concisely: For any measurable function `f : α → G`, measure `μ` on `α`, extended nonnegative real number `c`, the integral `∫(c * f dμ)` equals `c * ∫(f dμ)` in the real numbers.
|
MeasureTheory.Integrable.tendsto_set_integral_nhds_zero
theorem MeasureTheory.Integrable.tendsto_set_integral_nhds_zero :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {ι : Type u_6} {f : α → G},
MeasureTheory.Integrable f μ →
∀ {l : Filter ι} {s : ι → Set α},
Filter.Tendsto (↑↑μ ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (nhds 0)
This theorem, `MeasureTheory.Integrable.tendsto_set_integral_nhds_zero`, states that if a function `f` is integrable with respect to a measure `μ`, then the integral of `f` over a set `s`, denoted as `∫ x in s, f x ∂μ`, has the property of absolute continuity with respect to `s`. In particular, as the measure of the set `s`, denoted by `μ s`, tends towards zero, the integral of `f` over `s` also tends towards zero. This is captured in the condition that `Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (nhds 0)`, meaning that as `s` shrinks to a point under the filter `l`, the integral over `s` also converges to zero in the neighborhood of zero.
More concisely: If a function is integrable with respect to a measure, then the integral over any set of zero measure tends to zero as the set shrinks to a point.
|
MeasureTheory.ofReal_integral_eq_lintegral_ofReal
theorem MeasureTheory.ofReal_integral_eq_lintegral_ofReal :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ →
μ.ae.EventuallyLE 0 f → ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
This theorem states that for any measurable space `α`, and any real-valued function `f` defined on `α`, under the measure `μ`, if `f` is integrable and is almost everywhere nonnegative (i.e. `f` takes nonnegative values except possibly on a set of measure zero), then the extended nonnegative real part (obtained by treating all negative values as zero) of the integral of `f` over `μ` is equal to the integral over `μ` of the extended nonnegative real part of `f`. This essentially states that the process of taking the integral and the process of taking the extended nonnegative real part can be interchanged under the given conditions.
More concisely: If `μ` is a measure on measurable space `α`, `f` is a real-valued integrable and almost everywhere nonnegative function on `α`, then the integral of the extended nonnegative real part of `f` over `μ` equals the extended nonnegative real part of the integral of `f` over `μ`.
|
MeasureTheory.integral_dirac
theorem MeasureTheory.integral_dirac :
∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [hE : CompleteSpace E]
[inst_2 : MeasurableSpace α] [inst_3 : MeasurableSingletonClass α] (f : α → E) (a : α),
∫ (x : α), f x ∂MeasureTheory.Measure.dirac a = f a
The theorem `MeasureTheory.integral_dirac` states that for any normed add commutative group `E`, which is also a normed space over the real numbers ℝ and is complete, and for any measurable singleton space `α`, if we have a function `f : α → E` and an element `a` in `α`, then the integral of `f` with respect to the dirac measure at `a` is simply the value of the function at `a`. In other words, the integration of a function over a dirac measure at a point is just the evaluation of the function at that point.
More concisely: For any complete normed add commutative group `E` over ℝ, any measurable singleton space `α`, and function `f : α → E` with an element `a` in `α`, the integral of `f` with respect to the dirac measure at `a` equals `f a`.
|
MeasureTheory.integral_zero
theorem MeasureTheory.integral_zero :
∀ (α : Type u_1) (G : Type u_5) [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}, ∫ (x : α), 0 ∂μ = 0
This theorem states that for any type `α`, and any normed additive commutative group `G` that is also a normed space over the real numbers, given a measurable space `m` and a measure `μ` on that space, the integral over all `x` in `α` of the constant function 0 with respect to the measure `μ` is 0. In simpler terms, it's stating that if you integrate the constant zero function over any measure space, you'll always get zero irrespective of the space and the measure.
More concisely: For any normed additive commutative group `G` over the real numbers, and any measurable space `(α, m)`, the integral of the constant function 0 with respect to measure `μ` is equal to 0.
|
MeasureTheory.integral_def
theorem MeasureTheory.integral_def :
∀ {α : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {x : MeasurableSpace α}
(μ : MeasureTheory.Measure α) (f : α → G),
MeasureTheory.integral μ f =
if x_1 : CompleteSpace G then
if hf : MeasureTheory.Integrable f μ then MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf)
else 0
else 0
This theorem is about the definition of the Bochner integral in measure theory. If `G` is a complete space, and the function `f` from `α` to `G` is integrable with respect to measure `μ`, then the Bochner integral of `f` with respect to `μ` is the integral in the L1 space of the equivalence class of `f`. In other words, it's the integral of the function as it is represented in the L1 space (which is a space of equivalence classes of integrable functions). If `G` is not a complete space, or if `f` is not integrable, then the Bochner integral of `f` is defined to be zero.
More concisely: If `G` is a complete space and `f` is an integrable function from `α` to `G` with respect to measure `μ`, then the Bochner integral of `f` is the integral of its equivalence class in the L1 space. Otherwise, it is zero.
|
MeasureTheory.MeasurePreserving.integral_comp
theorem MeasureTheory.MeasurePreserving.integral_comp :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {β : Type u_7} {x : MeasurableSpace β} {f : α → β} {ν : MeasureTheory.Measure β},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ (g : β → G), ∫ (x : α), g (f x) ∂μ = ∫ (y : β), g y ∂ν
The theorem states that for any two types `α` and `β`, a normed additively commutative group `G`, a normed space over the real numbers `ℝ` and `G`, and a measurable space `m` associated with `α`. Given a measure `μ` on `α`, another measurable space `x` associated with `β`, a function `f` from `α` to `β`, and a measure `ν` on `β`, if the function `f` preserves measure from `μ` to `ν` and is a measurable embedding, then for any function `g` from `β` to `G`, the integral of `g` composed with `f` with respect to `μ` is equivalent to the integral of `g` with respect to `ν`. In mathematical notation, this is expressed as: if `f` is a measure-preserving measurable embedding, then `∫ g(f(x)) dμ = ∫ g(y) dν`.
More concisely: If `f: α → β` is a measure-preserving measurable embedding between measurable spaces `(α, μ)` and `(β, ν)`, and `g: β → G` is a function from `β` to a normed additively commutative group `G`, then the integral of `g ∘ f` with respect to `μ` is equal to the integral of `g` with respect to `ν`.
|
MeasureTheory.SimpleFunc.integral_eq_sum_of_subset
theorem MeasureTheory.SimpleFunc.integral_eq_sum_of_subset :
∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_2 : DecidablePred fun x => x ≠ 0] {f : MeasureTheory.SimpleFunc α F}
{s : Finset F},
Finset.filter (fun x => x ≠ 0) f.range ⊆ s →
MeasureTheory.SimpleFunc.integral μ f = s.sum fun x => (↑↑μ (↑f ⁻¹' {x})).toReal • x
The theorem `MeasureTheory.SimpleFunc.integral_eq_sum_of_subset` states that for any measurable space `α`, and any Normed Additive Commutative Group `F` which is also a Normed Space over the real numbers, given a measure `μ` on `α`, a simple function `f` from `α` to `F`, and a finite set `s` of elements from `F`, if the filtered range of `f` (excluding zero) is a subset of `s`, then the Bochner integral of `f` with respect to `μ` is equal to the sum over `s`, where each element `x` in `s` contributes `(μ (f ⁻¹' {x})).toReal • x` to the sum. Here `(f ⁻¹' {x})` denotes the preimage of `x` under `f`, and `•` denotes scalar multiplication in the Normed Space `F`.
More concisely: For any measurable space `α`, Normed Additive Commutative Group `F` over real numbers as a Normed Space, measure `μ` on `α`, simple function `f` from `α` to `F`, finite set `s` of elements from `F`, if the filtered range of `f` (excluding zero) is a subset of `s`, then the Bochner integral of `f` with respect to `μ` equals the sum of elements in `s` weighted by the product of their measures under the inverse image of each element and the element itself.
|
MeasureTheory.integral_map
theorem MeasureTheory.integral_map :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {β : Type u_7} [inst_2 : MeasurableSpace β] {φ : α → β},
AEMeasurable φ μ →
∀ {f : β → G},
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map φ μ) →
∫ (y : β), f y ∂MeasureTheory.Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ
This theorem, `MeasureTheory.integral_map`, states that for any types `α`, `G`, and `β`, with `G` being a normed addition commutative group and also a normed space over the real numbers, and given a measurable space `m` on `α`, a measure `μ` on that space, and a function `φ` from `α` to `β` that is almost everywhere measurable, then for any function `f` from `β` to `G` that is almost everywhere strongly measurable with respect to the pushforward measure of `φ` applied to `μ`, the integral of `f` with respect to the pushforward measure equals the integral of the composition of `f` and `φ` with respect to the original measure `μ`. In other words, the theorem states that the integral of a function over the image of a measure under a transformation is equal to the integral of the composed function over the original measure, provided the conditions of almost everywhere measurability are met.
More concisely: For any measurable space `(α, μ)`, normed additive commutative group and normed space `(G, ||||)` over the real numbers, almost everywhere measurable function `φ: α → β`, almost everywhere strongly measurable function `f: β → (G, ||||)`, and almost everywhere measurable measure `ν = φ_\*μ`, the integral of `f` with respect to `ν` equals the integral of `f ∘ φ` with respect to `μ`.
|
MeasureTheory.mul_meas_ge_le_integral_of_nonneg
theorem MeasureTheory.mul_meas_ge_le_integral_of_nonneg :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE 0 f →
MeasureTheory.Integrable f μ → ∀ (ε : ℝ), ε * (↑↑μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ
The theorem, named as "Markov's inequality" or "Chebyshev's first inequality", postulates that for a measurable space `α` with measure `μ` and a function `f : α → ℝ` that is almost everywhere non-negative (with respect to the measure `μ`) and integrable with respect to `μ`, for any real number `ε`, the product of `ε` and the measure of the set of elements in `α` where `f` takes on a value greater than or equal to `ε` is less than or equal to the integral of `f` over `α` with respect to the measure `μ`. In mathematical notation, if `f(x) ≥ 0` for almost all `x` and `f` is integrable, then for any `ε > 0`, we have `ε * μ({x | f(x) ≥ ε}) ≤ ∫ f dμ`.
More concisely: For any measurable space with measure and a non-negative, integrable function, the measure of the set where the function exceeds a given real number is less than or equal to the integral of the function multiplied by that number.
|
MeasureTheory.tendsto_integral_of_L1
theorem MeasureTheory.tendsto_integral_of_L1 :
∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {ι : Type u_6} (f : α → G),
MeasureTheory.Integrable f μ →
∀ {F : ι → α → G} {l : Filter ι},
(∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) →
Filter.Tendsto (fun i => ∫⁻ (x : α), ↑‖F i x - f x‖₊ ∂μ) l (nhds 0) →
Filter.Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (nhds (∫ (x : α), f x ∂μ))
The theorem `MeasureTheory.tendsto_integral_of_L1` states that if a sequence of functions `F i` converges to a function `f` in the `L1` norm, then the integral of `F i` with respect to a measure `μ` converges to the integral of `f` with respect to the same measure. Here, the `L1` convergence is specified in two parts: every function `F i` in the sequence is `Integrable` with respect to `μ` (almost everywhere), and the `L1` norm of the difference between `F i` and `f`, integrated over the whole space, tends to `0`. Convergence of the integrals means that for any neighborhood of the integral of `f`, there is a point in the filter (which can be thought of as a "large enough index" in the sequence) beyond which all the integrals of `F i` fall in that neighborhood.
More concisely: If a sequence of Integrable functions `F i` with respect to measure `μ` converges to a function `f` in `L1` norm, then the integrals of `F i` with respect to `μ` converge to the integral of `f` with respect to `μ`.
|