MeasureTheory.L1.SimpleFunc.integrable
theorem MeasureTheory.L1.SimpleFunc.integrable :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)),
MeasureTheory.Integrable (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
This theorem states that for any measurable space `α`, any normed add commutative group `E`, and any measure `μ` on `α`, if `f` is an element of the subspace of `Lp` consisting of equivalence classes of an integrable simple function (i.e., `f` belongs to `MeasureTheory.Lp.simpleFunc E 1 μ`), then the representative function of `f` (given by `MeasureTheory.Lp.simpleFunc.toSimpleFunc f`) is integrable with respect to the measure `μ`. In other words, the representative function is measurable and its norm has a finite integral over `α` with respect to measure `μ`.
More concisely: For any measurable space `α`, any normed add commutative group `E`, and any measure `μ` on `α`, if `f` is an integrable simple function in `Lp(μ, E)`, then its representative function is an integrable function with respect to `μ`.
|
MeasureTheory.SimpleFunc.integrable_iff
theorem MeasureTheory.SimpleFunc.integrable_iff :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{μ : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α E},
MeasureTheory.Integrable (↑f) μ ↔ ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
The theorem `MeasureTheory.SimpleFunc.integrable_iff` states that for any measurable space `α`, normed additive commutative group `E`, measure `μ` on `α`, and simple function `f` from `α` to `E`, the function `f` is integrable with respect to measure `μ` if and only if for all `y` in `E` that are not zero, the measure of the preimage of `{y}` under `f` is finite (less than infinity). In simpler terms, a simple function is integrable if the measure of the set of points that map to every non-zero value is finite.
More concisely: A simple function from a measurable space to a normed additive commutative group is integrable if and only if the measure of the preimage of every non-zero value is finite.
|
MeasureTheory.Integrable.induction
theorem MeasureTheory.Integrable.induction :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{μ : MeasureTheory.Measure α} (P : (α → E) → Prop),
(∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (s.indicator fun x => c)) →
(∀ ⦃f g : α → E⦄,
Disjoint (Function.support f) (Function.support g) →
MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → P f → P g → P (f + g)) →
IsClosed {f | P ↑↑f} →
(∀ ⦃f g : α → E⦄, μ.ae.EventuallyEq f g → MeasureTheory.Integrable f μ → P f → P g) →
∀ ⦃f : α → E⦄, MeasureTheory.Integrable f μ → P f
This theorem states that to prove a property for an arbitrary integrable function in a normed group, it suffices to show four things:
1. The property holds for multiples of characteristic functions. In other words, if `c` is any element of the normed group, `s` is a measurable subset of `α`, and the measure of `s` is finite, then the property `P` holds for the characteristic function of `s` multiplied by `c`.
2. The property is preserved under addition. Specifically, if `f` and `g` are integrable functions such that the support of `f` and `g` are disjoint (meaning their intersection is the empty set), and if the property `P` holds for both `f` and `g`, then `P` also holds for `f + g`.
3. The set of functions for which the property holds is closed in the `L¹` space. In other words, if a sequence of functions all satisfy `P`, and if they converge in `L¹` norm to a limit function, then the limit function also satisfies `P`.
4. The property is preserved under the almost-everywhere equal relation. This means that if `f` and `g` are functions that are equal almost everywhere (which means they are equal except on a subset of `α` with measure zero), and `f` is integrable and satisfies `P`, then `g` also satisfies `P`.
The theorem concludes that if these conditions are satisfied, then for any integrable function `f`, if `f` is integrable, then `f` satisfies `P`.
More concisely: If a property `P` holds for multiples of characteristic functions, is closed under addition and convergence in `L¹` space, and is preserved under the almost-everywhere equal relation, then any integrable function satisfies `P` almost everywhere.
|
MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt
theorem MeasureTheory.Memℒp.exists_simpleFunc_snorm_sub_lt :
∀ {β : Type u_2} [inst : MeasurableSpace β] {p : ENNReal} {E : Type u_7} [inst_1 : NormedAddCommGroup E] {f : β → E}
{μ : MeasureTheory.Measure β},
MeasureTheory.Memℒp f p μ →
p ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.snorm (f - ↑g) p μ < ε ∧ MeasureTheory.Memℒp (↑g) p μ
This theorem states that for any function `f` belonging to `ℒp` for some measure `μ` and extended nonnegative real number `p` (where `p` is not infinity), we can find a simple function `g` such that the `ℒp` seminorm of the difference between `f` and `g` is less than any given non-zero extended nonnegative real number `ε`. Moreover, this simple function `g` itself also belongs to `ℒp`. This essentially means that we can closely approximate any `ℒp` function with a simple function if `p` is less than infinity.
More concisely: Given any function `f` in `ℒp` for some measure `μ` and finite extended non-negative real number `p`, there exists a simple function `g` in `ℒp` such that the `ℒp` norm of `f - g` is less than any prescribed positive `ε`.
|
MeasureTheory.SimpleFunc.memℒp_iff
theorem MeasureTheory.SimpleFunc.memℒp_iff :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{μ : MeasureTheory.Measure α} {p : ENNReal} {f : MeasureTheory.SimpleFunc α E},
p ≠ 0 → p ≠ ⊤ → (MeasureTheory.Memℒp (↑f) p μ ↔ ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤)
The theorem `MeasureTheory.SimpleFunc.memℒp_iff` states that for any measure space `α`, any normed, additive commutative group `E`, any measure `μ` on `α`, any extended nonnegative real number `p` that is neither zero nor infinity, and any simple function `f` from `α` to `E`, the function `f` belongs to the space of `p`-integrable functions (i.e., `MeasureTheory.Memℒp`) if and only if for all nonzero elements `y` of `E`, the measure of the preimage of the set `{y}` under `f` is finite (i.e., is not infinity). This theorem essentially characterizes `p`-integrable functions in terms of the measure of the preimages of singletons.
More concisely: A simple function from a measure space to a normed, additive commutative group is `p`-integrable if and only if the measure of the preimage of every nonzero element is finite.
|
MeasureTheory.Memℒp.induction
theorem MeasureTheory.Memℒp.induction :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)],
p ≠ ⊤ →
∀ (P : (α → E) → Prop),
(∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (s.indicator fun x => c)) →
(∀ ⦃f g : α → E⦄,
Disjoint (Function.support f) (Function.support g) →
MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ → P f → P g → P (f + g)) →
IsClosed {f | P ↑↑f} →
(∀ ⦃f g : α → E⦄, μ.ae.EventuallyEq f g → MeasureTheory.Memℒp f p μ → P f → P g) →
∀ ⦃f : α → E⦄, MeasureTheory.Memℒp f p μ → P f
The theorem `MeasureTheory.Memℒp.induction` establishes a method for proving a certain property holds for any function from a measurable space `α` to a normed add commutative group `E` that belongs to the `Lᵖ` space (i.e., the function is almost everywhere strongly measurable and its `p`-th power integral is finite), given certain conditions. These conditions are:
1. The property holds for any characteristic function scaled by a constant,
2. The property is preserved under the operation of addition for disjointly supported functions in the `Lᵖ` space,
3. The set of functions for which the property holds is closed,
4. The property is preserved under the almost-everywhere equality relation.
Please note that `p` is a non-negative extended real number which is strictly less than infinity, and `μ` is a measure on the measurable space `α`. The property `P` is a predicate on functions from `α` to `E`. The theorem asserts that if these conditions are met, then for any function in the `Lᵖ` space, if the function satisfies the property `P`, then the property `P` holds for any function in the `Lᵖ` space.
For the second condition, the intersection of the images of two functions `f` and `g` should be a subset of `{0}`, but this stronger condition might be added in the future if required.
More concisely: If a property `P` satisfies the given conditions (being closed under scaling, addition of disjointly supported functions, and preservation under almost-everywhere equality), then any almost everywhere strongly measurable function from a measurable space to an `Lp` space with finite `p`-th power integral, having property `P`, also has property `P` for the sum of any two such functions with disjoint support.
|
MeasureTheory.Lp.simpleFunc.induction
theorem MeasureTheory.Lp.simpleFunc.induction :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α},
p ≠ 0 →
p ≠ ⊤ →
∀ {P : ↥(MeasureTheory.Lp.simpleFunc E p μ) → Prop},
(∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤),
P (MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) →
(∀ ⦃f g : MeasureTheory.SimpleFunc α E⦄ (hf : MeasureTheory.Memℒp (↑f) p μ)
(hg : MeasureTheory.Memℒp (↑g) p μ),
Disjoint (Function.support ↑f) (Function.support ↑g) →
P (MeasureTheory.Lp.simpleFunc.toLp f hf) →
P (MeasureTheory.Lp.simpleFunc.toLp g hg) →
P (MeasureTheory.Lp.simpleFunc.toLp f hf + MeasureTheory.Lp.simpleFunc.toLp g hg)) →
∀ (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)), P f
This theorem provides a way to prove a property for all simple `Lp` functions, where `0 < p < ∞`. The theorem states that to prove a property `P` for all simple `Lp` functions, it is sufficient to show:
1. The property `P` holds for all characteristic functions of finite-measure measurable sets, possibly multiplied by a constant. In mathematical terms, for any constant `c` and set `s` such that `s` is a measurable set and the measure of `s` is finite, `P` holds for the `Lp` function that is equal to `c` on `s` and zero elsewhere.
2. The property `P` is preserved under addition of simple `Lp` functions. In other words, if you have two simple `Lp` functions `f` and `g` such that their supports (the sets where they are non-zero) are disjoint, then `P` holding for both `f` and `g` implies that `P` also holds for `f + g`.
This theorem leverages the structure of the `Lp` space and is a powerful tool for proving theorems about simple `Lp` functions.
More concisely: The theorem asserts that to prove a property for all simple `Lp` functions, it is sufficient to verify it for characteristic functions of finite-measure sets, multiplied by constants, and to show preservation under addition of disjoint simple `Lp` functions.
|
MeasureTheory.Lp.simpleFunc.measurable
theorem MeasureTheory.Lp.simpleFunc.measurable :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} [inst_2 : MeasurableSpace E] (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
Measurable ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
The theorem `MeasureTheory.Lp.simpleFunc.measurable` states that if `α` is a measurable space and `E` is a normed additive commutative group and `p` is an extended nonnegative real number and `μ` is a measure on `α`, then for any function `f` that is a member of the space of equivalence classes of simple functions (`MeasureTheory.Lp.simpleFunc E p μ`), the representative of `f` found via `MeasureTheory.Lp.simpleFunc.toSimpleFunc` is a measurable function, meaning that the preimage of any measurable set under this function is also measurable.
More concisely: For any measurable space `(α, Σ, μ)`, normed additive commutative group `E` with a nonnegative real number `p`, the representative function of any simple `E`-valued function `f` in the space of simple functions `MeasureTheory.Lp.simpleFunc E p μ` is measurable.
|
MeasureTheory.Memℒp.induction_dense
theorem MeasureTheory.Memℒp.induction_dense :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α},
p ≠ ⊤ →
∀ (P : (α → E) → Prop),
(∀ (c : E) ⦃s : Set α⦄,
MeasurableSet s →
↑↑μ s < ⊤ →
∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.snorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g) →
(∀ (f g : α → E), P f → P g → P (f + g)) →
(∀ (f : α → E), P f → MeasureTheory.AEStronglyMeasurable f μ) →
∀ {f : α → E},
MeasureTheory.Memℒp f p μ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.snorm (f - g) p μ ≤ ε ∧ P g
This theorem states the following: Given a non-infinite `p`, a measure space on `α`, and a normed add commutative group `E`, a property `P` of functions from `α` to `E` satisfies the following conditions:
1. For every constant `c` in `E` and every measurable set `s` of `α` with finite measure, if a positive extended real number `ε` is given, there exists a function `g` such that the `ℒp` seminorm of the difference between `g` and the indicator function of `s` (which takes the value `c` on `s` and `0` elsewhere) is less than or equal to `ε`, and `P` holds for `g`.
2. `P` is stable under addition, i.e, if `P` holds for two functions `f` and `g`, then it also holds for their sum.
3. If `P` holds for a function `f`, then `f` is almost everywhere strongly measurable with respect to the given measure.
Then, for every function `f` from `α` to `E` that belongs to `ℒp` (i.e., it is almost everywhere strongly measurable and its `ℒp` seminorm is finite), for every positive extended real number `ε`, there exists a function `g` such that the `ℒp` seminorm of the difference between `f` and `g` is less than or equal to `ε`, and `P` holds for `g`. In other words, the set of functions satisfying `P` is dense in `ℒp`.
More concisely: Given a measure space, a non-infinite `p`, a normed add commutative group `E`, and a property `P` of functions from `α` to `E` satisfying conditions 1-3, the set of functions in `Lp` satisfying `P` is dense in `Lp`.
|
MeasureTheory.Lp.simpleFunc.denseRange
theorem MeasureTheory.Lp.simpleFunc.denseRange :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], p ≠ ⊤ → DenseRange Subtype.val
This theorem, named `MeasureTheory.Lp.simpleFunc.denseRange`, states that for any type `α` equipped with a `MeasurableSpace` structure, any type `E` equipped with a `NormedAddCommGroup` structure, any extended nonnegative real number `p` not equal to infinity (where `ENNReal` represents the extended nonnegative real numbers), and any measure `μ` on `α` where it is a fact that `1 ≤ p`, the function `Subtype.val` has a dense range. This means that the image of the `Subtype.val` function is a dense subset of the space it maps into.
More concisely: For any measurable space `(α, Σ)`, normed additive group `(E, +, ‖.‖)`, extended nonnegative real number `p > 0`, and measure `μ` on `α`, the range of `Subtype.val` from the set of measurable simple functions `MeasuredFunctions μ E` is dense in the Banach space `(E, ‖.��ėxpected Norm‖_2)`.
|
MeasureTheory.Lp.simpleFunc.memℒp
theorem MeasureTheory.Lp.simpleFunc.memℒp :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
MeasureTheory.Memℒp (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ
The theorem `MeasureTheory.Lp.simpleFunc.memℒp` states that for any measurable space `α`, any normed add comm group `E`, any extended nonnegative real number `p`, and any measure `μ` on `α`, if `f` is an element of `Lp.simpleFunc E p μ`, then the function produced by applying `toSimpleFunc` to `f` satisfies the `Memℒp` predicate. This means, in other words, that the function is almost everywhere strongly measurable and either its `p`-th power integral is finite when `p` is less than infinity, or its essential supremum is finite when `p` equals infinity.
More concisely: A simple function in the Lebesgue space `Lp(α, E, μ)` with finite `p-th` power integral or essential supremum, when `p` is finite or infinite respectively, is almost everywhere measurable.
|
MeasureTheory.Lp.simpleFunc.boundedSMul
theorem MeasureTheory.Lp.simpleFunc.boundedSMul :
∀ {α : Type u_1} {E : Type u_4} {𝕜 : Type u_6} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{p : ENNReal} {μ : MeasureTheory.Measure α} [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E]
[inst_4 : BoundedSMul 𝕜 E] [inst_5 : Fact (1 ≤ p)], BoundedSMul 𝕜 ↥(MeasureTheory.Lp.simpleFunc E p μ)
The theorem `MeasureTheory.Lp.simpleFunc.boundedSMul` states that if `E` is a normed space, then the space `Lp.simpleFunc E p μ` is also a normed space when scalar multiplication is bounded. Here, `E` is a `NormedAddCommGroup`, `𝕜` is a `NormedRing` and a `Module` over `E`, and `p` is an extended nonnegative real number which is assumed to be greater than or equal to 1. `μ` is a measure on a measurable space `α`. This theorem is used in the construction of the Bochner integral, despite not being declared as an instance.
More concisely: If `E` is a normed space, `μ` is a measure on a measurable space `α`, and scalar multiplication in `Lp.simpleFunc E p μ` is bounded, then `Lp.simpleFunc E p μ` is a normed space.
|
MeasureTheory.Lp.simpleFunc.uniformInducing
theorem MeasureTheory.Lp.simpleFunc.uniformInducing :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], UniformInducing Subtype.val
The theorem `MeasureTheory.Lp.simpleFunc.uniformInducing` states that for any types `α` and `E`, given a measurable space over `α`, a normed add commutative group over `E`, an extended nonnegative real number `p`, a measure `μ` defined on `α`, and the fact that `p` is greater than or equal to 1, the function `Subtype.val` is a uniform inducing function.
In mathematical terms, this theorem suggests that the function `Subtype.val`, which extracts the underlying element from a subtype, provides a uniform structure on the space of simple functions from `α` to `E` which are in `Lp` space with respect to the measure `μ`. This uniform structure is compatible with the topology induced by the `Lp` norm, which is why this function is called uniform inducing.
More concisely: For any measurable space over a type `α`, normed add commutative group over `E`, measure `μ` on `α`, and `p ≥ 1`, `Subtype.val` is a uniform inducing function for simple `Lp(μ, E)` functions from `α` to `E`.
|
MeasureTheory.Lp.induction
theorem MeasureTheory.Lp.induction :
∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} [_i : Fact (1 ≤ p)],
p ≠ ⊤ →
∀ (P : ↥(MeasureTheory.Lp E p μ) → Prop),
(∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤),
P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)) →
(∀ ⦃f g : α → E⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ),
Disjoint (Function.support f) (Function.support g) →
P (MeasureTheory.Memℒp.toLp f hf) →
P (MeasureTheory.Memℒp.toLp g hg) →
P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)) →
IsClosed {f | P f} → ∀ (f : ↥(MeasureTheory.Lp E p μ)), P f
The theorem `MeasureTheory.Lp.induction` states that in a second-countable Borel normed group, to prove a property for an arbitrary `Lp` function, it is sufficient to meet three conditions:
1. The property holds for characteristic functions (possibly multiplied by a constant). In other words, for any constant `c` and any measurable set `s` with measure less than infinity, the property holds for the `Lp` function which equals `c` on the set `s` and zero elsewhere.
2. The property is closed under addition. Specifically, if `f` and `g` are two functions such that `f` and `g` are essentially strongly measurable, their `p`-norms are finite, and their supports (the set of points where the function is non-zero) are disjoint, and if the property holds for `f` and `g`, then it also holds for the sum of `f` and `g`.
3. The set of `Lp` functions for which the property holds is closed. That is, if a sequence of `Lp` functions for which the property holds converges in the `Lp` space, then the limit function also satisfies the property.
The theorem is applicable for `p` in the extended nonnegative real numbers, except for infinity.
More concisely: In a second-countable Borel normed group, to prove a property for any `Lp` function, it is sufficient if it holds for characteristic functions, is closed under addition with disjoint supports and finite `p`-norms, and the set of satisfying functions is closed in the `Lp` space.
|