MeasureTheory.hasFiniteIntegral_def
theorem MeasureTheory.hasFiniteIntegral_def :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {x : MeasurableSpace α} (f : α → β)
(μ : MeasureTheory.Measure α), MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
The theorem `MeasureTheory.hasFiniteIntegral_def` states that for any types `α` and `β`, where `β` is a normed add commutative group, any measurable space `α`, any function `f` from `α` to `β`, and any measure `μ` on `α`, the function `f` has a finite integral with respect to measure `μ` if and only if the Lebesgue integral over `α` of the nonnegative extended real norm of `f` with respect to measure `μ` is less than infinity. This theorem provides a precise mathematical definition of what it means for a function to have a finite integral in measure theory.
More concisely: A measurable function from a measurable space to a normed add commutative group has a finite integral with respect to a measure if and only if the Lebesgue integral of the function's nonnegative extended real norm is finite.
|
MeasureTheory.Integrable.measure_gt_lt_top
theorem MeasureTheory.Integrable.measure_gt_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → ↑↑μ {a | ε < f a} < ⊤
This theorem states that if a real-valued function `f` is integrable with respect to a measure `μ`, then for any real number `c` greater than zero, the measure of the set of points where `f` exceeds `c` is finite. In other words, the set of points where the function exceeds a positive threshold has finite measure, which is one of the properties associated with integrable functions.
More concisely: If a real-valued function `f` is integrable with respect to measure `μ`, then the set `{x | f(x) > c}` has finite measure for any positive real number `c`.
|
MeasureTheory.Integrable.neg
theorem MeasureTheory.Integrable.neg :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (-f) μ
The theorem `MeasureTheory.Integrable.neg` states that for any measurable space `α`, any type `β` that forms a normed additive commutative group, any measure `μ` on the space `α`, and any function `f` from `α` to `β`, if `f` is integrable with respect to the measure `μ`, then the function `-f` (the function that maps each element of `α` to the negation of the corresponding element of `β` under `f`) is also integrable with respect to the measure `μ`.
More concisely: If `μ` is a measure on measurable space `α` and `f` is a integrable function from `α` to a normed additive commutative group `β`, then the function `-f` is also integrable with respect to `μ`.
|
MeasureTheory.Integrable.add
theorem MeasureTheory.Integrable.add :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f g : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (f + g) μ
The theorem `MeasureTheory.Integrable.add` states that for any two functions `f` and `g` from a set `α` to a normed additively commutative group `β`, with `α` being a measurable space and `μ` being a measure on `α`, if `f` and `g` are both integrable with respect to measure `μ`, then their sum `f + g` is also integrable with respect to the same measure. This means that the sum of two integrable functions is again an integrable function.
More concisely: If `f` and `g` are integrable functions from a measurable space `(α, μ)` to a normed additively commutative group `β`, then their sum `f + g` is also integrable on `(α, μ)`.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.1
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f : α → β), MeasureTheory.HasFiniteIntegral f μ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤)
This theorem in the Lean 4 library, `Mathlib.MeasureTheory.Function.L1Space._auxLemma.1`, states that for any types `α` and `β`, and for any measurable space `α` with a measure `μ`, and `β` being a normed add commutative group, a function `f` from `α` to `β` has a finite integral with respect to the measure `μ` if and only if the Lebesgue integral over this measure space of the nonnegative part of the norm of `f` is less than infinity. In simpler terms, the function `f` has a finite integral under the measure `μ` when the integral of the non-negative value of the norm of `f` is finite. This theorem links the concept of having a finite integral with the finitude of the integral of the norm, using the `ENNReal.ofReal` function to ensure non-negativity.
More concisely: A measurable function from a measure space to a normed add commutative group has a finite integral if and only if the integral of the non-negative part of its norm is finite.
|
MeasureTheory.Integrable.smul
theorem MeasureTheory.Integrable.smul :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{𝕜 : Type u_5} [inst_1 : NormedAddCommGroup 𝕜] [inst_2 : SMulZeroClass 𝕜 β] [inst_3 : BoundedSMul 𝕜 β] (c : 𝕜)
{f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (c • f) μ
The theorem `MeasureTheory.Integrable.smul` states that, for any given measurable space `α`, a measure `μ` on `α`, a normed additive commutative group `β`, a type `𝕜` which forms a normed additive commutative group and has a scalar multiplication with `β` that is both zero-preserving and bounded, and any scalar `c` of type `𝕜`, if a function `f` from `α` to `β` is integrable with respect to the measure `μ`, then the function obtained by scalar multiplication of `f` by `c` is also integrable with respect to the same measure `μ`. In mathematical terms, this theorem asserts that the integrability property is preserved under scalar multiplication in the context of measure theory.
More concisely: If `f` is an integrable function from a measurable space `(α, μ)` to a normed additive commutative group `β`, and `c` is a scalar in a normed additive commutative group `𝕜` with scalar multiplication preserving integrability, then `c • f` is an integrable function.
|
MeasureTheory.hasFiniteIntegral_norm_iff
theorem MeasureTheory.hasFiniteIntegral_norm_iff :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f : α → β), MeasureTheory.HasFiniteIntegral (fun a => ‖f a‖) μ ↔ MeasureTheory.HasFiniteIntegral f μ
The theorem `MeasureTheory.hasFiniteIntegral_norm_iff` states that for any types `α` and `β`, with `α` being a measurable space and `μ` being a measure on `α`, and `β` being a normed add commutative group, a function `f` from `α` to `β` has a finite integral with respect to the measure `μ` if and only if the function that assigns the norm of `f(a)` to each `a` in `α` also has a finite integral with respect to `μ`. In other words, the finiteness of the integral of `f` and the finiteness of the integral of the norm of `f` are equivalent.
More concisely: The theorem `MeasureTheory.hasFiniteIntegral_norm_iff` asserts that a measurable function from a measurable space to a normed add commutative group has a finite integral if and only if the function assigning the norm of its values to each point has a finite integral.
|
MeasureTheory.Integrable.essSup_smul
theorem MeasureTheory.Integrable.essSup_smul :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{𝕜 : Type u_5} [inst_1 : NormedField 𝕜] [inst_2 : NormedSpace 𝕜 β] {f : α → β},
MeasureTheory.Integrable f μ →
∀ {g : α → 𝕜},
MeasureTheory.AEStronglyMeasurable g μ →
essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤ → MeasureTheory.Integrable (fun x => g x • f x) μ
This is the statement of Hölder's inequality for integrable functions. It states that, given a measurable space and a measure on this space, and a normed field acting on a normed additively commutative group, if we have an integrable function from the measurable space to the normed group, then for any function from the measurable space to the normed field that is strongly measurable almost everywhere, and whose essential supremum of its norm is finite, the function obtained by pointwise multiplication of these two functions is also integrable. In simpler terms, the scalar multiplication of an integrable vector-valued function by a scalar function with finite essential supremum is integrable.
More concisely: If a measurable function from a measure space to a normed group and a strongly measurable almost everywhere function from the measure space to a normed field have finite essential supremums of their respective norms, then their pointwise product is an integrable function.
|
MeasureTheory.integrable_const_iff
theorem MeasureTheory.integrable_const_iff :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{c : β}, MeasureTheory.Integrable (fun x => c) μ ↔ c = 0 ∨ ↑↑μ Set.univ < ⊤
This theorem states that for any types `α` and `β`, a `measurable space α`, a `measure μ` on `α`, and a `normed add commutative group β`, a constant function `c: β` is integrable with respect to the measure `μ` if and only if either the constant function is zero or the measure of the universal set `Set.univ` is less than infinity. In simpler terms, a function that always returns a constant value is integrable if that constant is zero or if the entire space has finite measure.
More concisely: A constant function from a measurable space to a normed add commutative group is integrable with respect to a measure if and only if the constant value is zero or the measure of the universal set has finite size.
|
MeasureTheory.integrable_map_measure
theorem MeasureTheory.integrable_map_measure :
∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasurableSpace δ] [inst_1 : NormedAddCommGroup β] {f : α → δ} {g : δ → β},
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
AEMeasurable f μ →
(MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ)
The theorem `MeasureTheory.integrable_map_measure` states that for any types `α`, `β`, `δ`, a measurable space `α` denoted by `m`, and a measure `μ` on `α`, along with the conditions that `δ` is a measurable space and `β` is a normed add commutative group, given two functions `f : α → δ` and `g : δ → β`, if `g` is almost everywhere strongly measurable with respect to the pushforward of the measure `μ` by the function `f`, and `f` is almost everywhere measurable with respect to `μ`, then the integrability of `g` with respect to the pushforward measure is equivalent to the integrability of the composition `(g ∘ f)` with respect to the measure `μ`.
In simpler terms, the theorem describes a condition under which the integrability of a function `g` after a measure is transformed by another function `f` is equivalent to the integrability of the composition of `g` and `f` under the original measure.
More concisely: If `f : α → δ` and `g : δ → β` are measurable functions, `μ` is a measure on `α`, and `g` is almost everywhere strongly measurable with respect to the pushforward of `μ` by `f`, then `g` is integrable with respect to the pushforward measure if and only if the composition `g ∘ f` is integrable with respect to `μ`.
|
MeasureTheory.L1.ofReal_norm_sub_eq_lintegral
theorem MeasureTheory.L1.ofReal_norm_sub_eq_lintegral :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f g : ↥(MeasureTheory.Lp β 1 μ)), ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
This theorem, `MeasureTheory.L1.ofReal_norm_sub_eq_lintegral`, states that for any measurable space `α` and normed additive commutative group `β`, given a measure `μ` on `α` and two functions `f` and `g` in the `L¹ (β, μ)` space (which means the functions are absolutely integrable with respect to measure `μ`), the non-negative real part (`ENNReal.ofReal`) of the norm of the difference between the two functions `f - g` is equal to the Lebesgue integral of the non-negative part of the norm of the pointwise difference between `f` and `g`. Note that `(f - g) x` and `f x - g x` are not the same but are almost everywhere-equal.
More concisely: For measurable spaces `α` and normed additive commutative groups `β`, let `μ` be a measure on `α`, `f` and `g` be `L¹ (β, μ)` functions, and `|.|` denote the norm. Then, `∫(ENNReal.ofReal ∣(f - g)∣ dμ) = ∫(ENNReal.ofReal ∣f - g∣^+ dμ)`, where `∣f - g∣^+ = max(∣f - g∣, 0)`.
|
MeasureTheory.integrable_congr
theorem MeasureTheory.integrable_congr :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f g : α → β}, μ.ae.EventuallyEq f g → (MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ)
This theorem states that for any measurable space `α`, any measure `μ` on that space, and any two functions `f` and `g` from `α` to a normed additive commutative group `β`, if `f` and `g` are equal almost everywhere with respect to the measure `μ`, then `f` is integrable with respect to `μ` if and only if `g` is also integrable with respect to `μ`. Here, a function is deemed integrable if it is both measurable and has a finite integral.
More concisely: If two measurable functions from a measurable space to a normed additive commutative group are equal almost everywhere with respect to a measure, then they are both integrable with respect to that measure.
|
MeasureTheory.Integrable.congr
theorem MeasureTheory.Integrable.congr :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f g : α → β}, MeasureTheory.Integrable f μ → μ.ae.EventuallyEq f g → MeasureTheory.Integrable g μ
The theorem `MeasureTheory.Integrable.congr` states that given any two functions `f` and `g` from a measurable space `α` to a normed additive commutative group `β`, and a measure `μ` on the space `α`, if the function `f` is integrable with respect to the measure `μ` and the function `f` equals to the function `g` almost everywhere with respect to the measure `μ`, then the function `g` is also integrable with respect to the measure `μ`. In other words, the integrability of a function is preserved under equality almost everywhere.
More concisely: If two measurable functions from a measurable space to a normed additive commutative group are equal almost everywhere with respect to a measure, and one is integrable, then the other is also integrable.
|
MeasureTheory.Integrable.div_const
theorem MeasureTheory.Integrable.div_const :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜]
{f : α → 𝕜}, MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => f x / c) μ
The theorem `MeasureTheory.Integrable.div_const` states that for any measurable space `α` with a measure `μ`, a type `𝕜` forming a normed division ring, and a function `f : α → 𝕜` that is integrable with respect to `μ`, the function obtained by dividing `f` by any constant `c : 𝕜` is also integrable with respect to `μ`. Essentially, this theorem assures that the integrability property is preserved when a function is divided by a constant.
More concisely: If `α` is a measurable space with measure `μ`, `𝕜` is a normed division ring, and `f : α → 𝕜` is an integrable function, then the function `x mapsto (f x) / c` is integrable for any constant `c ∈ 𝕜`.
|
MeasureTheory.Integrable.measure_le_lt_top
theorem MeasureTheory.Integrable.measure_le_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ → ∀ {c : ℝ}, c < 0 → ↑↑μ {a | f a ≤ c} < ⊤
The theorem `MeasureTheory.Integrable.measure_le_lt_top` states that for any real-valued function `f` which is measurable and has a finite integral on a measure space `(α, m, μ)`, for any real number `c` less than zero, the set of points in `α` where `f` is less than or equal to `c` has finite measure. In other words, if `f` is integrable, then the measure of the set of points where the function value is not greater than a negative number is always finite.
More concisely: If a measurable, real-valued function `f` has finite integral on a measure space, then the set where `f ≤ c` (for any `c` < 0) has finite measure.
|
MeasureTheory.Integrable.measure_ge_lt_top
theorem MeasureTheory.Integrable.measure_ge_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → ↑↑μ {a | ε ≤ f a} < ⊤
This theorem states that if we have a real-valued function `f` that is integrable, then for any positive real number `c`, the set of all elements `x` for which `f(x)` is greater than or equal to `c` has a finite measure. In other words, the size (measure) of the set of all `x` that make `f(x)` larger than some positive number `c` is always finite, provided that the function `f` is integrable.
More concisely: If `f` is an integrable real-valued function, then the set `{x : ℝ | f x ≥ c}` has finite measure for any positive real number `c`.
|
MeasureTheory.Integrable.toL1.proof_1
theorem MeasureTheory.Integrable.toL1.proof_1 :
∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f : α → β), MeasureTheory.Integrable f μ → MeasureTheory.Memℒp f 1 μ
The theorem `MeasureTheory.Integrable.toL1.proof_1` states that for any measurable space `α`, type `β` in a normed add commutative group, a measure `μ` on `α`, and a function `f` from `α` to `β`, if `f` satisfies the condition of `Integrable` under measure `μ`, then `f` also satisfies the condition of `Memℒp` with `p` equal to 1 under the same measure `μ`. That is, if `f` is measurable and has finite integral under measure `μ`, then `f` is almost everywhere strongly measurable and the $L^1$ norm of `f` (which is the integral of the absolute value of `f`) is finite under measure `μ`.
More concisely: If a measurable function `f` from a measurable space `(α, μ)` to a normed add commutative group `β` is integrable with respect to `μ`, then `f` is almost everywhere strongly measurable and its $L^1$ norm is finite under `μ`.
|
MeasureTheory.Integrable.norm
theorem MeasureTheory.Integrable.norm :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun a => ‖f a‖) μ
The theorem `MeasureTheory.Integrable.norm` states that for any measurable space `α`, any normed additive commutative group `β`, any measure `μ` on `α`, and any function `f` from `α` to `β`, if `f` is integrable with respect to `μ`, then the function that maps each element of `α` to the norm of `f` at that element is also integrable with respect to `μ`. In other words, if the function `f` is integrable, then the function that gives the norm of `f` at each point is also integrable.
More concisely: If `f` is a measurable and integrable function from a measurable space `(α, Σ, μ)` to a normed additive commutative group `(β, +, ||·||)`, then the function `x ↦ ||f x||` is integrable on `α` with respect to `μ`.
|
MeasureTheory.integrable_norm_iff
theorem MeasureTheory.integrable_norm_iff :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β},
MeasureTheory.AEStronglyMeasurable f μ →
(MeasureTheory.Integrable (fun a => ‖f a‖) μ ↔ MeasureTheory.Integrable f μ)
The theorem `MeasureTheory.integrable_norm_iff` states that for any given measure `μ` on a measurable space `α`, and a function `f` mapping from `α` to a normed additive commutative group `β`, if the function `f` is almost everywhere strongly measurable with respect to the measure `μ`, then `f` is integrable with respect to `μ` if and only if the norm of `f`, denoted as `‖f a‖`, is integrable with respect to `μ`. Here, integrability means that the function is almost everywhere strongly measurable and has a finite integral.
More concisely: A strongly measurable function `f` from a measurable space `(α, μ)` to a normed additive commutative group `β` is integrable with respect to `μ` if and only if the norm of `f` is integrable with respect to `μ`.
|
MeasureTheory.Integrable.smul_essSup
theorem MeasureTheory.Integrable.smul_essSup :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{𝕜 : Type u_5} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [inst_3 : BoundedSMul 𝕜 β] {f : α → 𝕜},
MeasureTheory.Integrable f μ →
∀ {g : α → β},
MeasureTheory.AEStronglyMeasurable g μ →
essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤ → MeasureTheory.Integrable (fun x => f x • g x) μ
Hölder's inequality for integrable functions states that, given a scalar-valued function `f` and a vector-valued function `g`, if `f` is integrable and `g` is almost everywhere equal to the limit of a sequence of simple functions (i.e., `g` is AEStronglyMeasurable), and the essential supremum of the norm of `g` is finite, then the function resulting from the scalar multiplication of `f` and `g` is also integrable. In more mathematical terms, if `∫⁻ a, ‖f a‖ ∂μ` is finite (where `μ` is a measure and `a` ranges over the domain of `f` and `g`), and if `∃ c, f x ≤ c` almost everywhere (`c` being the essential supremum), then `∫⁻ a, ‖(f a) • (g a)‖ ∂μ` is finite. The theorem holds in a measurable space `m` and for a measure `μ`. The scalar values are of type `𝕜` which is a normed ring with a module structure over `β` and with a bounded scalar multiplication.
More concisely: If `f` is an integrable scalar-valued function, `g` is AEStronglyMeasurable vector-valued function with finite essential supremum norm, and the product `f * g` is pointwise defined, then `f * g` is integrable.
|
MeasureTheory.Integrable.coeFn_toL1
theorem MeasureTheory.Integrable.coeFn_toL1 :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β} (hf : MeasureTheory.Integrable f μ), μ.ae.EventuallyEq (↑↑(MeasureTheory.Integrable.toL1 f hf)) f
This theorem states that for any measurable space `α`, any normed additively commutative group `β`, any measure `μ` on `α`, and any function `f` from `α` to `β`, if `f` is integrable with respect to `μ`, then `f` is "equal almost everywhere" (which is denoted by `=ᶠ[MeasureTheory.Measure.ae μ]`) to the function that we get when we first convert `f` into its equivalence class in the space of integrable functions (i.e., `MeasureTheory.Integrable.toL1 f hf`), and then apply the canonical embedding of that space into the space of all functions from `α` to `β` (i.e., the double coercion `↑↑`). In simpler terms, the function `f` and its integrable representation are the same almost everywhere with respect to the measure `μ`.
More concisely: For any measurable space `α`, measurable function `f` from `α` to a normed additively commutative group `β`, and measure `μ` on `α`, if `f` is integrable with respect to `μ`, then `f =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.Integrable.toL1 f`.
|
MeasureTheory.Integrable.comp_measurable
theorem MeasureTheory.Integrable.comp_measurable :
∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasurableSpace δ] [inst_1 : NormedAddCommGroup β] {f : α → δ} {g : δ → β},
MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) → Measurable f → MeasureTheory.Integrable (g ∘ f) μ
The theorem `MeasureTheory.Integrable.comp_measurable` states that for any types `α`, `β`, and `δ`, given a measurable space `α` with measure `μ`, a measurable space `δ`, a normed add commutative group `β`, a function `f` from `α` to `δ`, and a function `g` from `δ` to `β`, if `g` is integrable with respect to the pushforward measure of `μ` via `f`, and `f` is measurable, then the composition of `g` and `f` (i.e. `g ∘ f`) is integrable with respect to the measure `μ`.
In simpler terms, if we have a measurable transformation `f`, and a function `g` which is integrable when we take into account the change in measure induced by `f`, then the function we get by applying `g` after `f` is integrable in the original measure space.
More concisely: If `f: α → δ` is measurable, `g: δ → β` is integrable with respect to the pushforward measure of `μ` via `f`, then `g ∘ f` is integrable with respect to the measure `μ` on `α`.
|
MeasureTheory.ofReal_toReal_ae_eq
theorem MeasureTheory.ofReal_toReal_ae_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
(∀ᵐ (x : α) ∂μ, f x < ⊤) → μ.ae.EventuallyEq (fun x => ENNReal.ofReal (f x).toReal) f
This theorem states that for any type `α`, measurable space `m`, measure `μ` over that space, and a function `f` that maps from the space `α` to the extended nonnegative real numbers (or ENNReal, usually denoted as [0, ∞]), if it is almost everywhere (with respect to the measure `μ`) that `f(x)` is less than infinity, then the function that maps `x` to the nonnegative real part of `f(x)` is equal to `f` almost everywhere. In other words, we can convert `f(x)` to a real number and then back to extended nonnegative real number without changing the value of `f(x)` almost everywhere.
In the context of measure theory, "almost everywhere" means that the set of points where the condition fails has measure zero. "ENNReal.ofReal (f x).toReal" is the operation of converting `f(x)` to a real number and then back to an extended nonnegative real number. The notation "=ᶠ[MeasureTheory.Measure.ae μ] f" means that the function is equal to `f` except possibly on a set of measure zero (i.e., almost everywhere).
More concisely: If a measurable function `f : α → ENNReal` is almost everywhere finite with respect to measure `μ`, then the pointwise application of the non-negative real part function and `f` are equal almost everywhere.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.37
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.37 : ∀ {r : NNReal}, (↑r = 0) = (r = 0)
This theorem states that for any type `α` and `β`, a measurable space `m` over `α`, a measure `μ` on that measurable space, and a function `f` from `α` to `β` that is almost everywhere strongly measurable with respect to `μ`, the function `f` is integrable (in the sense of `MeasureTheory.AEEqFun.Integrable`) if and only if it is integrable in the sense of `MeasureTheory.Integrable`. In other words, the equivalence class `[f]` of almost everywhere equal functions is integrable if and only if its representative function `f` is integrable. This connects the concept of integrability for almost everywhere equal functions and the more general concept of integrability.
More concisely: For any measurable spaces `α` and `β`, measure `μ` on `α`, almost everywhere strongly measurable function `f` from `α` to `β`, and integrals `∫` and `∫'` denoting integration with respect to `μ` on `α` and almost everywhere equal functions respectively, `f` is `∫'-integrable` if and only if `f` is `∫-integrable`.
|
MeasureTheory.Integrable.measure_lt_lt_top
theorem MeasureTheory.Integrable.measure_lt_lt_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
MeasureTheory.Integrable f μ → ∀ {c : ℝ}, c < 0 → ↑↑μ {a | f a < c} < ⊤
The theorem `MeasureTheory.Integrable.measure_lt_lt_top` asserts that if a real-valued function `f` is integrable, then for any real number `c` less than zero, the measure of the set of all points `x` such that `f(x) < c` is finite. In other words, the set of all points where the value of `f` is less than a given negative number has finite measure, given that `f` is an integrable function. This theorem applies in the context of a measurable space `α`, with a measure `μ` defined on it.
More concisely: If `f` is an integrable real-valued function on a measurable space `(α, μ)`, then for any real number `c` less than zero, the measure of the set `{x ∈ α | f(x) < c}` is finite.
|
IsUnit.integrable_smul_iff
theorem IsUnit.integrable_smul_iff :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{𝕜 : Type u_5} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [inst_3 : BoundedSMul 𝕜 β] {c : 𝕜},
IsUnit c → ∀ (f : α → β), MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
The theorem `IsUnit.integrable_smul_iff` states that for any types `α`, `β`, and `𝕜`, where `α` is a measurable space and `𝕜` is a normed ring that's also a module for `β`, given a measure `μ` on `α` and a normed add commutative group structure on `β`. If `c` is a unit in `𝕜` and `f` is a function from `α` to `β`, then `f` is integrable with respect to the measure `μ` if and only if the function obtained by scaling `f` by `c` is also integrable with respect to `μ`. This means that scaling a function by a unit in the ring does not affect its integrability property.
More concisely: For any measurable space `α`, normed ring `𝕜`, and measure `μ` on `α`, if `c` is a unit in `𝕜` and `f : α → β` is an integrable function with respect to `μ`, then the function `c * f` is also integrable with respect to `μ`. (Here, `β` is a normed add commutative group and `𝕜` is a module over `β`.)
|
MeasureTheory.Integrable.aestronglyMeasurable
theorem MeasureTheory.Integrable.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.AEStronglyMeasurable f μ
The theorem `MeasureTheory.Integrable.aestronglyMeasurable` states that for any type `α`, any measurable space `m` associated with that type, any measure `μ` on that space, any type `β` that forms a normed add commutative group, and any function `f` from `α` to `β`, if the function `f` is integrable with respect to the measure `μ` (meaning that `f` is measurable and the integral over `f` is finite), then `f` is almost everywhere strongly measurable with respect to `μ` (meaning that there exists a sequence of simple functions that leads to `f` almost everywhere).
More concisely: If a function from a measurable space to a normed add commutative group is integrable with respect to a given measure, then it is almost everywhere strongly measurable.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.20
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.20 :
∀ (α : Type u_1) (β : Type u_2) {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : NormedAddCommGroup β],
MeasureTheory.Integrable (fun x => 0) μ = True
This theorem asserts that for any types `α` and `β`, a given measurable space `m` associated with `α`, a measure `μ` also associated with `α`, and an instance of the type class `NormedAddCommGroup` on `β`, the function which maps every element of `α` to the zero element of `β` is integrable with respect to the measure `μ`. In other words, the zero function is always integrable.
More concisely: For any measurable space `(α, m)`, measure `μ` on `α`, and `NormedAddCommGroup` type `β`, the constant function from `α` to the zero element of `β` is integrable with respect to `μ`.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.2
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.2 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, (a < ⊤) = (a ≠ ⊤)
This theorem states that for any type `α` that has a partial ordering and an identified top element (`⊤`), for any element `a` of type `α`, `a` being less than the top element (`⊤`) is equivalent to `a` not being equal to the top element (`⊤`). This is applicable in contexts, such as measure theory, where the top element represents an "infinite" or "maximum" value.
More concisely: For any type `α` with a partial ordering and top element `⊤`, `a < ⊤` if and only if `a ≠ ⊤`.
|
MeasureTheory.L1.integrable_coeFn
theorem MeasureTheory.L1.integrable_coeFn :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f : ↥(MeasureTheory.Lp β 1 μ)), MeasureTheory.Integrable (↑↑f) μ
This theorem states that for any measure space `(α, m, μ)`, and any normed addition commutative group `β`, if `f` is an element of the `Lp` space `L1` for `β` with respect to measure `μ`, then the function `f` (represented by its equivalence class under the almost-everywhere equivalence relation in `↥(MeasureTheory.Lp β 1 μ)`) is integrable. In more mathematical terms, `f` is both almost everywhere strongly measurable and has a finite integral, where the integral is defined as `∫⁻ a, ‖f a‖ ∂μ` and it is finite.
More concisely: If `f` is an `L1` function in the `Lp` space `L1(μ, β)` of a measure space `(α, m, μ)`, then `f` is integrable, i.e., it is almost everywhere measurable and has a finite integral with respect to `μ`.
|
MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top
theorem MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
∫⁻ (x : α), f x ∂μ ≠ ⊤ → MeasureTheory.HasFiniteIntegral (fun x => (f x).toReal) μ
The theorem `MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top` states that for any measurable space `α` with measure `μ`, and any function `f` mapping from `α` to the extended non-negative real numbers (`ENNReal`), if the Lebesgue integral (notated as `∫⁻ (x : α), f x ∂μ`) of `f` with respect to `μ` is not infinite (i.e., `≠ ⊤`), then the function `f` when converted to real numbers (i.e., `(fun x => (f x).toReal)`) has a finite integral. In essence, if a function's integral over a measurable space is finite when using extended nonnegative real numbers, it remains finite when we restrict our attention to real numbers.
More concisely: If a measurable function from a measurable space to extended non-negative real numbers has a finite Lebesgue integral, then its integral over real numbers is also finite.
|
MeasureTheory.L1.norm_sub_eq_lintegral
theorem MeasureTheory.L1.norm_sub_eq_lintegral :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f g : ↥(MeasureTheory.Lp β 1 μ)), ‖f - g‖ = (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ).toReal
This theorem titled `MeasureTheory.L1.norm_sub_eq_lintegral` states that for any two functions `f` and `g` in the L¹ space of a given measure space (represented by measurable space `α` and measure `μ`), the norm of the difference between `f` and `g` is equal to the real part of the integral over the measure space `α` of the nonnegative version of the norm of the difference between the function values `f x` and `g x`. Note that this theorem emphasizes that this is not a special case of `norm_def`, as `(f - g) x` and `f x - g x` are not equal, but are almost everywhere equal.
More concisely: For any measurable functions `f` and `g` on a measure space `(α, μ)` in the L¹ space, the norm of `f - g` is equal to the real part of the integral of the absolute value of `(f x - g x)` over `α` with respect to `μ`.
|
MeasureTheory.AEEqFun.integrable_mk
theorem MeasureTheory.AEEqFun.integrable_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ),
(MeasureTheory.AEEqFun.mk f hf).Integrable ↔ MeasureTheory.Integrable f μ
The theorem `MeasureTheory.AEEqFun.integrable_mk` states that for any measure space `α`, any normed add commutative group `β`, any measurable space `m` derived from `α`, any measure `μ` on `α`, and any function `f` from `α` to `β` which is almost everywhere strongly measurable with respect to `μ`, the equivalence class `[f]` of the function `f` is integrable if and only if the function `f` itself is integrable. Here, integrability of a function means that it is almost everywhere strongly measurable and its integral (the integral of the absolute value of the function) over the given measure is finite.
More concisely: For any measure space, normed add commutative group, measurable space, measure, and almost everywhere strongly measurable function between them, the function is integrable if and only if its equivalence class is integrable.
|
MeasureTheory.Integrable.comp_aemeasurable
theorem MeasureTheory.Integrable.comp_aemeasurable :
∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasurableSpace δ] [inst_1 : NormedAddCommGroup β] {f : α → δ} {g : δ → β},
MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) →
AEMeasurable f μ → MeasureTheory.Integrable (g ∘ f) μ
The theorem `MeasureTheory.Integrable.comp_aemeasurable` states that for any types `α`, `β`, and `δ`, a measurable space `α`, a measure `μ` on `α`, a measurable space `δ`, a normed add commutative group `β`, and functions `f : α → δ` and `g : δ → β`; if `g` is integrable with respect to the pushforward of the measure `μ` by `f`, and if `f` is almost everywhere measurable with respect to `μ`, then the composition `g ∘ f` is integrable with respect to `μ`. In terms of measure theory, this means that the integrability of a function after a measure-preserving transformation is preserved if the transformation is almost everywhere measurable.
More concisely: If a measurable function `f : α → δ` and a integrable function `g : δ → β` satisfy `g` is integrable with respect to the pushforward measure of `μ` by `f` and `f` is almost everywhere measurable with respect to `μ`, then the composition `g ∘ f` is integrable with respect to `μ`.
|
MeasureTheory.HasFiniteIntegral.mono_measure
theorem MeasureTheory.HasFiniteIntegral.mono_measure :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {f : α → β},
MeasureTheory.HasFiniteIntegral f ν → μ ≤ ν → MeasureTheory.HasFiniteIntegral f μ
The theorem `MeasureTheory.HasFiniteIntegral.mono_measure` asserts that for any types `α` and `β`, a measurable space `m` over `α`, measures `μ` and `ν` on `α`, a normed add commutative group over `β`, and a function `f` from `α` to `β`, if the function `f` has a finite integral with respect to the measure `ν` and `μ` is less than or equal to `ν` (i.e., every set that's measurable in `μ` is also measurable in `ν` and `μ` assigns less or equal measure to every set), then `f` also has a finite integral with respect to the measure `μ`. In other words, if the integral of the norm of `f` with respect to `ν` is finite, and the measure `μ` is dominated by `ν`, then the integral of the norm of `f` with respect to `μ` is also finite.
More concisely: If `μ` is a measure dominated by `ν` on a measurable space, and `f` is a measurable function with finite integral with respect to `ν`, then `f` has a finite integral with respect to `μ`.
|
MeasureTheory.HasFiniteIntegral.mono
theorem MeasureTheory.HasFiniteIntegral.mono :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
MeasureTheory.HasFiniteIntegral g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) → MeasureTheory.HasFiniteIntegral f μ
This theorem states that for any types `α`, `β`, and `γ`, where `α` is a measurable space and `μ` is a measure on `α`, if `β` and `γ` form normed additive commutative groups and `f` is a map from `α` to `β` and `g` is a map from `α` to `γ`, if `g` has a finite integral over `μ` and almost everywhere in `α` the norm of `f` at a point is less than or equal to the norm of `g` at that point, then `f` also has a finite integral over `μ`. In mathematical terms, it states that if $\int \|\mathbf{g}(a)\| d\mu < \infty$ and $\|\mathbf{f}(a)\| \leq \|\mathbf{g}(a)\|$ almost everywhere, then $\int \|\mathbf{f}(a)\| d\mu < \infty$.
More concisely: If `μ` is a measure on a measurable space `α`, `f: α → β` and `g: α → γ` are measurable functions with `β` and `γ` normed additive commutative groups, `g` has finite integral over `μ`, and almost everywhere `||f(x)|| ≤ ||g(x)||`, then `f` also has a finite integral over `μ` with respect to the norm of its values.
|
MeasureTheory.integrable_zero
theorem MeasureTheory.integrable_zero :
∀ (α : Type u_1) (β : Type u_2) {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : NormedAddCommGroup β],
MeasureTheory.Integrable (fun x => 0) μ
The theorem `MeasureTheory.integrable_zero` states that for any measurable space `α`, any measure `μ` on that space, and any normed additive commutative group `β`, the zero function (i.e., the function that maps every element to zero) is integrable with respect to `μ`. In more mathematical language, it says that the function `f : α → β` defined by `f(x) = 0` for all `x ∈ α`, is integrable with respect to measure `μ`. This means it is both strongly measurable and has a finite integral.
More concisely: The zero function is integrable with respect to any measure on any measurable space.
|
MeasureTheory.memℒp_one_iff_integrable
theorem MeasureTheory.memℒp_one_iff_integrable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Memℒp f 1 μ ↔ MeasureTheory.Integrable f μ
The theorem `MeasureTheory.memℒp_one_iff_integrable` states that for any measurable space `α`, any normed add commutative group `β`, any measure `μ` on `α`, and any function `f` from `α` to `β`, the function `f` belongs to the space `ℒp` for `p = 1` with respect to the measure `μ` if and only if `f` is integrable with respect to `μ`. In mathematical terms, this is saying that $\langle f, 1, \mu \rangle \in \mathcal{L}^{p}$ if and only if $f$ is $\mu$-integrable. This links the concept of being in the `ℒp` space for `p = 1` with the concept of integrability.
More concisely: A measurable function from a measurable space to a normed add commutative group is integrable with respect to a measure if and only if it belongs to the Lebesgue space with p=1 with respect to that measure.
|
MeasureTheory.HasFiniteIntegral.congr'
theorem MeasureTheory.HasFiniteIntegral.congr' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
MeasureTheory.HasFiniteIntegral f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → MeasureTheory.HasFiniteIntegral g μ
The theorem `MeasureTheory.HasFiniteIntegral.congr'` states that for any types `α`, `β` and `γ`, given a measurable space `α`, a measure `μ` on that space, and two functions `f : α → β` and `g : α → γ` where `β` and `γ` are normed additive commutative groups, if `f` has a finite integral with respect to `μ` and, almost everywhere with respect to `μ`, the norm of `f` at any point `a` is equal to the norm of `g` at `a`, then `g` also has a finite integral with respect to `μ`. In other words, if two functions have their norms equal almost everywhere, and one of them has a finite measure-theoretic integral, then so does the other.
More concisely: If two measurable functions from a measurable space to normed additive commutative groups have equal norms almost everywhere and one of them has a finite integral with respect to a measure on the space, then the other function also has a finite integral with respect to that measure.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.12
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.12 :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), (a ≤ |a|) = True
This theorem, `Mathlib.MeasureTheory.Function.L1Space._auxLemma.12`, states that for any type `α` that has a Lattice structure and an AddGroup structure, any element `a` of this type satisfies the property that `a` is less than or equal to the absolute value of `a`. This is always true, as indicated by the result `True`. In mathematical notation, this can be written as $a \leq |a|$.
More concisely: For any type `α` with Lattice and AddGroup structures, every element `a` satisfies the inequality `|a| ≥ a`. Thus, `a ≤ |a|`.
|
MeasureTheory.Integrable.mono'
theorem MeasureTheory.Integrable.mono' :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β} {g : α → ℝ},
MeasureTheory.Integrable g μ →
MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a) → MeasureTheory.Integrable f μ
The theorem `MeasureTheory.Integrable.mono'` states that for any measurable space `α`, any measure `μ` on `α`, any normed add commutative group `β`, and any two functions `f : α → β` and `g : α → ℝ`, if `g` is integrable with respect to measure `μ`, `f` is almost everywhere strongly measurable with respect to `μ`, and almost everywhere, the norm of `f` is less than or equal to `g`, then `f` is also integrable with respect to `μ`. In other words, if we have a function `g` that is integrable, and another function `f` that is almost everywhere equal to the limit of a sequence of simple functions and is pointwise bounded by `g`, then `f` is also integrable.
More concisely: If a function `f : α → β` is almost everywhere strongly measurable, pointwise bounded by an integrable function `g : α → ℝ` (almost everywhere), then `f` is integrable.
|
MeasureTheory.integrable_const
theorem MeasureTheory.integrable_const :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
[inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : β), MeasureTheory.Integrable (fun x => c) μ
The theorem `MeasureTheory.integrable_const` states that for any types `α` and `β`, with `α` having a measurable space structure and a measure `μ`, and `β` forming a normed additively commutative group, if the measure `μ` is finite, then the constant function mapping every element of `α` to a fixed value `c` in `β` is integrable with respect to the measure `μ`. In other words, a constant function is measurable and its integral over the measure space is finite.
More concisely: For any measurable space `(α, Σ, μ)` with a finite measure `μ`, and any constant function `c : β`, the constant function from `α` to `β` is Σ-integrable.
|
MeasureTheory.Integrable.mul_const
theorem MeasureTheory.Integrable.mul_const :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [inst : NormedRing 𝕜]
{f : α → 𝕜}, MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => f x * c) μ
The theorem `MeasureTheory.Integrable.mul_const` states that for any type `α` with a measurable space structure `m`, any measure `μ` on `α`, any normed ring `𝕜`, and any function `f` from `α` to `𝕜` that is integrable with respect to `μ`, if we multiply `f` by a constant `c` from `𝕜`, the resulting function is also integrable with respect to `μ`. In simple terms, it means that the integrability of a function remains preserved even after multiplying it by a constant.
More concisely: If `f` is an integrable function from a measurable space `(α, m)` to a normed ring `𝕜`, then the function `c → c * f` is integrable for any constant `c` in `𝕜`.
|
MeasureTheory.Integrable.prod_mk
theorem MeasureTheory.Integrable.prod_mk :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (fun x => (f x, g x)) μ
The theorem `MeasureTheory.Integrable.prod_mk` states that for any types `α`, `β`, `γ`, measurable space `m` on `α`, and a measure `μ` on this measurable space, given a normed additive commutative group on `β` and `γ`, and functions `f` and `g` from `α` to `β` and `γ` respectively, if both `f` and `g` are integrable with respect to the measure `μ`, then the function that maps each element of `α` to the tuple `(f x, g x)` is also integrable with respect to the measure `μ`. In more intuitive terms, if two functions are separately integrable, then the function that pairs their outputs is also integrable.
More concisely: If `μ` is a measure on the measurable space `(α, m)`, and `f : α → β` and `g : α → γ` are integrable functions with respect to `μ`, then the function `x ↦ (f x, g x)` from `α` to `β × γ` is integrable with respect to `μ`.
|
MeasureTheory.integrable_toReal_of_lintegral_ne_top
theorem MeasureTheory.integrable_toReal_of_lintegral_ne_top :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
AEMeasurable f μ → ∫⁻ (x : α), f x ∂μ ≠ ⊤ → MeasureTheory.Integrable (fun x => (f x).toReal) μ
The theorem `MeasureTheory.integrable_toReal_of_lintegral_ne_top` states that for all measure spaces `α` with `m` as the measurable space and `μ` as the measure, and for all functions `f` from `α` to the extended nonnegative real numbers (`ENNReal`), if `f` is almost everywhere measurable with respect to `μ` and the Lebesgue integral of `f` with respect to `μ` is not infinite, then the function that sends each `x` from `α` to the real part of `f(x)` is integrable with respect to `μ`. In other words, if a function's values are almost always measurable and its integral is finite, then we can ensure that the real part of this function is integrable.
More concisely: If a measurable function from a measure space to the extended nonnegative real numbers with finite Lebesgue integral has almost everywhere defined real part, then the real part is integrable.
|
MeasureTheory.Integrable.add_measure
theorem MeasureTheory.Integrable.add_measure :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {f : α → β},
MeasureTheory.Integrable f μ → MeasureTheory.Integrable f ν → MeasureTheory.Integrable f (μ + ν)
The theorem `MeasureTheory.Integrable.add_measure` states that for any two measures `μ` and `ν` on a measurable space `α` and any function `f` from `α` to a normed additive commutative group `β`, if `f` is integrable with respect to both `μ` and `ν`, then `f` is also integrable with respect to the measure `μ + ν`, which is the sum of `μ` and `ν`. In other words, the integrability of `f` is preserved under the addition of measures.
More concisely: If measures `μ` and `ν` on measurable space `α` have integrable function `f` with respect to each, then `f` is integrable with respect to their sum `μ + ν`.
|
MeasureTheory.Integrable.sub
theorem MeasureTheory.Integrable.sub :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f g : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (f - g) μ
The theorem `MeasureTheory.Integrable.sub` states that for any measure space `α`, normed addition-commutative group `β`, measurable function `f` and `g` from `α` to `β`, and measure `μ` on `α`, if `f` and `g` are both integrable with respect to `μ`, then the function `f - g` is also integrable with respect to `μ`. In other words, the difference between two integrable functions is also integrable.
More concisely: If `f` and `g` are integrable functions from a measure space to a normed addition-commutative group with respect to a given measure, then their difference `f - g` is also an integrable function.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.18
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.18 :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
(f : α → β), (∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤) = MeasureTheory.HasFiniteIntegral f μ
This theorem states that for any types `α` and `β`, any measurable space `m` on `α`, any measure `μ` on `α`, and any function `f` from `α` to `β` where `β` forms a normed add commutative group, the condition that the extended distance from `f a` to `0` integrated with respect to measure `μ` over all `a` in `α` is finite is equivalent to the function `f` having a finite integral with respect to the measure `μ`. In mathematical terms, it asserts that `∫⁻ (a : α), edist (f a) 0 ∂μ < ∞` is equivalent to `∫⁻ (a : α), ‖f a‖ ∂μ < ∞`.
More concisely: The theorem asserts that for any measurable space, measure, and integrable function between normed add commutative groups, the finite integrability of the extended distance from the function to the origin equals the finite integrability of the function's norm.
|
MeasureTheory.Integrable.mono_measure
theorem MeasureTheory.Integrable.mono_measure :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] {f : α → β}, MeasureTheory.Integrable f ν → μ ≤ ν → MeasureTheory.Integrable f μ
The theorem `MeasureTheory.Integrable.mono_measure` states that for any types `α` and `β`, a measurable space `m` on `α`, measures `μ` and `ν` on the measurable space, a normed add commutative group instance on `β`, and a function `f` from `α` to `β`, if `f` is integrable with respect to measure `ν` and measure `μ` is less than or equal to measure `ν`, then `f` is also integrable with respect to measure `μ`. In other words, the integrability of a function under a certain measure is preserved when we move to a smaller measure.
More concisely: If `μ` is less than or equal to `ν` and `f` is integrable with respect to `ν` on the measurable space `(α, m)` with values in the normed add commutative group `(β, +, ||.||)`, then `f` is integrable with respect to `μ`.
|
MeasureTheory.hasFiniteIntegral_of_bounded
theorem MeasureTheory.hasFiniteIntegral_of_bounded :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
[inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : α → β} {C : ℝ},
(∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C) → MeasureTheory.HasFiniteIntegral f μ
The theorem `MeasureTheory.hasFiniteIntegral_of_bounded` states that for any types `α` and `β`, with `α` having a measurable space structure and `β` a normed add commutative group structure, and for any measure `μ` on `α` which is a finite measure, and for any function `f` from `α` to `β`, and for any real number `C`, if almost every `a` in `α` under measure `μ` has the property that the norm of `f(a)` is less than or equal to `C`, then `f` has a finite integral with respect to measure `μ`. In other words, if a function is almost everywhere bounded by a constant in a finite measure space, then it has a finite integral in that space.
More concisely: If a function from a measurable space with a finite measure to a normed add commutative group is almost everywhere bounded, then it has a finite integral with respect to the measure.
|
MeasureTheory.Integrable.const_mul
theorem MeasureTheory.Integrable.const_mul :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [inst : NormedRing 𝕜]
{f : α → 𝕜}, MeasureTheory.Integrable f μ → ∀ (c : 𝕜), MeasureTheory.Integrable (fun x => c * f x) μ
The theorem `MeasureTheory.Integrable.const_mul` states that, given a measurable space `α`, a measure `μ` on `α`, a normed ring `𝕜`, and a function `f` from `α` to `𝕜`, if `f` is integrable with respect to `μ`, then for any constant `c` in `𝕜`, the function obtained by multiplying `f` by `c` at each point (`c * f x`) is also integrable with respect to `μ`. In other words, the integrability of a function is preserved under scalar multiplication.
More concisely: If `f` is an integrable function from a measurable space `(α, Σ, μ)` to a normed ring `𝕜`, then for any constant `c` in `𝕜`, the function `c * f` is also integrable.
|
MeasureTheory.Integrable.mono
theorem MeasureTheory.Integrable.mono :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
MeasureTheory.Integrable g μ →
MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) → MeasureTheory.Integrable f μ
The theorem `MeasureTheory.Integrable.mono` can be described in natural language as follows:
Given a measurable space `α` with a measure `μ`, and two normed additively commutative groups `β` and `γ`, for any two functions `f` from `α` to `β` and `g` from `α` to `γ`, if `g` is integrable with respect to `μ`, `f` is almost everywhere strongly measurable with respect to `μ`, and almost everywhere, the norm of `f(a)` is less than or equal to the norm of `g(a)` for some `a` in `α`, then `f` is integrable with respect to `μ`.
In simpler terms, this theorem states that if one function (`g`) is integrable and another function (`f`) is almost everywhere strongly measurable and its norm is always less than or equal to the norm of `g`, then `f` is also integrable.
More concisely: If a strongly measurable function `f` satisfies the almost everywhere norm inequality with an integrable function `g`, then `f` is integrable.
|
MeasureTheory.integrable_finset_sum'
theorem MeasureTheory.integrable_finset_sum' :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{ι : Type u_5} (s : Finset ι) {f : ι → α → β},
(∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → MeasureTheory.Integrable (s.sum fun i => f i) μ
The theorem `MeasureTheory.integrable_finset_sum'` states that for any measurable space `α`, measure `μ` on `α`, normed additive commutative group `β`, type `ι`, and finite set `s` of type `ι`, if for every element `i` in `s`, the function `(f i)` is integrable with respect to the measure `μ`, then the function which sums up `f i` for every `i` in the finite set `s` is also integrable with respect to the measure `μ`. In other words, the integrability is preserved under taking finite sums in the context of measure theory.
More concisely: If `μ` is a measure on a measurable space `α`, and `f i` is an integrable function for each `i` in a finite set `s` with respect to `μ`, then the function that sums `f i` for all `i` in `s` is also integrable with respect to `μ`.
|
MeasureTheory.Integrable.hasFiniteIntegral
theorem MeasureTheory.Integrable.hasFiniteIntegral :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.HasFiniteIntegral f μ
The theorem `MeasureTheory.Integrable.hasFiniteIntegral` states that for any measure space `α` with a measure `μ`, any normed add commutative group `β`, and any function `f` from `α` to `β`, if the function `f` is integrable with respect to `μ`, then the integral of the norm of `f` with respect to `μ` is finite. In other words, if `f` satisfies the properties of being measurable and having a finite integral, then the integral `∫⁻ a, ‖f a‖ ∂μ` is finite.
More concisely: If a function from a measure space to a normed add commutative group is integrable, then the integral of the norm of the function is finite.
|
MeasureTheory.Integrable.measure_norm_ge_lt_top
theorem MeasureTheory.Integrable.measure_norm_ge_lt_top :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → ↑↑μ {x | ε ≤ ‖f x‖} < ⊤
This theorem, known as a non-quantitative version of the Markov inequality for integrable functions, states that for any measurable space `α`, any normed additive commutative group `β`, any measure `μ` on `α`, and any function `f` from `α` to `β` that is integrable with respect to `μ`, for all real number `ε` greater than 0, the measure of the set of points `x` where the norm of `f(x)` is greater than or equal to `ε` is finite.
More concisely: For any measurable space `α`, normed additive commutative group `β`, measure `μ` on `α`, and integrable function `f` from `α` to `β`, the set of points `x` in `α` with `||f(x)||_β ≥ ε` has finite measure under `μ` for any `ε > 0`.
|
MeasureTheory.Integrable.measure_norm_gt_lt_top
theorem MeasureTheory.Integrable.measure_norm_gt_lt_top :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ → ∀ {ε : ℝ}, 0 < ε → ↑↑μ {x | ε < ‖f x‖} < ⊤
This theorem is a non-quantitative version of the Markov inequality for integrable functions. It states that for any function `f` mapping from a measure space `α` to a normed commutative addition group `β`, which is integrable with respect to the measure `μ`, the measure of the set of points in `α` where the norm of `f(x)` is greater than a positive real number `ε` is always finite. This is true for every positive `ε`. In other words, the set where `f` significantly deviates from zero by more than `ε` has a finite measure for any positive `ε`.
More concisely: For any integrable function `f` from a measure space to a normed commutative addition group and for any positive real number `ε`, the measure of the set where the norm of `f` exceeds `ε` is finite.
|
Mathlib.MeasureTheory.Function.L1Space._auxLemma.14
theorem Mathlib.MeasureTheory.Function.L1Space._auxLemma.14 :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] [inst_1 : Finite α] [inst_2 : MeasurableSpace α]
[inst_3 : MeasurableSingletonClass α] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ]
(f : α → β), MeasureTheory.Integrable (fun a => f a) μ = True
The theorem `Mathlib.MeasureTheory.Function.L1Space._auxLemma.14` states that for any types `α` and `β`, where `β` is a normed add commutative group, `α` has a finite number of elements and a measurable singleton class, and for any measure `μ` on `α` which is finite, any function `f` from `α` to `β` is integrable. In other words, if a function `f` maps from a finite measurable space `α` to a normed add commutative group `β` and we have a finite measure `μ`, then the function `f` is always integrable with respect to the measure `μ`. This underlines the fact that integrability is a property that always holds when our domain is finite.
More concisely: A function from a finite measurable space to a normed add commutative group is integrable with respect to any finite measure.
|
MeasureTheory.MeasurePreserving.integrable_comp_emb
theorem MeasureTheory.MeasurePreserving.integrable_comp_emb :
∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasurableSpace δ] [inst_1 : NormedAddCommGroup β] {f : α → δ} {ν : MeasureTheory.Measure δ},
MeasureTheory.MeasurePreserving f μ ν →
MeasurableEmbedding f → ∀ {g : δ → β}, MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν
The theorem `MeasureTheory.MeasurePreserving.integrable_comp_emb` states that for any types `α`, `β`, and `δ`, given a measurable space `α`, a measure `μ` on `α`, a measurable space `δ`, a normed additively commutative group `β`, a function `f : α → δ`, and a measure `ν` on `δ`, if `f` is a measure-preserving function from `μ` to `ν` and `f` is a measurable embedding, then for any function `g : δ → β`, the function `g` composed with `f` (`g ∘ f`) is integrable with respect to `μ` if and only if `g` is integrable with respect to `ν`. In simpler terms, it says that under these conditions, the integrability of a function composed with a measure-preserving function is preserved.
More concisely: If `f : α → δ` is a measure-preserving and measurable embedding of measurable spaces with measures `μ` and `ν`, then the integrability of a function `g : δ → β` with respect to `μ` is equivalent to its integrability with respect to `ν`.
|
MeasureTheory.hasFiniteIntegral_iff_ofReal
theorem MeasureTheory.hasFiniteIntegral_iff_ofReal :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
μ.ae.EventuallyLE 0 f → (MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤)
The theorem `MeasureTheory.hasFiniteIntegral_iff_ofReal` states that for any measurable space `α`, any measure `μ` on `α`, and any function `f` from `α` to the real numbers, if the function `f` is nonnegative almost everywhere (with respect to the measure `μ`), then `f` has a finite integral with respect to `μ` if and only if the integral of the nonnegative real extension of `f` is finite. In other words, `f` is integrable in the sense of Lebesgue Integration (i.e., the integral of the absolute value of `f` is finite) if and only if the integral of the nonnegative real part of `f` is finite.
More concisely: For any measurable space, measure, and measurable function, if the function is nonnegative almost everywhere and its nonnegative real extension has a finite integral, then the original function is integrable with respect to the measure.
|
MeasureTheory.HasFiniteIntegral.smul
theorem MeasureTheory.HasFiniteIntegral.smul :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{𝕜 : Type u_5} [inst_1 : NormedAddCommGroup 𝕜] [inst_2 : SMulZeroClass 𝕜 β] [inst_3 : BoundedSMul 𝕜 β] (c : 𝕜)
{f : α → β}, MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (c • f) μ
The theorem `MeasureTheory.HasFiniteIntegral.smul` states that given a type `α` with a measurable space structure `m`, a measure `μ` on `α`, and a target type `β` equipped with a normed commutative additive group structure, if a function `f` from `α` to `β` has a finite integral (meaning the integral of the norm of `f a` is finite), then the function obtained by scaling `f` by a scalar `c` from another normed additive commutative group `𝕜` (which also has a zero product structure and a bounded scalar multiplication with `β`) also has a finite integral. In mathematical terms, if `∫⁻ a, ‖f(a)‖ ∂μ < ∞`, then `∫⁻ a, ‖c * f(a)‖ ∂μ < ∞`.
More concisely: If `f: α → β` is a measurable function with finite integral `∫⁻ a, ‖f(a)‖ dμ < ∞` over a measure space `(α, Σ, m, μ)`, then the scaled function `c * f` also has a finite integral `∫⁻ a, ‖c * f(a)‖ dμ < ∞`, for any scalar `c` in a normed additive commutative group `𝕜` with bounded scalar multiplication on `β`.
|