MeasureTheory.indicatorConstLp_disjoint_union
theorem MeasureTheory.indicatorConstLp_disjoint_union :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : ↑↑μ s ≠ ⊤)
(hμt : ↑↑μ t ≠ ⊤),
s ∩ t = ∅ →
∀ (c : E),
MeasureTheory.indicatorConstLp p ⋯ ⋯ c =
MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p ht hμt c
This theorem states that for any measure space `α`, any normed add commutative group `E`, any extended nonnegative real number `p`, and any measure `μ` on `α`, given two sets `s` and `t` in `α` that are measurable and with finite measure, if the intersection of `s` and `t` is empty (`s` and `t` are disjoint), then for every element `c` in `E`, the indicator function of the disjoint union of `s` and `t` is equal to the sum of the indicator functions of `s` and `t`. The indicator function here is represented in the space of `p`-integrable functions (`MeasureTheory.Lp E p μ`).
In mathematical terms, this theorem is often understood as stating that the indicator function of the disjoint union of two sets is the sum of the indicators of the sets. This is an essential property of indicator functions in measure theory.
More concisely: For any measure space, normed add commutative group, and measure, the indicator functions of two disjoint, measurable sets with finite measure are equal to the indicator function of their disjoint union in the space of `p`-integrable functions.
|
MeasureTheory.Lp.coeFn_add
theorem MeasureTheory.Lp.coeFn_add :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), μ.ae.EventuallyEq (↑↑(f + g)) (↑↑f + ↑↑g)
This theorem, `MeasureTheory.Lp.coeFn_add`, states that for any measure space `α`, type `E` that forms a normed additive commutative group, an extended nonnegative real number `p`, measure `μ`, and two elements `f` and `g` of the Lp space over `E` with respect to `p` and `μ`, the function application of the sum `f + g` is almost everywhere equal to the sum of the function applications of `f` and `g`. In other words, this theorem asserts the almost everywhere pointwise additivity of elements in the Lp space.
More concisely: For any measure space, normed additive commutative group, measure, and elements in the Lp space, their sum is almost everywhere equal to the pointwise sum of their functions.
|
MeasureTheory.indicatorConstLp_coeFn
theorem MeasureTheory.indicatorConstLp_coeFn :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : ↑↑μ s ≠ ⊤} {c : E},
μ.ae.EventuallyEq (↑↑(MeasureTheory.indicatorConstLp p hs hμs c)) (s.indicator fun x => c)
This theorem states that for any measurable set `s` in a measurable space `α`, and for any constant `c` of type `E` in a normed additive commutative group, the function equivalence of the indicator function that takes on the constant value `c` in the set `s` and zero elsewhere holds almost everywhere with respect to a measure `μ`, if the measure of the set `s` under `μ` is not infinity. This is implemented through the `MeasureTheory.indicatorConstLp` function, which returns an extended nonnegative real number `p`. In other words, the measure-theoretic `Lp` indicator function of a set is almost everywhere equal to the simple indicator function of the set.
More concisely: For any measurable set `s` in a measurable space with finite measure `μ`, and for any constant `c`, the indicator function of `s` equals `c` almost everywhere if and only if the `Lp` norm of the difference between the indicator function and the constant function is finite.
|
MeasureTheory.exists_snorm_indicator_le
theorem MeasureTheory.exists_snorm_indicator_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E],
p ≠ ⊤ →
∀ (c : E) {ε : ENNReal},
ε ≠ 0 → ∃ η, 0 < η ∧ ∀ (s : Set α), ↑↑μ s ≤ ↑η → MeasureTheory.snorm (s.indicator fun x => c) p μ ≤ ε
This theorem states that for any `p` in the extended nonnegative real numbers, except infinity, and for any nonzero `ε` in the extended nonnegative real numbers, there exists a `η` in the extended nonnegative real numbers such that for any set `s` of type `α`, if the measure of `s` is less than or equal to `η`, then the `ℒ^p` norm of the indicator function of `s` (which assigns the value `c` to elements in `s` and `0` otherwise) is less than or equal to `ε`. This expresses the idea that the `ℒ^p` norm of the indicator function of a set becomes arbitrarily small when the measure of the set becomes small, for all `p` less than infinity.
More concisely: For any `p` finite and any nonzero `ε`, there exists an `η` such that the `ℒ^p` norm of the indicator function of any set with measure less than `η` is less than `ε`.
|
MeasureTheory.Lp.mul_meas_ge_le_pow_norm'
theorem MeasureTheory.Lp.mul_meas_ge_le_pow_norm' :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)),
p ≠ 0 → p ≠ ⊤ → ∀ (ε : ENNReal), ε ^ p.toReal * ↑↑μ {x | ε ≤ ↑‖↑↑f x‖₊} ≤ ENNReal.ofReal ‖f‖ ^ p.toReal
This theorem is a version of Markov's inequality for elements of `Lp` spaces. For a given measurable space `α`, a normed commutative addition group `E`, a measure `μ` on `α`, a nonnegative real number `p` that is not infinity, and a function `f` from `α` to `E` that belongs to the `Lp` space, if `ε` is a nonnegative real number, then the measure of the set of elements `x` in `α` where `ε` is less than or equal to the norm of `f(x)` times `ε` raised to the power of `p`, is less than or equal to the norm of `f` raised to the power of `p`. This inequality holds when `p` is not equal to 0 or infinity.
More concisely: For measurable spaces `α`, normed commutative addition groups `E`, measures `μ`, real numbers `p ≠ 0, ∞`, and `Lp` functions `f` on `α` to `E`, the measure of `{x : α | ε <= ||f x||p}` is less than or equal to `||f||p^p` for all `ε >= 0`.
|
MeasureTheory.Lp.nnnorm_def
theorem MeasureTheory.Lp.nnnorm_def :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖f‖₊ = (MeasureTheory.snorm (↑↑f) p μ).toNNReal
The theorem `MeasureTheory.Lp.nnnorm_def` states that for any measure space `α`, any extended nonnegative real number `p`, any measure `μ` on `α`, and any element `f` in the `Lp` space of a normed add commutative group `E`, the non-negative norm of `f`, denoted as `‖f‖₊`, is equal to the `ℒp` seminorm of `f`, denoted as `MeasureTheory.snorm (↑↑f) p μ`, converted to a non-negative real number. This `ℒp` seminorm might be defined differently based on the value of `p`: it's `0` if `p=0`, it's `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and it's `essSup ‖f‖ μ` for `p = ∞`.
More concisely: For any measure space, extended nonnegative real number `p`, measure `μ`, and `Lp` space element `f`, the non-negative norm `‖f‖₊` equals the `ℒp` seminorm `Measure Theory.snorm (↑↑f) p μ` of `f`. The `ℒp` seminorm's value depends on `p`: it's `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞` and `essSup ‖f‖ μ` for `p = ∞`.
|
MeasureTheory.snorm_indicator_const
theorem MeasureTheory.snorm_indicator_const :
∀ {α : Type u_1} {G : Type u_4} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup G] {s : Set α} {c : G},
MeasurableSet s →
p ≠ 0 → p ≠ ⊤ → MeasureTheory.snorm (s.indicator fun x => c) p μ = ↑‖c‖₊ * ↑↑μ s ^ (1 / p.toReal)
This theorem states that for any type `α`, any normed additive commutative group `G`, any measurable space `m0` on `α`, any extended non-negative real number `p`, any measure `μ` on `α`, any set `s` of `α`, and any element `c` of `G`, given that the set `s` is measurable, and `p` is neither 0 nor infinity, the seminorm of the indicator function of the set `s` (which maps each element in `s` to `c` and all other elements to zero) according to measure `μ` and `p` equals to the non-negative real number norm of `c` times the power of the measure of the set `s` to the reciprocal of `p`. In mathematical terms, if `s` is measurable and `p` is any real number except 0 and infinity, then we have `∥indicator s (λx, c)∥_p = ∥c∥ * μ(s)^(1/p)`.
More concisely: For any measurable set `s` in a measurable space `(α, m0)`, the $L^p$ norm of the indicator function of `s` with value `c` for all elements in `s` and 0 for all other elements is equal to `|c| * (measure of `s`) ^(1/p)`, where `p` is any real number excluding 0 and infinity.
|
MeasureTheory.Lp.stronglyMeasurable
theorem MeasureTheory.Lp.stronglyMeasurable :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.StronglyMeasurable ↑↑f
This theorem states that for any measurable space `α`, normed addative commutative group `E`, measure `μ` on `α`, and function `f` in the `Lp` space over `E` with respect to `μ` and a nonnegative extended real number `p`, the function `f` is strongly measurable. Strongly measurable here means that the function `f` is the limit of a sequence of simple functions.
More concisely: Any `Lp` function on a measurable space with respect to a measure is strongly measurable.
|
ContinuousLinearMap.coeFn_compLp
theorem ContinuousLinearMap.coeFn_compLp :
∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_5} [inst_2 : NontriviallyNormedField 𝕜]
[inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] F) (f : ↥(MeasureTheory.Lp E p μ)),
∀ᵐ (a : α) ∂μ, ↑↑(L.compLp f) a = L (↑↑f a)
This theorem states that for any α of type 'Type u_1', any E and F of Types 'u_2' and 'u_3' respectively, given a measurable space m0, a measure μ on α, and an extended nonnegative real number p, under the norms of additive commutative group E and F, a nontrivially normed field 𝕜, and normed spaces E and F over 𝕜, for any continuous linear map L from E to F, and for any function f in the Lp space defined on E, p, and μ, it holds almost everywhere with respect to the measure μ that the value of the function (L composed with f) at any point α is equal to the value of L applied to f at the point α.
In mathematical terms, this theorem states that for a function in the Lp space, the composition of the function with a continuous linear map is equal to the application of the map to the function, almost everywhere with respect to the measure.
More concisely: For any continuous linear map L between normed spaces and any function in the Lp space, the value of L(f) is almost everywhere equal to f(L) when composed.
|
MeasureTheory.Lp.norm_compMeasurePreserving
theorem MeasureTheory.Lp.norm_compMeasurePreserving :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {β : Type u_5} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
{f : α → β} (g : ↥(MeasureTheory.Lp E p μb)) (hf : MeasureTheory.MeasurePreserving f μ μb),
‖(MeasureTheory.Lp.compMeasurePreserving f hf) g‖ = ‖g‖
This theorem states that for any measure-preserving function `f` from a measurable space `α` to a measurable space `β`, and for any function `g` from the Lp space over the measure space `β`, the Lp norm of the composition of `f` and `g` (after the measure-preserving transformation by `f`) is equal to the Lp norm of `g`. Here, the Lp space is a space of functions that are measurable with respect to a given measure, and the norm involves integration according to the measure and the p-th power of the absolute value of the function. The theorem hence states that measure-preserving transformations do not change the Lp norm of functions in the Lp space. The Lp norm is a generalization of the Euclidean norm and is used extensively in functional analysis and measure theory.
More concisely: For any measure-preserving function `f` from a measurable space `α` to a measurable space `β` and any function `g` in the Lp space over `β`, the Lp norm of `g ∘ f` equals the Lp norm of `g`.
|
MeasureTheory.Lp.norm_def
theorem MeasureTheory.Lp.norm_def :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖f‖ = (MeasureTheory.snorm (↑↑f) p μ).toReal
This theorem establishes a definition for the norm of a function in a Lp space. Specifically, for any measurable space `α`, any normed add commutative group `E`, any measure `μ` on `α`, and any function `f` in the Lp space over `E` with measure `μ` and norm `p` (where `p` is an extended nonnegative real number), the norm of the function `f` (`‖f‖`) is defined to be the real part of the Lp seminorm (`MeasureTheory.snorm`) of the function `f`. The Lp seminorm is defined differently depending on the value of `p`: it equals `0` for `p=0`, `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and the essential supremum of `‖f‖` over `μ` for `p = ∞`.
More concisely: For any measurable space `α`, normed add commutative group `E`, measure `μ` on `α`, and function `f` in the Lp space over `E` with measure `μ` and norm `p`, the norm of `f` equals the real part of the Lp seminorm of `f`, where the Lp seminorm is `0` for `p=0`, `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and the essential supremum of `‖f‖` over `μ` for `p = ∞`.
|
MeasureTheory.Lp.coeFn_zero
theorem MeasureTheory.Lp.coeFn_zero :
∀ {α : Type u_1} (E : Type u_2) {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
[inst : NormedAddCommGroup E], μ.ae.EventuallyEq (↑↑0) 0
This theorem, `MeasureTheory.Lp.coeFn_zero`, states that for any type `α`, any normed additively commutative group `E`, any measurable space `m0` on `α`, any extended nonnegative real number `p`, and any measure `μ` on `α`, it is almost everywhere true (according to the measure `μ`) that the double coercion of `0` is equal to `0`. In this context, "almost everywhere" means on all sets except a set of measure zero. The double coercion is a technical detail related to the way numbers are represented in the Lean 4 type system. Essentially, this theorem is stating that zero is zero almost everywhere.
More concisely: For any measurable space `(α, μ)`, normed additively commutative group `E`, and extended nonnegative real number `p`, the double coercion of `0` is equal to `0` almost everywhere in `E` with respect to `μ`.
|
BoundedContinuousFunction.Lp_norm_le
theorem BoundedContinuousFunction.Lp_norm_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α] [inst_2 : BorelSpace α]
[inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E),
‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * ‖f‖
The theorem `BoundedContinuousFunction.Lp_norm_le` states that for any bounded continuous function `f` from a measurable space `α` to a normed add-commutative group `E` with a finite measure `μ` and given a `p` in the set of extended nonnegative real numbers (`ENNReal`), the `Lp`-norm of this function is less than or equal to the measure of the whole space (considered as `ℝ≥0`) raised to the power of the reciprocal of `p`, multiplied by the sup-norm of the function `f`.
In other words, this theorem states a bound on the `Lp`-norm of a bounded continuous function in terms of its sup-norm, with a constant factor that depends on the measure of the entire space. The function is defined on a measurable space with a finite measure, it is continuous and bounded, and the space is equipped with a topological space structure that is Borel and second countable.
More concisely: For any bounded continuous function from a finite measure measurable space to a normed add-commutative group, its `Lp`-norm is bounded above by the sup-norm multiplied by the measure's square root of reciprocal `p`.
|
LipschitzWith.comp_memℒp
theorem LipschitzWith.comp_memℒp :
∀ {p : ENNReal} {α : Type u_5} {E : Type u_6} {F : Type u_7} {K : NNReal} [inst : MeasurableSpace α]
{μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] {f : α → E}
{g : E → F}, LipschitzWith K g → g 0 = 0 → MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp (g ∘ f) p μ
This theorem states that if a function `g` is Lipschitz continuous with a nonnegative real constant `K` and `g(0) = 0`, and a function `f` belongs to the space of `p`-integrable functions (in the sense of `MeasureTheory.Memℒp`), then the composition of `g` and `f` (i.e., `g ∘ f`) also belongs to this space of `p`-integrable functions. Here, `p` is an extended nonnegative real number (which can be infinity), and `f` and `g` are functions from a measurable space `α` to normed add-commutative groups `E` and `F` respectively. The measure on the space `α` is given by `μ`.
More concisely: If `g` is a Lipschitz continuous function with `g(0) = 0` and has a nonnegative real constant `K`, and `f` is `p`-integrable, then the composition `g ∘ f` is also `p`-integrable for any extended nonnegative real number `p`.
|
MeasureTheory.Lp.snorm_ne_top
theorem MeasureTheory.Lp.snorm_ne_top :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.snorm (↑↑f) p μ ≠ ⊤
The theorem `MeasureTheory.Lp.snorm_ne_top` states that for any measurable space `α`, any type `E` that has a normed add commutative group structure, any extended nonnegative real number `p`, any measure `μ` on `α`, and any function `f` in the Lp space over `α` with respect to `E`, `p`, and `μ`, the Lp seminorm (`MeasureTheory.snorm`) of `f` with respect to `p` and `μ` is not equal to positive infinity. In mathematical terms, this asserts that all functions in the Lp space have finite Lp seminorm.
More concisely: For any measurable space, normed add commutative group, measure, and Lp function, their Lp seminorm is finite.
|
MeasureTheory.Memℒp.coeFn_toLp
theorem MeasureTheory.Memℒp.coeFn_toLp :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.Memℒp f p μ),
μ.ae.EventuallyEq (↑↑(MeasureTheory.Memℒp.toLp f hf)) f
This theorem states that for any function `f` from `α` to `E` and for any measure `μ` on the measurable space `α`, if the function `f` satisfies the property `Memℒp` (which means the function is almost everywhere (ae) strongly measurable and its Lp norm is finite), then the function representation in Lp space obtained by `Memℒp.toLp` is almost everywhere equal to the original function `f`. In mathematical terms, it means if `f:α→E` is in `Lp` space (denoted by `Memℒp f p μ`), then `f` is almost everywhere equal to the function represented in `Lp` space (denoted by `MeasureTheory.Memℒp.toLp f hf`). Here, "almost everywhere" refers to the set of points where a property holds except for a set of measure zero, defined by `MeasureTheory.Measure.ae μ`.
More concisely: If a function `f: α → E` is almost everywhere (ae) strongly measurable with finite Lp norm, then `f` is a.e. equal to its representation in the Lp space obtained by `Memℒp.toLp`.
|
MeasureTheory.Lp.mem_boundedContinuousFunction_iff
theorem MeasureTheory.Lp.mem_boundedContinuousFunction_iff :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α] [inst_2 : BorelSpace α]
[inst_3 : SecondCountableTopologyEither α E] {f : ↥(MeasureTheory.Lp E p μ)},
f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔ ∃ f₀, ContinuousMap.toAEEqFun μ f₀.toContinuousMap = ↑f
This theorem states that for any measurable space `α`, type `E`, measure `μ`, and `f` in `Lp(E, p, μ)`, `f` is in `Lp.boundedContinuousFunction(E, p, μ)` if and only if there exists a `f₀` such that when `f₀` is converted to a continuous map and then to an `AEEqFun` with respect to measure `μ`, it equals `f`. In simpler terms, an element of Lp space with measure `μ` is considered to have a bounded continuous representative if we can find some `f₀` that, when regarded as a continuous map and then as an almost everywhere equal function (AEEqFun), gives the original element in the Lp space. This theorem bridges the gap between Lp spaces and bounded continuous functions.
More concisely: A function in the Lp space with respect to a measure is equivalent to a bounded continuous function if and only if it has a representative that can be converted to a continuous function and an almost everywhere equal function with respect to that measure.
|
BoundedContinuousFunction.mem_Lp
theorem BoundedContinuousFunction.mem_Lp :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α] [inst_2 : BorelSpace α]
[inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E), ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ MeasureTheory.Lp E p μ
This theorem states that any bounded continuous function on a finite-measure space belongs to the Lp space. Here, `α` is the type representing the set, `E` is the type representing the elements of the function, `m0` is the measurable space, `p` is the extended nonnegative real number representing the Lp norm, and `μ` is the measure. The function `f` is a bounded continuous function from `α` to `E`. The theorem asserts that the function `f`, when coerced to a measurable function using the provided function `toAEEqFun`, is an element of the Lp space as defined by `MeasureTheory.Lp E p μ`. The assumptions include the requirements that `E` forms a normed addition commutative group, `α` has a topological space structure, and `α` has a Borel space structure. Moreover, `α` and `E` should have a second countable topology, and the measure `μ` should be finite.
More concisely: Any bounded and continuous function from a second countable measurable space with a finite measure to a normed additive commutative group is an element of the Lp space with respect to that measure.
|
MeasureTheory.Lp.memℒp
theorem MeasureTheory.Lp.memℒp :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.Memℒp (↑↑f) p μ
This theorem states that for any measure space `α`, normed additive commutative group `E`, extended nonnegative real numbers `p`, measure `μ` on `α`, and function `f` in the Lp space of measurable functions from `α` to `E`, the function `f` satisfies the property of being almost everywhere strongly measurable and having finite Lp norm (`∫ ‖f a‖^p ∂μ)^(1/p)` is finite if `p < ∞`, or `essSup f < ∞` if `p = ∞`). In other words, any function in the Lp space is in the set of functions for which the Lp norm is finite almost everywhere.
More concisely: Any function in the Lp space of measurable functions from a measure space to a normed additive commutative group has finite Lp norm almost everywhere when the real number p is finite, or essential supremum is finite when p is infinite.
|
MeasureTheory.Lp.aestronglyMeasurable
theorem MeasureTheory.Lp.aestronglyMeasurable :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), MeasureTheory.AEStronglyMeasurable (↑↑f) μ
The theorem `MeasureTheory.Lp.aestronglyMeasurable` states that for any measurable space `α`, type `E` that forms a normed additive commutative group, extended nonnegative real number `p`, and a measure `μ` on `α`, every function `f` that lies in the `Lp` space (the space of functions whose p-th power of absolute value is integrable) with respect to `E`, `p`, and `μ`, is almost everywhere strongly measurable with respect to the measure `μ`. In other words, `f` is equal almost everywhere to the limit of a sequence of simple functions (functions that take a finite number of values), as defined by the `AEStronglyMeasurable` property.
More concisely: Every `Lp` function on a measurable space with respect to a given measure is almost everywhere equal to a simple function.
|
MeasureTheory.memℒp_indicator_const
theorem MeasureTheory.memℒp_indicator_const :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
{s : Set α} (p : ENNReal),
MeasurableSet s → ∀ (c : E), c = 0 ∨ ↑↑μ s ≠ ⊤ → MeasureTheory.Memℒp (s.indicator fun x => c) p μ
The theorem `MeasureTheory.memℒp_indicator_const` states that for any type `α`, type `E` (where `E` is a normed add commutative group), a measurable space `m0` on `α`, a measure `μ` on `α`, a set `s` of `α`, and a constant `c` from `E`, if `s` is measurable and either `c` equals zero or the measure of `s` is not infinity, then the function that assigns `c` to each element in `s` and `0` to each element not in `s` (which is denoted by `Set.indicator s fun x => c`) is in `L^p` space with respect to the measure `μ`. In other words, this function is almost everywhere strongly measurable and its `p`-th power integral is finite if `p` is less than infinity or its essential supremum is less than infinity if `p` equals infinity.
More concisely: If `s` is a measurable subset of a measurable space `(α, m0)` with finite measure `μ` or `μ(s) = 0`, then the indicator function `x ↦ χ\_s(x) := if x ∈ s then c else 0` belongs to the `L^p(μ)` space for any `p ≤ ∞`.
|
MeasureTheory.Lp.lipschitzWith_pos_part
theorem MeasureTheory.Lp.lipschitzWith_pos_part : LipschitzWith 1 fun x => max x 0
This theorem states that the function `max x 0`, which yields the maximum of `x` and `0`, is Lipschitz continuous with a Lipschitz constant of `1`. More formally, for any two inputs `x` and `y`, the distance in the pseudo metric space between `max x 0` and `max y 0` is less than or equal to `1` times the distance between `x` and `y`.
More concisely: The function `max x 0` is Lipschitz continuous with Lipschitz constant 1 in the pseudo metric space. That is, |max x 0 - max y 0| ≤ |x - y| for all x and y.
|
MeasureTheory.Lp.ext
theorem MeasureTheory.Lp.ext :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f g : ↥(MeasureTheory.Lp E p μ)}, μ.ae.EventuallyEq ↑↑f ↑↑g → f = g
This theorem states that for any type `α`, any type `E` that forms a normed add commutative group, any measurable space `m0` on `α`, any extended nonnegative real number `p`, and any measure `μ` on `α`, if `f` and `g` are elements of the `Lp` space defined over `E` with respect to the measure `μ` and `p`, then if `f` and `g` are equal almost everywhere (i.e., they are equal except on a set of measure zero), then `f` and `g` are considered equal. In other words, two functions in the `Lp` space are considered the same if they differ only on a set of measure zero.
More concisely: For any measurable spaces `α`, `E` with `E` being a normed add commutative group, measure `μ` on `α`, and `p` an extended nonnegative real number, if `f` and `g` are equal almost everywhere in the `Lp` space over `E` with respect to `μ`, then `f` and `g` are equal as elements of `Lp`.
|
MeasureTheory.Lp.norm_toLp
theorem MeasureTheory.Lp.norm_toLp :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : α → E) (hf : MeasureTheory.Memℒp f p μ),
‖MeasureTheory.Memℒp.toLp f hf‖ = (MeasureTheory.snorm f p μ).toReal
This theorem states that for any type `α`, type `E` forming a normed additive commutative group, a measurable space `m0` on `α`, an extended nonnegative real `p`, a measure `μ` on `α`, and a function `f` from `α` to `E` that satisfies the `Memℒp` property, the norm of the element in Lp space corresponding to `f`, obtained via `Memℒp.toLp`, is equal to the real part of the `ℒp` seminorm of `f` with respect to measure `μ` and `p`.
In other words, for a function `f` that is almost everywhere strongly measurable and whose `ℒp` seminorm is finite, when this function is mapped to an Lp space, the norm of the resulting element is the same as the `ℒp` seminorm of the original function. The `ℒp` seminorm, denoted `MeasureTheory.snorm`, is defined as `0` for `p=0`, as the essential supremum of `‖f a‖` with respect to measure `μ` for `p = ∞`, and as `∫ ‖f a‖^p ∂μ` to the power of `1/p` for `0 < p < ∞`.
More concisely: For any measurable space `(α, μ)`, type `E` forming a normed additive commutative group, and a measurable function `f: α → E` satisfying the `Memℒp` property with finite `ℒp` seminorm, the Lp norm of `Memℒp.toLp f` equals the `ℒp` seminorm of `f` with respect to `μ` and `p`.
|
MeasureTheory.Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top
theorem MeasureTheory.Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
{p q : ENNReal} {f : α → E},
MeasureTheory.Memℒp f q μ → ∀ {s : Set α}, (∀ x ∉ s, f x = 0) → ↑↑μ s ≠ ⊤ → p ≤ q → MeasureTheory.Memℒp f p μ
This theorem says that if a function is part of the space `ℒ^p` and is supported on a set with finite measure, then this function also belongs to the space `ℒ^q` for any `q` that is less than or equal to `p`. More specifically, given a function `f` from a type `α` to a Normed Additive Commutative Group `E`, and a measure `μ` on `α`, if `f` has the property that `(∫ ‖f a‖^q ∂μ)^(1/q)` is finite (i.e., `f` belongs to `ℒ^q`) and for any `x` not in a certain set `s`, `f(x)` equals zero, and the measure of `s` is not infinity, then if `p` is less than or equal to `q`, `f` also belongs to `ℒ^p`, which means that `(∫ ‖f a‖^p ∂μ)^(1/p)` is finite.
More concisely: If `f` is a measurable function from a measure space to a Normed Additive Commutative Group, with finite `μ`-measure support and finite `μ`-integrals of `‖f‖^q` for some `q ≤ p`, then `f` belongs to `ℒ^p`.
|
MeasureTheory.Lp.mem_Lp_iff_memℒp
theorem MeasureTheory.Lp.mem_Lp_iff_memℒp :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] {f : α →ₘ[μ] E}, f ∈ MeasureTheory.Lp E p μ ↔ MeasureTheory.Memℒp (↑f) p μ
This theorem establishes an equivalence relationship between two key concepts in measure theory. For any measure space `α`, type `E`, measurable space `m0`, extended nonnegative real number `p`, measure `μ`, and function `f` from `α` to `E` that is integrable with respect to `μ`, the function `f` belongs to the Lp space with respect to `E`, `p`, and `μ` if and only if `f` satisfies the Memℒp property. The Memℒp property signifies that `f` is almost everywhere strongly measurable and the integral of the p-th power of its norm with respect to `μ` is finite (when `p < ∞`) or the essential supremum of `f` is finite (when `p = ∞`).
More concisely: For any measurable function `f` from a measure space to a normed vector space with finite p-th moment, with respect to a given measure, `f` belongs to the Lp space if and only if it satisfies the Memℒp property.
|
MeasureTheory.Memℒp.snorm_mk_lt_top
theorem MeasureTheory.Memℒp.snorm_mk_lt_top :
∀ {α : Type u_5} {E : Type u_6} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
[inst_1 : NormedAddCommGroup E] {p : ENNReal} {f : α → E} (hfp : MeasureTheory.Memℒp f p μ),
MeasureTheory.snorm (↑(MeasureTheory.AEEqFun.mk f ⋯)) p μ < ⊤
The theorem `MeasureTheory.Memℒp.snorm_mk_lt_top` states that for any measurable space `α`, any normed add commutative group `E`, any measure `μ` on `α`, any extended nonnegative real number `p`, and any function `f` from `α` to `E` that satisfies the property `MeasureTheory.Memℒp` (which signifies that `f` is almost everywhere strongly measurable and its Lp-norm is finite), the seminorm in `ℒp` of the equivalence class `[f]` of `f` (constructed based on the equivalence relation of being almost everywhere equal) is strictly less than infinity. In mathematical terms, this says that if $\|f\|_p$ is finite, then the `ℒp` seminorm of the equivalence class of `f`, denoted as $\| [f] \|_p$, is also finite.
More concisely: For any measurable space, normed add commutative group, measure, extended nonnegative real number, and almost everywhere strongly measurable function with finite Lp-norm, the Lp-seminorm of its equivalence class is finite.
|
ContinuousMap.toLp_norm_le
theorem ContinuousMap.toLp_norm_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
[inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α] [inst_2 : BorelSpace α]
[inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
{𝕜 : Type u_5} [inst_6 : Fact (1 ≤ p)] [inst_7 : NontriviallyNormedField 𝕜] [inst_8 : NormedSpace 𝕜 E],
‖ContinuousMap.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹
This theorem establishes a bound for the operator norm of `ContinuousMap.toLp`. Given a measurable space `α`, a type `E` that forms a normed additive commutative group, a topological space `α`, a Borel space `α`, a second countable topology on the Cartesian product of `α` and `E`, a compact space `α`, a finite measure `μ` on `α`, an extended nonnegative real number `p`, and a nontrivially normed field `𝕜` that also forms a normed space with `E`; the operator norm of the mapping from continuous maps to `Lp` spaces, `ContinuousMap.toLp`, is less than or equal to the nonnegative real number representation of the measure of the whole space with respect to `μ`, raised to the inverse real part of `p`. This result is particularly useful for bounding the size of the operator in terms of the space and measure used.
More concisely: The operator norm of `ContinuousMap.toLp` from the space of continuous functions to the `Lp` space with respect to a compact measurable space and finite measure is bounded above by the measure of the space raised to the power of 1/p.
|
MeasureTheory.Lp.coeFn_sub
theorem MeasureTheory.Lp.coeFn_sub :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), μ.ae.EventuallyEq (↑↑(f - g)) (↑↑f - ↑↑g)
This theorem states that for any two members `f` and `g` of the `MeasureTheory.Lp` space over a measurable space `α` with measure `μ`, normed add commutative group `E`, and extended non-negative real number `p`, the difference of `f` and `g` under the norm operator is almost everywhere equal to the difference of `f` and `g` individually under the norm operator. In simpler terms, this means that the difference between the norms of `f` and `g` is the same no matter where you measure it, except for a set of measure zero.
More concisely: For measurable functions `f` and `g` in the `Lp` space over a measurable space `(α, μ)` with norm `∥.∥_p`, the almost everywhere equality `∥f - g∥_p = ∥f - g∥_p AlmostEverywhere` holds.
|
MeasureTheory.Memℒp.toLp.proof_2
theorem MeasureTheory.Memℒp.toLp.proof_2 :
∀ {α : Type u_2} {E : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] (f : α → E), MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable f μ
This theorem states that for any types `α` and `E`, a measurable space `m0` on `α`, an extended nonnegative real number `p`, a measure `μ` on `α`, and a `NormedAddCommGroup` instance on `E`, if a function `f` from `α` to `E` satisfies the `Memℒp` property with respect to `p` and `μ`, then `f` is almost everywhere strongly measurable with respect to `μ`.
In mathematical terms, this says that if `f` is a function from `α` to `E` such that it is almost everywhere strongly measurable and the norm of `f` raised to the power `p` has a finite integral (for `p < ∞`) or the essential supremum of `f` is finite (for `p = ∞`), then `f` is almost everywhere equivalent to the limit of a sequence of simple functions.
More concisely: If a function from a measurable space to a Normed Additive Commutative Group satisfies the `Memℒp` property with respect to a measure and a p-th power integrable or p-th power essential supremum finite extended real number, then it is almost everywhere equivalent to the limit of a sequence of simple functions.
|
BoundedContinuousFunction.Lp_nnnorm_le
theorem BoundedContinuousFunction.Lp_nnnorm_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
[inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α] [inst_2 : BorelSpace α]
[inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α E),
‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊
This theorem states that for any bounded continuous function 'f' from a measurable space 'α' to a normed add commutative group 'E', the `Lp`-norm of 'f' is at most a constant times its sup-norm. Here the constant depends on the measure of the whole space. More precisely, the `Lp`-norm is bounded above by the nonnegative real number equivalent of the measure of the whole space raised to the power of the reciprocal of 'p' (where 'p' is a number from the extended nonnegative real numbers) multiplied by the sup-norm of 'f'. The spaces involved have additional properties such as 'α' being a topological space with a Borel and second-countable topology, and the measure being a finite measure.
More concisely: For any bounded, measurable function $f:\alpha \rightarrow E$ from a Borel and second-countable measurable space $\alpha$ with a finite measure, and a normed add commutative group $E$, the $L^p$ norm of $f$ is less than or equal to the measure of $\alpha$'s total volume raised to the power of $1/p$ multiplied by the supremum norm of $f$.
|