MeasureTheory.exists_upperSemicontinuous_le_integral_le
theorem MeasureTheory.exists_upperSemicontinuous_le_integral_le :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{μ : MeasureTheory.Measure α} [inst_3 : μ.WeaklyRegular] (f : α → NNReal),
MeasureTheory.Integrable (fun x => ↑(f x)) μ →
∀ {ε : ℝ},
0 < ε →
∃ g,
(∀ (x : α), g x ≤ f x) ∧
UpperSemicontinuous g ∧
MeasureTheory.Integrable (fun x => ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ε ≤ ∫ (x : α), ↑(g x) ∂μ
The theorem states that given an integrable function `f` which takes values in the non-negative real numbers, there exists another function `g` that is upper semicontinuous and less than or equal to `f` such that the integral of `g` is arbitrarily close to the integral of `f`. More precisely, for any positive real number `ε`, there exists such a function `g` that satisfies these properties and also that the difference between the integral of `f` and the integral of `g` is greater than or equal to negative `ε`. This is an auxiliary lemma for the Vitali-Carathéodory theorem.
More concisely: Given an integrable, non-negative function `f`, there exists an upper semicontinuous function `g ≤ f` such that the integral of `g` is arbitrarily close to the integral of `f` with a difference of at least negative `ε`.
|
MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge
theorem MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
(μ : MeasureTheory.Measure α) [inst_3 : μ.WeaklyRegular] [inst_4 : MeasureTheory.SigmaFinite μ] (f : α → NNReal),
Measurable f →
∀ {ε : ENNReal},
ε ≠ 0 →
∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
This theorem states that for any given measurable function `f` with values in the nonnegative real numbers (denoted as `ℝ≥0`) in a sigma-finite space, there exists a lower semicontinuous function `g` that is greater than `f` and whose integral is arbitrarily close to the integral of `f`. More formally, for any non-zero amount `ε`, there exists a function `g` such that for all `x` in the domain, `g(x)` is greater than `f(x)`, `g` is lower semicontinuous, and the Lebesgue integral of `g` with respect to a measure `μ` is less than or equal to the Lebesgue integral of `f` plus `ε`. This theorem is a helper lemma for the Vitali-Carathéodory theorem.
More concisely: For any measurable function `f` with non-negative values in a sigma-finite space, there exists a lower semicontinuous function `g` that is greater than `f` and satisfies the integral of `g` with respect to any measure `μ` being less than or equal to the integral of `f` plus an arbitrary `ε`.
|
MeasureTheory.exists_upperSemicontinuous_lt_integral_gt
theorem MeasureTheory.exists_upperSemicontinuous_lt_integral_gt :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{μ : MeasureTheory.Measure α} [inst_3 : μ.WeaklyRegular] [inst_4 : MeasureTheory.SigmaFinite μ] (f : α → ℝ),
MeasureTheory.Integrable f μ →
∀ {ε : ℝ},
0 < ε →
∃ g,
(∀ (x : α), g x < ↑(f x)) ∧
UpperSemicontinuous g ∧
MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
(∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε
**Vitali-Carathéodory Theorem**: For any given integrable real-valued function `f` defined on a topological space `α`, there exists another integrable function `g` such that `g(x)` is less than `f(x)` for all `x` in `α`. This function `g` is upper semicontinuous, and the integral of `g` is arbitrarily close (within any positive real number `ε`) to the integral of `f`. Note that `g` is generally valued in the extended real numbers (EReal). Additionally, the value of `g` is almost everywhere greater than negative infinity with respect to the measure `μ`.
More concisely: Given an integrable real-valued function on a topological space, there exists an integrable, upper semicontinuous function with values in the extended real numbers whose integral is arbitrarily close to that of the original function, and which is almost everywhere greater than negative infinity.
|
MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge
theorem MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
(μ : MeasureTheory.Measure α) [inst_3 : μ.WeaklyRegular] (f : α → ENNReal),
Measurable f →
∀ {ε : ENNReal},
ε ≠ 0 → ∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
The theorem `MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge` states that for any topological, measurable, and Borel space `α`, given a measure `μ` on `α` which is weakly regular, and a measurable function `f` from `α` to the extended nonnegative real numbers, if `ε` is a nonzero extended nonnegative real number, then there exists a function `g` such that for each `x` in `α`, `f(x)` is less than or equal to `g(x)`, `g` is lower semicontinuous, and the Lebesgue integral of `g` with respect to the measure `μ` is less than or equal to the Lebesgue integral of `f` with respect to `μ` plus `ε`. This theorem is an auxiliary lemma used in the proof of the Vitali-Carathéodory theorem.
More concisely: Given a weakly regular measure `μ` on a topological, measurable, and Borel space `α`, and a measurable function `f` from `α` to the extended nonnegative reals, there exists a lower semicontinuous function `g` such that `f(x) ≤ g(x)` for all `x` in `α` and the Lebesgue integral of `g` with respect to `μ` is less than or equal to that of `f` plus `ε`.
|
MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal
theorem MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{μ : MeasureTheory.Measure α} [inst_3 : μ.WeaklyRegular] [inst_4 : MeasureTheory.SigmaFinite μ] (f : α → NNReal),
MeasureTheory.Integrable (fun x => ↑(f x)) μ →
∀ {ε : ℝ},
0 < ε →
∃ g,
(∀ (x : α), ↑(f x) < g x) ∧
LowerSemicontinuous g ∧
(∀ᵐ (x : α) ∂μ, g x < ⊤) ∧
MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ε
This theorem expresses that for any integrable function `f` mapping to non-negative real numbers (`ℝ≥0`) in a sigma-finite space, given a positive real number `ε`, there exists another function `g` that exceeds `f` at every point, is lower semicontinuous, and such that almost every point `x`under measure `μ`, `g(x)` is less than infinity. Furthermore, `g` is also integrable and the integration of `g` over the entire domain is less than the integration of `f` plus `ε`. This is an auxiliary lemma for the Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.
More concisely: Given an integrable, non-negative function `f` on a sigma-finite measure space, for any `ε > 0`, there exists a lower semicontinuous, integrable function `g` such that `g(x) < ∞` almost everywhere, and the integral of `g` is strictly less than the integral of `f` plus `ε`.
|
MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt
theorem MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{μ : MeasureTheory.Measure α} [inst_3 : μ.WeaklyRegular] [inst_4 : MeasureTheory.SigmaFinite μ] (f : α → ℝ),
MeasureTheory.Integrable f μ →
∀ {ε : ℝ},
0 < ε →
∃ g,
(∀ (x : α), ↑(f x) < g x) ∧
LowerSemicontinuous g ∧
MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧
(∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
**Vitali-Carathéodory Theorem**: Given an integrable real-valued function `f` defined on a topological space `α` equipped with a sigma-finite and weakly regular Borel measure `μ`, there exists a lower semicontinuous function `g` which is integrable and whose values are greater than those of `f`. Furthermore, the integral of `g` is arbitrarily close to that of `f` (specifically, less than the integral of `f` plus any positive real number `ε`), and almost everywhere, `g` takes finite values. The function `g` has to be valued in the extended real number line in general.
More concisely: Given a sigma-finite, weakly regular Borel measure `μ` on a topological space `α` and an integrable real-valued function `f` on `α`, there exists a lower semicontinuous, integrable, extended real-valued function `g` such that $\int g \ d\mu < \int f \ d\mu + \epsilon$ for any $\epsilon > 0$ and $\operatorname{dom} g = \alpha$.
|
MeasureTheory.exists_upperSemicontinuous_le_lintegral_le
theorem MeasureTheory.exists_upperSemicontinuous_le_lintegral_le :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{μ : MeasureTheory.Measure α} [inst_3 : μ.WeaklyRegular] (f : α → NNReal),
∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤ →
∀ {ε : ENNReal},
ε ≠ 0 →
∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
This theorem, which is an auxiliary lemma for the Vitali-Carathéodory theorem, states that for every integrable function `f` that maps to the nonnegative real numbers, there exists an upper semicontinuous function `g` such that `g` is less than or equal to `f` at every input and the integral of `g` is within an arbitrarily small difference of the integral of `f`. The input space is a topological space that also supports a measure, and the measure is weakly regular. The theorem is quantified across all small non-zero values of the extended real numbers, denoted as `ε`.
More concisely: For every integrable, non-negative real-valued function on a weakly regular topological measure space, there exists an upper semicontinuous function with the same integral value up to an arbitrarily small positive error.
|
MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable
theorem MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
(μ : MeasureTheory.Measure α) [inst_3 : μ.WeaklyRegular] [inst_4 : MeasureTheory.SigmaFinite μ] (f : α → NNReal),
AEMeasurable f μ →
∀ {ε : ENNReal},
ε ≠ 0 →
∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
This theorem states that given a function `f` that is almost everywhere measurable with values in the nonnegative real numbers (`ℝ≥0`) in a sigma-finite space, there exists another function `g` that is lower semicontinuous and strictly greater than `f` everywhere, with the property that the integral of `g` is arbitrarily close to the integral of `f`. This closeness is quantified by an arbitrary, nonzero extended nonnegative real number `ε`. This theorem is an auxiliary lemma for the Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.
More concisely: Given an almost everywhere measurable function `f` from a sigma-finite space to the nonnegative reals with finite integral, there exists a lower semicontinuous function `g` strictly greater than `f` such that their integrals differ by an arbitrarily small amount.
|
MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge
theorem MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
(μ : MeasureTheory.Measure α) [inst_3 : μ.WeaklyRegular] (f : MeasureTheory.SimpleFunc α NNReal) {ε : ENNReal},
ε ≠ 0 →
∃ g, (∀ (x : α), ↑f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(↑f x) ∂μ + ε
This theorem, which is a part of the Vitali-Carathéodory theorem, states that for any simple function `f` mapping into the nonnegative real numbers and defined over a topological space `α` that is also measurable and Borel, with respect to a measure `μ` that is weakly regular, there exists a lower semicontinuous function `g` which is greater than or equal to `f` such that the integral of `g` is arbitrarily close to the integral of `f`. The arbitrarily close condition is defined in terms of a non-zero `ε` which belongs to the extended nonnegative real numbers. Specifically, the theorem states that the integral of `g` is less than or equal to the integral of `f` plus `ε`.
More concisely: Given a simple function `f` mapping into the nonnegative reals, defined on a measurable and Borel topological space `α` with respect to a weakly regular measure `μ`, there exists a lower semicontinuous function `g` such that $\int g \leq \int f + \epsilon$, for some non-zero `ε` in the extended nonnegative reals.
|
MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le
theorem MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
{μ : MeasureTheory.Measure α} [inst_3 : μ.WeaklyRegular] (f : MeasureTheory.SimpleFunc α NNReal),
∫⁻ (x : α), ↑(↑f x) ∂μ ≠ ⊤ →
∀ {ε : ENNReal},
ε ≠ 0 →
∃ g, (∀ (x : α), g x ≤ ↑f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
This theorem states that given a simple function `f` that takes values in the set of nonnegative real numbers and operates in a topological space with a measurable space and Borel space, along with a measure `μ` that is weakly regular, if the integral over `f` does not equal infinity, then for any extended nonnegative real number `ε` that does not equal zero, there exists an upper semicontinuous function `g` that does not surpass `f` at any point in the domain, and the integral over `f` is less than or equal to the integral over `g` plus `ε`.
This theorem is an auxiliary lemma for the Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`. The statement of this theorem is in terms of the Lebesgue integral, or `lintegral`.
More concisely: Given a simple, nonnegative real-valued function `f` on a measurable space with a weakly regular measure `μ`, if the integral of `f` is finite, then there exists an upper semicontinuous function `g` that does not exceed `f` and satisfies the integral of `g` being less than or equal to the integral of `f` plus a given positive `ε`.
|