MeasureTheory.snorm_add_le'
theorem MeasureTheory.snorm_add_le' :
∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
{f g : α → E},
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ →
∀ (p : ENNReal),
MeasureTheory.snorm (f + g) p μ ≤
MeasureTheory.LpAddConst p * (MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ)
This theorem, `MeasureTheory.snorm_add_le'`, states that for any two functions `f` and `g` from a set `α` to a normed additive commutative group `E`, if both functions are almost everywhere strongly measurable with respect to a measure `μ`, then for any extended nonnegative real number `p`, the seminorm of the sum of the functions, `(f + g)`, is less than or equal to a constant times the sum of the seminorms of `f` and `g` individually.
Here, the constant is determined by `MeasureTheory.LpAddConst p`, which is `1` if `p` is greater than or equal to `1` or `p` equals `0`, and `2^(1/p - 1)` if `p` is between `0` and `1`. The seminorm, given by `MeasureTheory.snorm`, is `0` for `p=0`, `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞`, and the essential supremum of `‖f‖` with respect to `μ` for `p = ∞`.
More concisely: For almost everywhere strongly measurable functions `f` and `g` from a set `α` to a normed additive commutative group `E` with respect to a measure `μ`, the seminorm of their sum `(f + g)` is less than or equal to `MeasureTheory.LpAddConst p` times the sum of the seminorms of `f` and `g`, where `p` is an extended nonnegative real number and `MeasureTheory.LpAddConst p` is defined as `1` for `p ≥ 1` or `p = 0`, and `2^(1/p - 1)` for `0 < p < 1`.
|
MeasureTheory.Memℒp.add
theorem MeasureTheory.Memℒp.add :
∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] {p : ENNReal}
{μ : MeasureTheory.Measure α} {f g : α → E},
MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ → MeasureTheory.Memℒp (f + g) p μ
The theorem `MeasureTheory.Memℒp.add` states that, for any measure space `α`, any normed additive commutative group `E`, any extended nonnegative real number `p`, any measure `μ` on `α`, and any two functions `f` and `g` from `α` to `E`, if `f` and `g` both satisfy the Memℒp property with respect to `p` and `μ`, then the function `f + g` (the pointwise sum of `f` and `g`) also satisfies the Memℒp property with respect to `p` and `μ`.
In other words, the Memℒp property, which captures a certain kind of "integrability", is preserved under pointwise addition of functions.
More concisely: If functions $f$ and $g$ are integrable with respect to measure $\mu$ with exponent $p$ in the measure space $\alpha$ over the normed additive commutative group $E$, then their pointwise sum $f + g$ is also integrable with respect to $\mu$ with exponent $p$ in $E$.
|
Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality._auxLemma.2
theorem Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality._auxLemma.2 :
∀ {r q : NNReal}, (↑r ≤ ↑q) = (r ≤ q)
This theorem, named `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality._auxLemma.2`, asserts a comparison property between nonnegative real numbers, denoted as `NNReal`. Specifically, for any two nonnegative real numbers `r` and `q`, the inequality expressed in terms of their natural embeddings into real numbers (`↑r ≤ ↑q`) is equivalent to the direct inequality between `r` and `q` itself (`r ≤ q`). In other words, comparing `r` and `q` directly or comparing their real number counterparts yields the same result.
More concisely: For any nonnegative real numbers `r` and `q`, `↑r ≤ ↑q` if and only if `r ≤ q`.
|
MeasureTheory.exists_Lp_half
theorem MeasureTheory.exists_Lp_half :
∀ {α : Type u_1} (E : Type u_2) {m : MeasurableSpace α} [inst : NormedAddCommGroup E] (μ : MeasureTheory.Measure α)
(p : ENNReal) {δ : ENNReal},
δ ≠ 0 →
∃ η,
0 < η ∧
∀ (f g : α → E),
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ →
MeasureTheory.snorm f p μ ≤ η → MeasureTheory.snorm g p μ ≤ η → MeasureTheory.snorm (f + g) p μ < δ
This theorem, titled "MeasureTheory.exists_Lp_half", is a technical lemma used to control the addition of functions in the `L^p` space even when `p < 1`. Given `δ > 0`, the theorem asserts that there exists `η` such that two functions whose `L^p` seminorms are bounded by `η` will have their sum's `L^p` seminorm bounded by `δ`. Although `η = δ / 2` could be taken for `p ≥ 1`, the significance of this lemma is that it is also applicable for `p < 1`. The theorem is defined for a measurable space `α`, a normed add commutative group `E`, a measure `μ` on `α`, `p` as an extended nonnegative real number, and `δ` as another extended nonnegative real number. The functions under consideration are `f` and `g`, both of which are almost everywhere strongly measurable with respect to the measure `μ`.
More concisely: Given a measurable space, a normed add commutative group, a measure, and extended nonnegative real numbers `p`, `δ`, there exists `η` such that for almost everywhere strongly measurable functions `f` and `g` on the space, if `||f||_p` and `||g||_p` are both less than `η`, then `||f + g||_p` is less than `δ`.
|