MeasureTheory.snorm_const_smul_le
theorem MeasureTheory.snorm_const_smul_le :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] {𝕜 : Type u_5} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 F]
[inst_3 : BoundedSMul 𝕜 F] (c : 𝕜) (f : α → F),
MeasureTheory.snorm (c • f) p μ ≤ ‖c‖₊ • MeasureTheory.snorm f p μ
This theorem asserts that for any measurable space `α`, any normed additive commutative group `F`, any extended non-negative real number `p`, any measure `μ` on `α`, any normed ring `𝕜`, and any scalar multiplication of `𝕜` on `F`, if `f` is a function from `α` to `F` and `c` is an element of `𝕜`, then the `ℒp` seminorm (as defined by `MeasureTheory.snorm`) of the scalar multiple `c • f` is less than or equal to the product of the non-negative norm of `c` and the `ℒp` seminorm of `f`. This formalizes a type of inequality for the `ℒp` seminorm under scalar multiplication.
More concisely: For any measurable space `α`, normed additive commutative group `F`, extended non-negative real number `p`, measure `μ` on `α`, normed ring `𝕜`, and scalar multiplication of `𝕜` on `F`, if `f : α → F` is measurable and `c ∈ 𝕜`, then `||c • f||ₗₙ ≤ ||c|| • ||f||ₗₙ`, where `||.||` denotes the `ℒp` seminorm.
|
MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg
theorem MeasureTheory.snorm_eq_zero_and_zero_of_ae_le_mul_neg :
∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : ℝ},
(∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) →
c < 0 → ∀ (p : ENNReal), MeasureTheory.snorm f p μ = 0 ∧ MeasureTheory.snorm g p μ = 0
This theorem states that for any measure space `α`, any two functions `f` and `g` from `α` to two normed add commutative groups `F` and `G` respectively, and any real number `c` less than zero, if for almost every `x` in the measure space, the norm of `f(x)` is less than or equal to `c` times the norm of `g(x)`, then the `ℒp` seminorm of both `f` and `g` with respect to any extended nonnegative real number `p` and the measure `μ` is zero. In other words, if the norm of `f(x)` is bounded above by a negative multiple of the norm of `g(x)` almost everywhere, then the `ℒp` seminorms of both `f` and `g` must be zero for all `p`.
More concisely: If two functions from a measure space to normed add commutative groups satisfy the condition that the norm of one function is less than or equal to a negative multiple of the norm of the other function almost everywhere, then their `ℒp` seminorms with respect to any extended nonnegative real number `p` and the measure `μ` are zero.
|
MeasureTheory.snorm_mono_ae
theorem MeasureTheory.snorm_mono_ae :
∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
(∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
The theorem `MeasureTheory.snorm_mono_ae` states that in a measurable space, given two normed additive commutative groups (`F` and `G`), a measure and an extended non-negative real number `p`, if almost everywhere in the measurable space the norm of a function `f` from the space to `F` is less than or equal to the norm of a function `g` from the space to `G`, then the `ℒp` seminorm of `f` is less than or equal to the `ℒp` seminorm of `g`.
In the `ℒp` seminorm, `p` is equal to `0` for `p=0`, to `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞` and to `essSup ‖f‖ μ` for `p = ∞`.
More concisely: If two measurable functions from a measurable space to normed additive commutative groups have almost everywhere less than or equal norms, then the `ℒp` seminorm of the first function is less than or equal to that of the second function for any `0 ≤ p <= ∞`.
|
Continuous.memℒp_top_of_hasCompactSupport
theorem Continuous.memℒp_top_of_hasCompactSupport :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] {X : Type u_5} [inst_1 : TopologicalSpace X]
[inst_2 : MeasurableSpace X] [inst_3 : OpensMeasurableSpace X] {f : X → E},
Continuous f → HasCompactSupport f → ∀ (μ : MeasureTheory.Measure X), MeasureTheory.Memℒp f ⊤ μ
The theorem `Continuous.memℒp_top_of_hasCompactSupport` states that for any continuous function `f` from a type `X` to a normed add commutative group `E`, where `X` is a topological space with a measurable structure such that the set of open subsets is measurable, if `f` has compact support, then the function `f` belongs to the space `L^∞` with respect to any measure `μ` on `X`. In other words, `f` is almost everywhere strongly measurable and the essential supremum of `f` is finite.
More concisely: A continuous function from a measurable topological space to a normed add commutative group with compact support belongs to the space `L^∞` with respect to any measurable measure.
|
MeasureTheory.Memℒp.snorm_ne_top
theorem MeasureTheory.Memℒp.snorm_ne_top :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.Memℒp f p μ → MeasureTheory.snorm f p μ ≠ ⊤
This theorem asserts that for any measurable space `α`, any extended nonnegative real number `p`, any measure `μ` on `α`, any normed add commutative group `E`, and any function `f` from `α` to `E`, if `f` satisfies the property of being `p`-integrable (i.e., `f` is almost everywhere strongly measurable and either the `p`-th power of the integral of the norm of `f` is finite, if `p < ∞`, or the essential supremum of `f` is finite, if `p = ∞`), then the `p`-seminorm of `f` (which is `0` when `p=0`, the `p`-th root of the integral of the `p`-th power of the norm of `f` when `0 < p < ∞`, and the essential supremum of the norm of `f` when `p = ∞`) is not equal to infinity. This theorem is essentially a restatement of part of the definition of `p`-integrability.
More concisely: If `α` is a measurable space, `p` is an extended nonnegative real number, `μ` is a measure on `α`, `E` is a normed add commutative group, and `f` is a `p`-integrable function from `α` to `E`, then the `p`-seminorm of `f` is finite.
|
MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul
theorem MeasureTheory.snorm_le_nnreal_smul_snorm_of_ae_le_mul :
∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G} {c : NNReal},
(∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) →
∀ (p : ENNReal), MeasureTheory.snorm f p μ ≤ c • MeasureTheory.snorm g p μ
This theorem states that for any measurable space `α` and measures `μ` on `α`, along with two normed addition commutative groups `F` and `G`, and functions `f : α → F` and `g : α → G` with a non-negative real number `c`, if almost everywhere in the measure space `α` the non-negative norm of `f` at `x` is less than or equal to `c` multiplied by the non-negative norm of `g` at `x`, then for every extended non-negative real number `p`, the `ℒp` seminorm of `f` is less than or equal to `c` times the `ℒp` seminorm of `g`.
In mathematical notation, given $f : \alpha \rightarrow F$, $g : \alpha \rightarrow G$ and a non-negative real number $c$, if $\|f(x)\|_{+} \leq c \cdot \|g(x)\|_{+}$ holds almost everywhere, then $\|f\|_{p} \leq c \cdot \|g\|_{p}$ for all extended non-negative real number $p$, where $\|.\|_{+}$ denotes the non-negative norm and $\|.\|_{p}$ denotes the `ℒp` seminorm.
More concisely: If the almost everywhere non-negative norm of a function `f` is less than or equal to the product of a constant `c` and the almost everywhere non-negative norm of another function `g`, then the `ℒp` seminorm of `f` is less than or equal to `c` times the `ℒp` seminorm of `g` for all extended non-negative real numbers `p`.
|
MeasureTheory.snorm_mono_nnnorm_ae
theorem MeasureTheory.snorm_mono_nnnorm_ae :
∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
(∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) → MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
The theorem `MeasureTheory.snorm_mono_nnnorm_ae` states that for any two functions `f` and `g` from a set `α` to normed additive commutative groups `F` and `G` respectively, and for a given measure `μ` on `α` and an extended nonnegative real `p`, if almost everywhere in `α` the nonnegative norm of `f(x)` is less than or equal to the nonnegative norm of `g(x)`, then the `ℒp` seminorm of `f` with respect to measure `μ` and `p` is less than or equal to the `ℒp` seminorm of `g` with respect to measure `μ` and `p`. The `ℒp` seminorm is defined as `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, `essSup ‖f‖ μ` for `p = ∞`, and `0` for `p=0`.
More concisely: If two functions from a measure space to normed additive commutative groups have almost everywhere less than or equal nonnegative norms, then the corresponding `ℒp` seminorms with respect to a given measure and `p > 0` satisfy the inequality.
|
MeasureTheory.snorm_neg
theorem MeasureTheory.snorm_neg :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] {f : α → F}, MeasureTheory.snorm (-f) p μ = MeasureTheory.snorm f p μ
The theorem `MeasureTheory.snorm_neg` states that the seminorm of the negative of a function `f`, under certain conditions, is equal to the seminorm of the function `f` itself. Specifically, for any measurable space `α`, any normed additive commutative group `F`, any measure `μ` on `α`, any extended nonnegative real number `p`, and any function `f` from `α` to `F`, we have `MeasureTheory.snorm (-f) p μ = MeasureTheory.snorm f p μ`. In simpler terms, taking the negative of a function does not change its `ℒp` seminorm, whether `p` is zero, positive but finite, or infinity.
More concisely: For any measurable function `f` from a measurable space to a normed additive commutative group, and for any measure and `ℒp` norm, the `ℒp` seminorm of the negative of `f` is equal to that of `f`.
|
MeasureTheory.snorm_const
theorem MeasureTheory.snorm_const :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] (c : F),
p ≠ 0 → μ ≠ 0 → MeasureTheory.snorm (fun x => c) p μ = ↑‖c‖₊ * ↑↑μ Set.univ ^ (1 / p.toReal)
The theorem `MeasureTheory.snorm_const` states that for any non-zero measure `μ` on a measurable space `α` and any non-zero extended nonnegative real number `p`, the `ℒp` seminorm of a constant function `c` (from `α` to a normed additive commutative group `F`) is equal to the norm of `c` multiplied by the measure of the universal set (which contains all the elements of `α`), raised to the power of `1 / p`. In mathematical terms, if `p ≠ 0` and `μ ≠ 0`, then we have `∥c∥₊ * μ(Ω)^(1/p)` where `Ω` represents the universal set.
More concisely: For any non-zero measure μ on a measurable space α and non-zero extended real number p, the ℒp seminorm of a constant function c from α to a normed additive commutative group F is equal to the norm of c multiplied by the measure of the universal set Ω raised to the power of 1/p.
|
MeasureTheory.memℒp_top_of_bound
theorem MeasureTheory.memℒp_top_of_bound :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
{f : α → E},
MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.Memℒp f ⊤ μ
The theorem `MeasureTheory.memℒp_top_of_bound` states that for any types `α` and `E` with `E` being a normed additive commutative group, and given a measurable space `m0` on `α`, a measure `μ` on `α`, and a function `f` from `α` to `E`, if the function `f` is almost everywhere strongly measurable with respect to the measure `μ`, and there exists a real number `C` such that almost everywhere the norm of `f(x)` is less than or equal to `C`, then `f` belongs to the space `Memℒp` for `p = ∞` with respect to the measure `μ`. In other words, `f` is almost everywhere strongly measurable and its essential supremum is finite.
More concisely: If a strongly measurable function from a measurable space to a normed additive commutative group is almost everywhere norm-bounded, then it belongs to the space of essentially bounded measurable functions.
|
MeasureTheory.snorm_mono
theorem MeasureTheory.snorm_mono :
∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
(∀ (x : α), ‖f x‖ ≤ ‖g x‖) → MeasureTheory.snorm f p μ ≤ MeasureTheory.snorm g p μ
This theorem, named `MeasureTheory.snorm_mono`, states the following: Given two types `α` and `F` and `G`, where `α` is a measurable space and `F` and `G` are normed additive commutative groups, if for every element `x` of type `α`, the norm of `f(x)` is less than or equal to the norm of `g(x)`, then the seminorm (or `ℒp` norm) of `f` is less than or equal to the seminorm of `g`. Here, `f` and `g` are functions from `α` to `F` and `G` respectively, `p` is an extended non-negative real number representing the `p` in `ℒp` norm, and `μ` is a measure on the measurable space `α`. This theorem basically demonstrates the monotonicity of the `ℒp` norm in the context of measure theory.
More concisely: If `μ` is a measure on a measurable space `α` and `p ≥ 0` is an extended real number, given functions `f : α → F` and `g : α → G` with `F` and `G` normed additive commutative groups, if `∀x ∈ α, ||f(x)|| ≤ ||g(x)||`, then `||f||ₚ(μ) ≤ ||g||ₚ(μ)`, where `||.||ₚ(μ)` denotes the seminorm (or `ℒp` norm) with respect to the measure `μ`.
|
MeasureTheory.Memℒp.of_le_mul
theorem MeasureTheory.Memℒp.of_le_mul :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F} {c : ℝ},
MeasureTheory.Memℒp g p μ →
MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) → MeasureTheory.Memℒp f p μ
This theorem, `MeasureTheory.Memℒp.of_le_mul`, states that for all types `α`, `E`, `F`, a measurable space `m0`, an extended nonnegative real number `p`, and a measure `μ` on `α`, if `g` is an `α`-to-`F` function in `L^p(μ)` and `f` is an `α`-to-`E` function that is almost everywhere strongly measurable with respect to `μ`, and almost everywhere, the norm of `f(x)` is less than or equal to a constant `c` times the norm of `g(x)`, then `f` is also in `L^p(μ)`. In other words, if a function is bounded by a constant multiple of another function that is in `L^p(μ)`, then the original function is also in `L^p(μ)`. This is an important property in the theory of `L^p` spaces.
More concisely: If a strongly measurable function `f` satisfies almost everywhere `||f(x)|| ≤ c ||g(x)||` for some constant `c` and a measurable function `g` in `L^p(μ)`, then `f` belongs to `L^p(μ)`.
|
MeasureTheory.Memℒp.snorm_lt_top
theorem MeasureTheory.Memℒp.snorm_lt_top :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.Memℒp f p μ → MeasureTheory.snorm f p μ < ⊤
This theorem states that for any types `α` and `E`, where `α` is equipped with a measurable space structure `m0`, `E` is a normed additive commutative group, and `p` is an extended nonnegative real number, if we have a measure `μ` on `α` and a function `f` from `α` to `E` that satisfies the property `MeasureTheory.Memℒp` (which means that `f` is almost everywhere strongly measurable and the p-th power of the integral over the measure space of the norm of `f` raised to the power `p` is finite for `p < ∞`, or the essential supremum of `f` is finite for `p = ∞`), then the seminorm of `f`, `MeasureTheory.snorm f p μ`, is less than infinity. This seminorm is defined differently based on the value of `p`: it is `0` for `p=0`, it is the p-th root of the integral of the p-th power of the norm of `f` for `0 < p < ∞`, and it is the essential supremum of the norm of `f` for `p = ∞`.
More concisely: For any measurable space `(α, m0)`, normed additive commutative group `E`, extended nonnegative real number `p`, measure `μ` on `α`, and almost everywhere strongly measurable function `f` from `α` to `E` satisfying `MeasureTheory.Memℒp`, the seminorm `MeasureTheory.snorm f p μ` is finite.
|
MeasureTheory.snorm_congr_ae
theorem MeasureTheory.snorm_congr_ae :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] {f g : α → F},
μ.ae.EventuallyEq f g → MeasureTheory.snorm f p μ = MeasureTheory.snorm g p μ
The theorem `MeasureTheory.snorm_congr_ae` states that for any two functions `f` and `g` from a measurable space `α` into a normed additive commutative group `F`, if `f` and `g` are equal almost everywhere with respect to a given measure `μ` (i.e., `f =ᶠ[MeasureTheory.Measure.ae μ] g`), then the `ℒp` seminorms of `f` and `g` with respect to the measure `μ` and a specified `p` in the extended nonnegative real numbers are also equal (i.e., `MeasureTheory.snorm f p μ = MeasureTheory.snorm g p μ`).
In other words, if two functions are equal almost everywhere, their `ℒp` seminorms are the same.
More concisely: If two measurable functions from a measurable space into a normed additive commutative group are equal almost everywhere with respect to a given measure, then they have equal `ℒp` seminorms.
|
MeasureTheory.memℒp_top_const
theorem MeasureTheory.memℒp_top_const :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
(c : E), MeasureTheory.Memℒp (fun x => c) ⊤ μ
This theorem states that for any type `α`, any type `E` that forms a normed additive commutative group, any measurable space `m0` over `α`, any measure `μ` of `α`, and any constant `c` of type `E`, the function `f` that maps every element of `α` to `c` satisfies the `Memℒp` property at infinity with respect to `μ`. In mathematical terms, this means that the function `f` is almost everywhere strongly measurable and its essential supremum is finite.
More concisely: For any measurable space `(α, m0)`, any normed additive commutative group `E` with measure `μ`, and any constant `c` in `E`, the function mapping every `x` in `α` to `c` is a strongly measurable function of `α` with finite essential supremum with respect to `μ`.
|
MeasureTheory.snorm_one_eq_lintegral_nnnorm
theorem MeasureTheory.snorm_one_eq_lintegral_nnnorm :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
{f : α → F}, MeasureTheory.snorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
This theorem states that for any measured space 'α', any normed added commutative group 'F', any measurable function 'f' from 'α' to 'F', and any measure 'μ' on 'α', the ℒ¹ seminorm of 'f' (with respect to 'μ') is equal to the Lebesgue integral over 'α' of the nonnegative part of the norm of 'f'. In mathematical language, this is saying that `MeasureTheory.snorm f 1 μ` is equal to `∫⁻ (x : α), ↑‖f x‖₊ ∂μ`, where `‖f x‖₊` denotes the nonnegative part of the norm of 'f' at 'x'.
More concisely: The ℒ¹ norm of a measurable function from a measured space to a normed additive commutative group, with respect to a given measure, equals the Lebesgue integral of the nonnegative part of its norm over the measured space.
|
MeasureTheory.snorm_congr_norm_ae
theorem MeasureTheory.snorm_congr_norm_ae :
∀ {α : Type u_1} {F : Type u_3} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
(∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖) → MeasureTheory.snorm f p μ = MeasureTheory.snorm g p μ
The theorem `MeasureTheory.snorm_congr_norm_ae` states that for any two functions `f` and `g` from a measure space `α` to normed additive commutative groups `F` and `G` respectively, and for any extended nonnegative real number `p` and a measure `μ` on `α`, if the norm of `f(x)` is almost everywhere equal to the norm of `g(x)`, then the seminorm `ℒp` of `f` with respect to `p` and `μ` equals the seminorm `ℒp` of `g` with respect to `p` and `μ`. Here, almost everywhere means except on a set of measure zero. The seminorm `ℒp` is defined as `0` for `p=0`, `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and `essSup ‖f‖ μ` for `p = ∞`.
More concisely: For measurable functions `f: α → F` and `g: α → G` from a measure space `(α, μ)` to normed additive commutative groups `F` and `G` respectively, with `p ≥ 0` an extended real number, if the norms of `f(x)` and `g(x)` are almost equal for all `x ∈ α` except a set of measure zero, then `ℒp(f) = ℒp(g)`, where `ℒp(f)` denotes the seminorm of `f` with respect to `p` and `μ`.
|
MeasureTheory.Memℒp.ae_eq
theorem MeasureTheory.Memℒp.ae_eq :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f g : α → E},
μ.ae.EventuallyEq f g → MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ
The theorem `MeasureTheory.Memℒp.ae_eq` states that for any types `α` and `E`, any measurable space `m0` over `α`, any extended non-negative real number `p`, any measure `μ` on `α`, and any normed additive commutative group `E`, if two functions `f` and `g` from `α` to `E` are equal almost everywhere with respect to the measure `μ` (i.e., they are equal except on a set of measure zero), then if `f` belongs to the space `ℒp` (i.e., `f` is almost everywhere strongly measurable and either the p-th power of the norm of `f` integrated with respect to `μ` is finite if `p` is less than infinity, or the essential supremum of `f` is less than infinity if `p` equals infinity), so does `g`. In mathematical notation, we could write this as: if `f = g` almost everywhere and `f ∈ ℒp(μ)`, then `g ∈ ℒp(μ)`.
More concisely: If two functions are equal almost everywhere and one is in the Lebesgue space Lp with respect to a measure, then the other is also in Lp with respect to that measure.
|
MeasureTheory.memℒp_congr_ae
theorem MeasureTheory.memℒp_congr_ae :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f g : α → E},
μ.ae.EventuallyEq f g → (MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p μ)
This theorem is stating that for any types `α` and `E`, with `α` being a measurable space and `E` being a normed add commutative group, for any extended nonnegative real number `p`, for any measure `μ` on `α`, and for any two functions `f` and `g` from `α` to `E`, if `f` and `g` are equal "almost everywhere" (that is, they are equal except on a set of measure zero), then `f` satisfies the `Memℒp` property (which means that `f` is almost everywhere strongly measurable and its p-th power norm integrated with respect to μ is finite) if and only if `g` also satisfies the `Memℒp` property. This theorem basically confirms that the `Memℒp` property is preserved under changes on sets of measure zero.
More concisely: For measurable spaces `α` and normed add commutative groups `E`, if functions `f` and `g` from `α` to `E` are almost everywhere equal and satisfy the `Memℒp` property for some extended nonnegative real number `p`, then they have interchangeable `Memℒp` status.
|
MeasureTheory.Memℒp.of_bound
theorem MeasureTheory.Memℒp.of_bound :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : α → E},
MeasureTheory.AEStronglyMeasurable f μ → ∀ (C : ℝ), (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) → MeasureTheory.Memℒp f p μ
This theorem states that for any types `α` and `E`, a measure space `m0` on `α`, an extended nonnegative real number `p`, a measure `μ` on `α`, a normed additively commutative group structure on `E`, and a measure `μ` that is finite, if we have a function `f` from `α` to `E` which is almost everywhere strongly measurable with respect to `μ`, then if there exists a real number `C` such that the norm of `f(x)` is less than or equal to `C` for almost all `x` in the measure space, `f` is in the function space `L^p(μ)`. In other words, `f` is almost everywhere strongly measurable and the `p`-th power of the norm of `f`, integrated with respect to `μ`, raised to the power `1/p`, is finite if `p` is finite, or the essential supremum of `f` is finite if `p` is infinity.
More concisely: Given a measure space `(α, m0)`, a finite measure `μ`, an almost everywhere strongly measurable function `f` from `α` to a normed additively commutative group `E`, and a real number `C` such that the norm of `f(x)` is less than or equal to `C` for almost every `x` with respect to `μ`, if the integral of the `p`-th power of the norm of `f` is finite for some finite `p` or the essential supremum of `|f|` is finite when `p = ∞`, then `f` belongs to the `L^p(μ, E)` space.
|
MeasureTheory.Memℒp.norm
theorem MeasureTheory.Memℒp.norm :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp (fun x => ‖f x‖) p μ
The theorem `MeasureTheory.Memℒp.norm` states that given a measurable space `α`, a normed add commutative group `E`, a measure `μ` on `α`, a function `f` mapping from `α` to `E`, and a nonnegative extended real number `p`, if `f` satisfies the property of being almost everywhere strongly measurable and having its `p`th power integral norm finite (if `p` is less than infinity) or its essential supremum finite (if `p` is equal to infinity), denoted by `MeasureTheory.Memℒp f p μ`, then the norm of `f`, represented by the function `(fun x => ‖f x‖)`, also satisfies this property, i.e., `MeasureTheory.Memℒp (fun x => ‖f x‖) p μ`.
More concisely: If a measurable function `f` from a measurable space `α` to a normed add commutative group `E` is almost everywhere strongly measurable and has finite `p`-th power integral norm or essential supremum (if `p` is finite or infinite, respectively), then the norm function `x ↦ ||f x||` is also measurable.
|
MeasureTheory.snorm_zero
theorem MeasureTheory.snorm_zero :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F], MeasureTheory.snorm 0 p μ = 0
This theorem states that for any type `α`, type `F` forming a normed additive commutative group, any measurable space `m0` over `α`, any extended nonnegative real number `p`, and any measure `μ` over the measurable space `α`, the `ℒp` seminorm of the zero function will always be zero. The `ℒp` seminorm, denoted as `MeasureTheory.snorm`, is typically used in the context of measure theory and functional analysis.
More concisely: For any normed additive commutative group `F` over type `α`, measurable space `m0` over `α`, extended nonnegative real number `p`, and measure `μ` over `m0`, the `ℒp` seminorm of the zero function is equal to zero.
|
MeasureTheory.snorm_exponent_zero
theorem MeasureTheory.snorm_exponent_zero :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
{f : α → F}, MeasureTheory.snorm f 0 μ = 0
This theorem states that for any measurable space `α`, any type `F` that forms a normed add commutative group, any measure `μ` on `α`, and any function `f` from `α` to `F`, the `ℒp` seminorm (`MeasureTheory.snorm`) of `f` with exponent `0` and with respect to the measure `μ` is always equal to `0`.
More concisely: For any measurable space `α`, any normed add commutative group `F`, any measure `μ` on `α`, and any `μ`-measurable function `f` from `α` to `F`, the `ℒp` seminorm of `f` with `p = 0` is equal to 0.
|
MeasureTheory.snorm_eq_lintegral_rpow_nnnorm
theorem MeasureTheory.snorm_eq_lintegral_rpow_nnnorm :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F],
p ≠ 0 → p ≠ ⊤ → ∀ {f : α → F}, MeasureTheory.snorm f p μ = (∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
This theorem states that for any non-zero and non-infinite extended nonnegative real number `p`, in a measurable space `α` with a measure `μ`, and a function `f` from `α` to any normed add commutative group `F`, the `ℒp` seminorm of `f` (denoted as `MeasureTheory.snorm f p μ`) is equal to the Lebesgue integral of the nonnegative norm of `f(x)` raised to the power of `p`, and this whole quantity raised to the power of `1 / p`. This Lebesgue integral is denoted as `(∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ)`, where `∫⁻` denotes the Lebesgue integral, and `‖f x‖₊` denotes the nonnegative norm of `f(x)`. The condition that `p ≠ 0` and `p ≠ ⊤` ensures that `p` is a positive finite number.
More concisely: For any measurable function `f` from a measurable space `(α, μ)` with a finite, positive measure `μ` and a non-zero, finite real number `p`, the `ℒp` seminorm of `f` equals the `p-th` power of the Lebesgue integral of the nonnegative norm of `f(x)` raised to the power of `p`.
|
MeasureTheory.snorm_mono_measure
theorem MeasureTheory.snorm_mono_measure :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F] (f : α → F), ν ≤ μ → MeasureTheory.snorm f p ν ≤ MeasureTheory.snorm f p μ
The theorem `MeasureTheory.snorm_mono_measure` states that for any types `α` and `F` with `α` being a measurable space and `F` being a normed additive commutative group, any extended nonnegative real number `p`, and any two measures `μ` and `ν` on `α`, if `ν` is less than or equal to `μ` (i.e., every set that `ν` assigns a finite measure to is also assigned a finite measure by `μ`), then the `ℒp` seminorm of a function `f` from `α` to `F` with respect to the measure `ν` is less than or equal to the `ℒp` seminorm of `f` with respect to the measure `μ`. This theorem asserts the monotonicity of the `ℒp` seminorm with respect to the underlying measure.
More concisely: For any measurable space `α`, normed additive commutative group `F`, extended nonnegative real number `p`, and measures `μ` and `ν` on `α` with `ν` less than or equal to `μ`, the `ℒp` seminorm of a function from `α` to `F` is monotone with respect to the underlying measure, i.e., the seminorm with respect to `ν` is less than or equal to the seminorm with respect to `μ`.
|
MeasureTheory.zero_memℒp
theorem MeasureTheory.zero_memℒp :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E], MeasureTheory.Memℒp 0 p μ
This theorem states that for any type `α` equipped with a measurable space structure `m0`, any extended nonnegative real number `p`, and any measure `μ` on `α`, the zero function (which maps every element of `α` to the zero of a normed additively commutative group `E`) is a member of `ℒp`. In other words, the zero function is almost everywhere strongly measurable and its `p`-th power norm is finite if `p` is less than infinity, or its essential supremum is finite if `p` equals infinity.
More concisely: The zero function is an element of the Lebesgue space `ℒp(α, m0)` for any measurable space `(α, m0)` and normed additively commutative group `E` with respect to any measure `μ` and any `p ∈ [0, ∞)`.
|
MeasureTheory.Memℒp.mono_measure
theorem MeasureTheory.Memℒp.mono_measure :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α → E}, ν ≤ μ → MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp f p ν
The theorem `MeasureTheory.Memℒp.mono_measure` states that for any types `α` and `E`, any measurable space `m0` on `α`, any extended nonnegative real number `p`, and any two measures `μ` and `ν` on `α`, if `ν` is less than or equal to `μ` (in the sense of measures), then if the function `f` from `α` to `E` belongs to the space `L^p(μ)` (i.e., `f` is almost everywhere strongly measurable and `(∫ ‖f a‖^p dμ)^(1/p)` is finite if `p < ∞`, or the essential supremum of `f` is finite if `p = ∞`), then `f` also belongs to the space `L^p(ν)`. This theorem is a kind of monotonicity property of the `L^p` spaces with respect to the underlying measure.
More concisely: If `μ` is a measure larger than or equal to `ν` on a measurable space `(α, ℒ)` and `f` is an `L^p(μ)` function, then `f` is also an `L^p(ν)` function.
|
MeasureTheory.Memℒp.mono
theorem MeasureTheory.Memℒp.mono :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F},
MeasureTheory.Memℒp g p μ →
MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.Memℒp f p μ
The theorem `MeasureTheory.Memℒp.mono` states that for any two functions `f` and `g` from a certain type `α` to normed add-commutative groups `E` and `F` respectively, given a measure `μ` on `α` and a real number `p` in the extended non-negative real numbers, if `g` belongs to the space of `p`-integrable functions (denoted `MeasureTheory.Memℒp g p μ`) and `f` is almost everywhere strongly measurable with respect to measure `μ` (denoted `MeasureTheory.AEStronglyMeasurable f μ`), and if almost everywhere `f` is less than or equal to `g` with respect to the norm (`∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖`), then `f` also belongs to the space of `p`-integrable functions (denoted `MeasureTheory.Memℒp f p μ`). In other words, under these conditions, integrability is preserved under pointwise norm domination.
More concisely: If `f` is almost everywhere strongly measurable, `g` is `p-`integrable, and `‖f x‖ ≤ ‖g x‖ almost everywhere with respect to measure `μ`, then `f` is also `p-`integrable.
|
MeasureTheory.Memℒp.aestronglyMeasurable
theorem MeasureTheory.Memℒp.aestronglyMeasurable :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
{f : α → E} {p : ENNReal}, MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable f μ
This theorem states that for any measurable space `α`, type `E` that is a normed add commutative group, measure `μ` on this space, and function `f` from `α` to `E`, if `f` belongs to the space of essentially `p`-integrable functions (`MeasureTheory.Memℒp f p μ`), then `f` is almost everywhere strongly measurable (`MeasureTheory.AEStronglyMeasurable f μ`). In mathematical terms, this means that `f` is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: If a function `f` from a measurable space `α` to a normed add commutative group `E` is essentially `p`-integrable with respect to measure `μ`, then `f` is almost everywhere strongly measurable.
|
MeasureTheory.Memℒp.restrict
theorem MeasureTheory.Memℒp.restrict :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (s : Set α) {f : α → E},
MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp f p (μ.restrict s)
The theorem `MeasureTheory.Memℒp.restrict` states that for any type `α`, any extended nonnegative real number `p`, any measure `μ` on a measurable space `α`, and any normed additive commutative group `E`, if a function `f` from `α` to `E` belongs to `ℒp(μ)` (i.e., `f` is almost-everywhere strongly measurable and the `p`-th power of the norm of `f` integrated with respect to `μ` is finite), then `f` also belongs to `ℒp(μ.restrict s)` for any subset `s` of `α`. In other words, the `ℒp` property is preserved when the measure is restricted to a subset of the space.
More concisely: If `f` is a function from a measurable space `(α, Σ, μ)` to a normed additive commutative group `E` that belongs to `ℒp(μ)` for some extended nonnegative real number `p`, then `f` also belongs to `ℒp(μ.restrict s)` for any subset `s` of `α`.
|
MeasureTheory.snorm_eq_snorm'
theorem MeasureTheory.snorm_eq_snorm' :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F],
p ≠ 0 → p ≠ ⊤ → ∀ {f : α → F}, MeasureTheory.snorm f p μ = MeasureTheory.snorm' f p.toReal μ
This theorem states that for any measure space `α`, any extended nonnegative real number `p` that is neither `0` nor `∞`, any measure `μ`, and any function `f` from `α` to a normed additive commutative group `F`, the `ℒp` seminorm of `f` with respect to `p` and `μ` is equal to the integral of the `ℒq` seminorm of `f` raised to the power `q` and then to the power of `1/q`. In mathematical terms, for `0 < p < ∞`, we have `(∫ ‖f a‖^p ∂μ) ^ (1/p) = (∫ ‖f a‖^q ∂μ) ^ (1/q)`.
More concisely: For any measure space, measurable function, and finite p > 0, the ℒp and ℒq integrals of the absolute value of the function, with respect to a given measure, are related by the equation (∫ |f(a)|^p dμ)^(1/p) = (∫ |f(a)|^q dμ)^(1/q), where 1/p + 1/q = 1.
|
Mathlib.MeasureTheory.Function.LpSeminorm.Basic._auxLemma.1
theorem Mathlib.MeasureTheory.Function.LpSeminorm.Basic._auxLemma.1 :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
{f : α → E}, MeasureTheory.Memℒp f 0 μ = MeasureTheory.AEStronglyMeasurable f μ
This theorem states that for any measure space `α`, any normed additively commutative group `E`, any measure `μ` on `α`, and any function `f` from `α` to `E`, the property that `f` belongs to the space of `L^p` functions (denoted by `MeasureTheory.Memℒp`) for `p = 0` is equivalent to the property that `f` is almost everywhere strongly measurable (`MeasureTheory.AEStronglyMeasurable`). Here, "almost everywhere strongly measurable" means that `f` is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: For any measure space `α`, any normed additively commutative group `E`, and any measure `μ` on `α`, the function `f` from `α` to `E` belongs to the space of `L^p` functions for `p = 0` if and only if it is almost everywhere strongly measurable.
|
MeasureTheory.snorm_exponent_top
theorem MeasureTheory.snorm_exponent_top :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
{f : α → F}, MeasureTheory.snorm f ⊤ μ = MeasureTheory.snormEssSup f μ
The theorem `MeasureTheory.snorm_exponent_top` states that for any measurable space `α`, any type `F` that forms a normed add commutative group, any measure `μ` on `α`, and any function `f` from `α` to `F`, the `ℒp` seminorm of `f` with exponent `∞` (represented as `MeasureTheory.snorm f ⊤ μ`) equals the essential supremum of `‖f‖` (represented as `MeasureTheory.snormEssSup f μ`). In simpler terms, this theorem shows the equivalence between two ways of measuring the size of functions in the context of measure theory when the exponent is infinity.
More concisely: The `ℒp` seminorm of a measurable function `f` from a measurable space `α` to a normed add commutative group `F` with respect to measure `μ` at infinity equals the essential supreme of the function's norm.
|
MeasureTheory.Memℒp.of_le
theorem MeasureTheory.Memℒp.of_le :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F},
MeasureTheory.Memℒp g p μ →
MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.Memℒp f p μ
The theorem `MeasureTheory.Memℒp.of_le` states that for all types `α`, `E`, and `F`, a measurable space `m0` on `α`, an extended real number `p`, and a measure `μ` on `α`, and given normed add commutative groups over `E` and `F`, if a function `g` from `α` to `F` belongs to the space of `ℒp` functions with respect to measure `μ` (`MeasureTheory.Memℒp g p μ`), a function `f` from `α` to `E` is almost everywhere strongly measurable with respect to measure `μ` (`MeasureTheory.AEStronglyMeasurable f μ`), and for almost every `x` in `α` the norm of `f x` is less than or equal to the norm of `g x` (`∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖`), then `f` also belongs to the space of `ℒp` functions with respect to measure `μ` (`MeasureTheory.Memℒp f p μ`). This theorem is essentially saying that the set of `ℒp` functions is closed under taking almost everywhere less-than-or-equal-to bounded variants.
More concisely: If a function `f` from a measurable space to a normed add commutative group is almost everywhere strongly measurable, belongs to `ℒp` for some `p`, and has almost everywhere norm less than or equal to another `ℒp` function `g`, then `f` is also in `ℒp`.
|
MeasureTheory.snorm_measure_zero
theorem MeasureTheory.snorm_measure_zero :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] [inst_1 : MeasurableSpace α]
{f : α → F}, MeasureTheory.snorm f p 0 = 0
This theorem states that for any type `α`, any normed additive commutative group `F`, and any extended nonnegative real number `p`, if we have a function `f` from `α` to `F`, then the `ℒp` seminorm of `f` with respect to the measure `0` is always `0`. In other words, if the measure of the space is zero, then the seminorm of any function on that space is also zero, regardless of the value of `p`.
More concisely: For any type `α`, normed additive commutative group `F`, and extended nonnegative real number `p`, the `ℒp` seminorm of any function from `α` to `F` is zero when the measure of the domain is zero.
|
MeasureTheory.Memℒp.neg
theorem MeasureTheory.Memℒp.neg :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α → E}, MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp (-f) p μ
The theorem `MeasureTheory.Memℒp.neg` states that for any measurable space `α`, any type `E` that forms a normed additive commutative group, any extended nonnegative real number `p`, any measure `μ` on `α`, and any function `f` from `α` to `E`, if `f` satisfies the property `Memℒp` (i.e., `f` is almost everywhere strongly measurable and the L^p norm of `f` is finite if `p` is less than infinity or the essential supremum of `f` is finite if `p` equals infinity), then the negation of `f` (i.e., `-f`) also satisfies the property `Memℒp`. This theorem essentially asserts that the `Memℒp` property is preserved under taking negations.
More concisely: If `f` is a measurable function from a measurable space to a normed additive commutative group with finite L^p norm or essential supremum, then the negation of `f` also satisfies the same property.
|
MeasureTheory.snorm'_zero
theorem MeasureTheory.snorm'_zero :
∀ {α : Type u_1} {F : Type u_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup F], 0 < q → MeasureTheory.snorm' 0 q μ = 0
The theorem `MeasureTheory.snorm'_zero` states that for any measurable space `α`, type `F` that forms a normed additively commutative group, a real number `q` such that `0 < q`, and a measure `μ` on `α`, the `snorm'` of the zero function (a function that maps every element of `α` to `0` in `F`) with respect to measure `μ` and exponent `q` is `0`. In other words, the seminorm, calculated as the `q`-th power mean of the norms of the function values (with `q` > 0), of the zero function is `0`.
More concisely: For any measurable space, normed additively commutative group, real number `q` with `0 < q`, and measure, the seminorm of the zero function with respect to the measure and exponent `q` equals `0`.
|
MeasureTheory.memℒp_const
theorem MeasureTheory.memℒp_const :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (c : E) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Memℒp (fun x => c) p μ
The theorem `MeasureTheory.memℒp_const` states that for any type `α` with a measurable space structure `m0`, any extended nonnegative real number `p`, any measure `μ` on `α`, any normed add commutative group `E`, and any element `c` of `E` such that `μ` is a finite measure, the constant function `fun x => c` is a member of `ℒp` space with respect to measure `μ`. This means that the function is almost everywhere strongly measurable and its `p`-th power norm integrated over `μ` is finite if `p` is less than infinity, or its essential supremum is less than infinity if `p` equals infinity.
More concisely: For any measurable space `(α, m0)`, normed add commutative group `E`, finite measure `μ` on `α`, extended nonnegative real number `p`, and constant function `c : E`, the function `fun x => c` belongs to the `Lp` space `ℒp(α, E, μ)`.
|
MeasureTheory.memℒp_zero_iff_aestronglyMeasurable
theorem MeasureTheory.memℒp_zero_iff_aestronglyMeasurable :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
{f : α → E}, MeasureTheory.Memℒp f 0 μ ↔ MeasureTheory.AEStronglyMeasurable f μ
This theorem states that for any types `α` and `E`, if `α` is a measurable space, `μ` is a measure on `α`, and `E` is a normed additive commutative group, then a function `f` from `α` to `E` belongs to the space `ℒp` for `p=0` with respect to the measure `μ` if and only if `f` is "almost everywhere strongly measurable" with respect to `μ`. Here, "almost everywhere strongly measurable" means that `f` is almost everywhere equal to the limit of a sequence of simple functions. In the context of the `ℒp` space for `p=0`, a function belongs to this space if it is almost everywhere strongly measurable and the essential supremum of the function is finite.
More concisely: A function from a measurable space to a normed additive commutative group belongs to the ℒp space for p=0 with respect to a measure if and only if it is almost everywhere strongly measurable.
|