MeasureTheory.Memℒp.exists_boundedContinuous_snorm_sub_le
theorem MeasureTheory.Memℒp.exists_boundedContinuous_snorm_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal}
[inst_5 : NormedSpace ℝ E] [inst_6 : μ.WeaklyRegular],
p ≠ ⊤ →
∀ {f : α → E},
MeasureTheory.Memℒp f p μ →
∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.snorm (f - ⇑g) p μ ≤ ε ∧ MeasureTheory.Memℒp (⇑g) p μ
This theorem states that for any function `f` in `ℒp` space where `p` is not infinity, if the space `α` is measurable, also a topological space, a T4 space, and a Borel space, and the function `E` is a normed addition commutative group, with a measure `μ` that is weakly regular, then for any non-zero extended nonnegative real number `ε`, there exists a bounded continuous function `g` such that the `ℒp` seminorm of the difference between `f` and `g` is less than or equal to `ε` and `g` is also in `ℒp` space.
In mathematical terms, if `f` is in `ℒp` (Lebesgue `p`-integrable functions) for some `p` less than infinity, then there exists a sequence of bounded continuous functions that approximates `f` in the `ℒp` norm, i.e., for any `ε > 0`, there exists a bounded continuous function `g` such that the `ℒp` norm of `f - g` is less than or equal to `ε`.
More concisely: If `f` is a Lebesgue integrable function in the `ℒp` space for some finite `p`, and `α` is a measurable, topological T4 Borel space with a weakly regular measure `μ` and the normed additive commutative group `E`, then for any `ε > 0`, there exists a bounded continuous function `g` in `ℒp` such that the `ℒp` norm of `f - g` is less than or equal to `ε`.
|
MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le
theorem MeasureTheory.Integrable.exists_boundedContinuous_lintegral_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
[inst_5 : NormedSpace ℝ E] [inst_6 : μ.WeaklyRegular] {f : α → E},
MeasureTheory.Integrable f μ →
∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
The theorem states that for any given measurable space with a topological structure, which also satisfies the T4 separation axiom (also known as normality), and is a Borel space, and for any given normed additively commutative group, along with a measure defined on the space, if we have a function that is integrable (i.e., it is measurable and its integral over the measure is finite), then for any positive extended nonnegative real number `ε`, there exists a bounded continuous function `g` such that the integral over the absolute difference between the original function and `g` with respect to the measure is less than or equal to `ε`, and furthermore, `g` is also integrable with respect to the same measure. This theorem essentially states that any integrable function can be approximated by bounded continuous functions in the context of measure theory.
More concisely: Given a measurable space with a T4 topology and Borel structure, any integrable function on a normed additively commutative group can be approximated by a bounded, continuous, and integrable function.
|
MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le
theorem MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
[inst_5 : NormedSpace ℝ E] [inst_6 : WeaklyLocallyCompactSpace α] [inst_7 : μ.Regular] {f : α → E},
MeasureTheory.Integrable f μ →
∀ {ε : ENNReal},
ε ≠ 0 →
∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
In a locally compact T4 (normal Hausdorff) space that has a Borel measure and is weakly locally compact, any function that is integrable with respect to a regular measure can be approximated by compactly supported continuous functions. More precisely, for any non-zero extended nonnegative real number `ε`, there exists a function `g` which has compact support and is both continuous and integrable, such that the integral over the space of the nonnegative real part of the norm of the difference between the original function `f` and the approximating function `g` is less than or equal to `ε`.
More concisely: In a locally compact T4 (normal Hausdorff) space with a regular Borel measure and weak compactness, any integrable function can be approximated by a compactly supported, continuous, and integrable function up to an arbitrary positive real number.
|
MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le
theorem MeasureTheory.Integrable.exists_boundedContinuous_integral_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
[inst_5 : NormedSpace ℝ E] [inst_6 : μ.WeaklyRegular] {f : α → E},
MeasureTheory.Integrable f μ →
∀ {ε : ℝ}, 0 < ε → ∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
The theorem states that for any integrable function 'f' in a T4 topological space (a space where any two disjoint closed sets have disjoint open neighborhoods), a Borel space (the smallest sigma-algebra containing all open sets), and a weakly regular measure space, there exists a bounded continuous function 'g' such that the integral of the norm of the difference between 'f' and 'g' is less than or equal to any given positive real number 'ε'. Furthermore, this function 'g' itself is also integrable.
In simpler terms, it means that we can approximate any integrable function by a bounded continuous function with a precision specified by a given positive real number.
More concisely: Given an integrable function 'f' on a T4 topological space with a weakly regular measure, there exists a bounded, continuous, and integrable function 'g' such that the integral of the norm of 'f' - 'g' is less than or equal to any given positive real number.
|
MeasureTheory.exists_continuous_snorm_sub_le_of_closed
theorem MeasureTheory.exists_continuous_snorm_sub_le_of_closed :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal}
[inst_5 : NormedSpace ℝ E] [inst_6 : μ.OuterRegular],
p ≠ ⊤ →
∀ {s u : Set α},
IsClosed s →
IsOpen u →
s ⊆ u →
↑↑μ s ≠ ⊤ →
∀ (c : E) {ε : ENNReal},
ε ≠ 0 →
∃ f,
Continuous f ∧
MeasureTheory.snorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧
(∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.Memℒp f p μ
This theorem is a variant of Urysohn's lemma in the context of $\mathcal{L}^p$ spaces and outer regular measures. Given a measurable space `α` that is also a topological space, a closed set `s` and an open set `u` such that `s` is contained in `u` and the measure of `s` is finite, and a vector `c`, there exists a continuous function `f` that is equal to `c` on `s` and `0` outside of `u`, and its norm is bounded by the norm of `c` everywhere. Moreover, the $\mathcal{L}^p$ norm of the difference between `f` and the indicator function of `s` taking value `c` can be made arbitrarily small. Importantly, this function `f` also belongs to the $\mathcal{L}^p$ space. The theorem asserts that this construction is possible whenever `p` is not equal to infinity and the measure of `s` is not infinite.
More concisely: Given a measurable and topological space `α`, a closed `s` with finite measure, an open `u` containing `s`, and a finite `p`, there exists a continuous `f : α → ℝ` with `f = c` on `s`, `f = 0` outside `u`, and `∥f - 1\_s∥_p < ε`, where `1_s` is the indicator function of `s` and `c ∈ ℝ` is a constant.
|
MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le
theorem MeasureTheory.Memℒp.exists_hasCompactSupport_snorm_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal}
[inst_5 : NormedSpace ℝ E] [inst_6 : WeaklyLocallyCompactSpace α] [inst_7 : μ.Regular],
p ≠ ⊤ →
∀ {f : α → E},
MeasureTheory.Memℒp f p μ →
∀ {ε : ENNReal},
ε ≠ 0 →
∃ g,
HasCompactSupport g ∧
MeasureTheory.snorm (f - g) p μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Memℒp g p μ
This theorem states that in a locally compact space, for any function `f` that lies in `ℒp` space (i.e., `f` is almost everywhere strongly measurable and its `ℒp` seminorm is finite) with `p` not equal to infinity, we can find a function `g` with compact support such that the `ℒp` seminorm of the difference between `f` and `g` is less than or equal to `ε` (where `ε` is a non-zero extended nonnegative real number) and `g` is a continuous function that also lies in `ℒp` space. The space is assumed to be a T₄ space (every two disjoint closed sets have disjoint open neighborhoods) with a Borel measure that is regular (every Borel set can be approximated from inside and outside by compact sets). In other words, any function in `ℒp` can be approximated by compactly supported continuous functions when `p` is less than infinity.
More concisely: In a locally compact T₄ space with a regular Borel measure, for any `f` in `ℒp` with finite `ℒp` seminorm and `p` not equal to infinity, there exists a compactly supported continuous `g` in `ℒp` such that the `ℒp` distance between `f` and `g` is less than `ε`.
|
MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le
theorem MeasureTheory.Memℒp.exists_hasCompactSupport_integral_rpow_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
[inst_5 : NormedSpace ℝ E] [inst_6 : WeaklyLocallyCompactSpace α] [inst_7 : μ.Regular] {p : ℝ},
0 < p →
∀ {f : α → E},
MeasureTheory.Memℒp f (ENNReal.ofReal p) μ →
∀ {ε : ℝ},
0 < ε →
∃ g,
HasCompactSupport g ∧
∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Memℒp g (ENNReal.ofReal p) μ
The theorem states that in a locally compact space, for any function `f` that belongs to the space of `p`-integrable functions (`ℒp` space) with `0 < p < ∞`, there exists a compactly supported continuous function `g` such that the integral of the `p`-th power of the norm of the difference between `f` and `g` with respect to a measure `μ` is less than or equal to any given positive real number `ε`. Moreover, this approximating function `g` also belongs to the `ℒp` space. This theorem effectively shows that `ℒp` functions can be approximated by continuous functions with compact support in the context of locally compact spaces.
More concisely: In a locally compact space, for any `p`-integrable function `f`, there exists a compactly supported, continuous `g` in the `ℒp` space such that the `p`-th power integral of the norm difference between `f` and `g` is less than `ε`.
|
MeasureTheory.Lp.boundedContinuousFunction_dense
theorem MeasureTheory.Lp.boundedContinuousFunction_dense :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] (E : Type u_2) [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal}
[inst_5 : NormedSpace ℝ E] [inst_6 : SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)],
p ≠ ⊤ → ∀ [inst_7 : μ.WeaklyRegular], (MeasureTheory.Lp.boundedContinuousFunction E p μ).topologicalClosure = ⊤
The theorem `MeasureTheory.Lp.boundedContinuousFunction_dense` states that for any measure space `α` that is also a topological space, a `T4Space` and a `BorelSpace`, and any normed add-commutative group `E` that is also a normed space over the real numbers, given a measure `μ` on `α` and a nonnegative extended real number `p` (denoted `ENNReal` in Lean 4), if `α` and `E` also have a second-countable topology, and `p` is a real number greater than or equal to 1 and less than infinity, and assuming `μ` is weakly regular, then the topological closure of the space of bounded continuous functions in `Lp` is the entire space. In other words, every function in `Lp` can be approximated in `Lp` by continuous functions.
More concisely: Given a second-countable measure space with a weakly regular measure, a normed group, and real number `p` (1 ≤ p < ∞), every function in the `Lp` space can be approximated by bounded continuous functions.
|
Mathlib.MeasureTheory.Function.ContinuousMapDense._auxLemma.14
theorem Mathlib.MeasureTheory.Function.ContinuousMapDense._auxLemma.14 :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
{f : α → β}, MeasureTheory.Integrable f μ = MeasureTheory.Memℒp f 1 μ
This theorem states that for any types `α` and `β`, any measurable space `m` over `α`, any measure `μ` over `α`, and any function `f` from `α` to `β` in a normed additive commutative group, the function `f` is integrable with respect to the measure `μ` if and only if `f` is almost everywhere strongly measurable and the real-numbered power mean of the norm of `f` with exponent 1 (also known as the L1 norm of `f`) is finite with respect to `μ`. In mathematical terms, it asserts that $\int ‖f a‖ \, dμ < ∞$ is equivalent to the condition that $\left(\int ‖f a‖^1 \, dμ\right)^{1/1} < ∞$.
More concisely: A function between measurable spaces is integrable with respect to a measure if and only if it is almost everywhere strongly measurable and has finite L1 norm with respect to that measure.
|
MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le
theorem MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
[inst_5 : NormedSpace ℝ E] [inst_6 : WeaklyLocallyCompactSpace α] [inst_7 : μ.Regular] {f : α → E},
MeasureTheory.Integrable f μ →
∀ {ε : ℝ},
0 < ε →
∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
This theorem states that in a locally compact space, for any integrable function, it is always possible to find a compactly supported continuous function which approximates the integral of the given function within any given positive error bound. Specifically, given any measurable, topological space that satisfies the properties of a T4 space (i.e., a normal space that is also T1) and a Borel space, and a measure that is regular. Given any integrable function in this space, it is always possible to find a continuous function with compact support such that the integral of the absolute difference between the original function and the approximating function (over the measure space) is less than or equal to a given positive error bound.
More concisely: In a locally compact T4 Borel space endowed with a regular measure, for any integrable function there exists a compactly supported continuous function with minimal integral difference.
|
MeasureTheory.Memℒp.exists_boundedContinuous_integral_rpow_sub_le
theorem MeasureTheory.Memℒp.exists_boundedContinuous_integral_rpow_sub_le :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : T4Space α]
[inst_3 : BorelSpace α] {E : Type u_2} [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
[inst_5 : NormedSpace ℝ E] [inst_6 : μ.WeaklyRegular] {p : ℝ},
0 < p →
∀ {f : α → E},
MeasureTheory.Memℒp f (ENNReal.ofReal p) μ →
∀ {ε : ℝ}, 0 < ε → ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MeasureTheory.Memℒp (⇑g) (ENNReal.ofReal p) μ
The theorem states that for any function `f` that belongs to the space `ℒp` (signified by `MeasureTheory.Memℒp f (ENNReal.ofReal p) μ`), where `p` is a positive real number (`0 < p`) and `μ` is a measure, there exists a bounded continuous function `g` such that the integral of the `p`-th power of the norm of the difference between `f` and `g` (`∫ (x : α), ‖f x - g x‖ ^ p ∂μ`) is less than or equal to `ε` (a positive real number, `0 < ε`) and `g` also belongs to the `ℒp` space. In other words, any function in `ℒp` can be approximated by bounded continuous functions when `0 < p < ∞`. The approximation is such that the `p`-th power integral of the difference between the function and its approximation is within any given positive limit. This property is one of the fundamental aspects of `ℒp` spaces in measure theory.
More concisely: For any `f` in `ℒp` space with measure `μ` and positive real number `p`, `ε`, there exists a bounded continuous `g` in `ℒp` such that the integral of `‖f - g‖^p ∂μ` is less than or equal to `ε`.
|