MeasureTheory.memℒp_trim_of_mem_lpMeasSubgroup
theorem MeasureTheory.memℒp_trim_of_mem_lpMeasSubgroup :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp F p μ))
(hf_meas : f ∈ MeasureTheory.lpMeasSubgroup F m p μ), MeasureTheory.Memℒp (Exists.choose ⋯) p (μ.trim hm)
This theorem states that, given a function `f` in the Lp space (`MeasureTheory.Lp F p μ`), which is an extended nonnegative real number (`ENNReal`) under a specific measure (`μ`) and belongs to the set of functions (`MeasureTheory.lpMeasSubgroup F m p μ`) that are almost everywhere equal to a measurable function, then this function (`f`) is almost everywhere strongly measurable and its seminorm is finite (`MeasureTheory.Memℒp`). This holds true for the measure (`μ`) trimmed by a measurable space `m`, which is less than or equal to another measurable space `m0` (`μ.trim hm`). Here, 'almost everywhere' means 'except on a set of measure zero'.
More concisely: Given a function `f` in the `Lp` space under measure `μ` that is almost everywhere equal to a measurable function and has finite seminorm, `f` is almost everywhere strongly measurable in the trimmed measure `μ.trim hm`.
|
MeasureTheory.lpMeas.ae_fin_strongly_measurable'
theorem MeasureTheory.lpMeas.ae_fin_strongly_measurable' :
∀ {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
(f : ↥(MeasureTheory.lpMeas F 𝕜 m p μ)),
p ≠ 0 → p ≠ ⊤ → ∃ g, MeasureTheory.FinStronglyMeasurable g (μ.trim hm) ∧ μ.ae.EventuallyEq (↑↑↑f) g
The theorem states that for any types `α`, `F`, and `𝕜`, and any extended nonnegative real number `p` that is neither 0 nor infinity, given a measure space `m` that is less than or equal to `m0`, a measure `μ`, and a function `f` in the space of measurable `Lp` functions, there exists a function `g` that is finitely strongly measurable with respect to the trimmed measure `μ.trim hm`, and almost everywhere equal to `f` under the measure `μ`. In simpler terms, this theorem is stating that under certain conditions, we can approximate `Lp` measurable functions by sequences of simple functions whose support has finite measure, except possibly on a set of measure zero.
More concisely: Given a measure space, a measure less than or equal to a given measure `m0`, an `Lp` measurable function `f`, and a non-zero, finite extended real number `p`, there exists a finitely strongly measurable function `g` that almost everywhere equals `f` under the trimmed measure.
|
MeasureTheory.lpMeasSubgroupToLpTrim_right_inv
theorem MeasureTheory.lpMeasSubgroupToLpTrim_right_inv :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (hm : m ≤ m0),
Function.RightInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm)
(MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
The theorem `MeasureTheory.lpMeasSubgroupToLpTrim_right_inv` states that for any type `α`, any normed add commutative group `F`, any extended nonnegative real number `p`, and any two measurable spaces `m` and `m0` such that `m` is a subspace of `m0`, and any measure `μ` on `α`, the function `MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm` is a right inverse of the function `MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm`. In other words, if you first apply `MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm` to an element and then apply `MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm` to the result, you end up with the original element. This relationship holds regardless of the specific elements of type `α`, `F`, `p`, `m`, `m0`, and `μ` that you started with.
More concisely: For any normed add commutative group `F`, measurable spaces `m` and `m0` with `m` a subspace of `m0`, measure `μ` on a type `α`, and extended nonnegative real number `p`, the functions `MeasureTheory.lpMeasSubgroupToLpTrim F p μ` and `MeasureTheory.lpTrimToLpMeasSubgroup F p μ` are right inverses of each other.
|
MeasureTheory.StronglyMeasurable.aeStronglyMeasurable'
theorem MeasureTheory.StronglyMeasurable.aeStronglyMeasurable' :
∀ {α : Type u_1} {β : Type u_2} {m x : MeasurableSpace α} [inst : TopologicalSpace β] {μ : MeasureTheory.Measure α}
{f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable' m f μ
The theorem `MeasureTheory.StronglyMeasurable.aeStronglyMeasurable'` states that for all types `α` and `β`, with `α` being a measurable space (denoted by `m` and `x`), `β` being a topological space, and a measure `μ` on `α`, if a function `f` from `α` to `β` is strongly measurable (i.e., it can be approximated by a sequence of simple functions), then `f` is almost everywhere (`μ`-almost everywhere) equal to a function that is `m`-strongly measurable (i.e., it is strongly measurable under the measurable space `m`). This implies that a strongly measurable function can be modified on a set of measure zero to obtain a function that is strongly measurable in a potentially different measurable space structure.
More concisely: If a strongly measurable function between a measurable space and a topological space can be approximated by simple functions, then it is almost everywhere equal to an `m`-strongly measurable function.
|
MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable'
theorem MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable' :
∀ {α : Type u_1} {F : Type u_3} {𝕜 : Type u_5} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
{f : ↥(MeasureTheory.Lp F p μ)},
f ∈ MeasureTheory.lpMeas F 𝕜 m p μ ↔ MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ
The theorem `MeasureTheory.mem_lpMeas_iff_aeStronglyMeasurable'` states that for any type `α`, any normed additive commutative group `F`, any type `𝕜` that behaves like a real number (captured by the `RCLike 𝕜` typeclass), any extended nonnegative real number `p`, any two measurable spaces `m` and `m0` over `α`, any measure `μ` on `α`, and any function `f` in the `Lp` space over `F` with respect to `p` and `μ`, `f` belongs to the subspace of `Lp` measurable functions if and only if `f` is almost everywhere `m`-strongly measurable with respect to `μ`. In mathematical terms, a function is in the space `Lp` of `F` with respect to a measure `μ` if and only if it is almost everywhere strongly measurable.
More concisely: A function belongs to the space of `Lp` measurable functions with respect to a measure if and only if it is almost everywhere strongly measurable.
|
MeasureTheory.AEStronglyMeasurable'.stronglyMeasurable_mk
theorem MeasureTheory.AEStronglyMeasurable'.stronglyMeasurable_mk :
∀ {α : Type u_1} {β : Type u_2} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} (hfm : MeasureTheory.AEStronglyMeasurable' m f μ),
MeasureTheory.StronglyMeasurable (MeasureTheory.AEStronglyMeasurable'.mk f hfm)
This theorem states that for any given topological space `β` and measurable spaces `m` and `m0` of type `α`, together with a measure `μ` on `α`, if a function `f` from `α` to `β` is almost everywhere (`μ`-a.e.) equal to an `m`-strongly measurable function (i.e., `f` satisfies `MeasureTheory.AEStronglyMeasurable' m f μ`), then the function almost everywhere equal to `f` that is `m`-strongly measurable (i.e., the function obtained by `MeasureTheory.AEStronglyMeasurable'.mk f hfm`) is strongly measurable (i.e., it is the limit point of a sequence of simple functions).
More concisely: Given a topological space β, measurable spaces m and m0 of type α, and a measure μ on α, if a function f from α to β is almost everywhere equal to an m-strongly measurable function, then the almost everywhere equal, m-strongly measurable function is itself strongly measurable.
|
MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on
theorem MeasureTheory.AEStronglyMeasurable'.aeStronglyMeasurable'_of_measurableSpace_le_on :
∀ {α : Type u_1} {E : Type u_2} {m m₂ m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : TopologicalSpace E] [inst_1 : Zero E],
m ≤ m0 →
∀ {s : Set α} {f : α → E},
MeasurableSet s →
(∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) →
MeasureTheory.AEStronglyMeasurable' m f μ →
(μ.restrict sᶜ).ae.EventuallyEq f 0 → MeasureTheory.AEStronglyMeasurable' m₂ f μ
The theorem states that for every type `α` and `E` and for every measurable spaces `m`, `m0` and `m2` on `α` and a measure `μ` on `E`, if `m` is a sub-measurable space of `m0` and for a set `s` and a function `f` from `α` to `E`, `s` is measurable and the intersection of `s` with any set `t` is also measurable, and if `f` is `m`-almost everywhere strongly measurable according to the measure theory, and `f` is almost everywhere equal to 0 on the complement of `s` with respect to `μ`, then `f` is also `m2`-almost everywhere strongly measurable. In other words, if a function is almost everywhere strongly measurable in one σ-algebra and its behavior outside a specific measurable set is known, then it is also almost everywhere strongly measurable in a larger σ-algebra.
More concisely: If `α` is a type, `m`, `m0`, `m2` are measurable spaces on `α`, `μ` is a measure on a set `E`, `m` is a sub-measurable space of `m0`, `s` is a measurable set, `f` is an `m`-almost everywhere strongly measurable function from `α` to `E` almost everywhere equal to 0 on `s`'s complement with respect to `μ`, then `f` is `m2`-almost everywhere strongly measurable.
|
MeasureTheory.lpMeasSubgroupToLpTrim_left_inv
theorem MeasureTheory.lpMeasSubgroupToLpTrim_left_inv :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (hm : m ≤ m0),
Function.LeftInverse (MeasureTheory.lpTrimToLpMeasSubgroup F p μ hm)
(MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm)
The theorem `MeasureTheory.lpMeasSubgroupToLpTrim_left_inv` states that for any types `α` and `F`, extended nonnegative real number `p`, a normed add comm group instance `inst` for `F`, measurable spaces `m` and `m0`, and a measure `μ`, where `m` is less than or equal to `m0`, the function `lpTrimToLpMeasSubgroup` is a left inverse of the function `lpMeasSubgroupToLpTrim`. In other words, if we first transform a function using `lpMeasSubgroupToLpTrim` and then apply `lpTrimToLpMeasSubgroup` to the result, we get back the original function. This is expressed mathematically as: `lpTrimToLpMeasSubgroup ∘ lpMeasSubgroupToLpTrim = id`.
More concisely: The theorem `MeasureTheory.lpMeasSubgroupToLpTrim_left_inv` asserts that the composition of `lpMeasSubgroupToLpTrim` and `lpTrimToLpMeasSubgroup` equals the identity function for measurable functions between Lebesgue measurable spaces and normed additive commutative groups.
|
MeasureTheory.AEStronglyMeasurable'.ae_eq_mk
theorem MeasureTheory.AEStronglyMeasurable'.ae_eq_mk :
∀ {α : Type u_1} {β : Type u_2} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} (hfm : MeasureTheory.AEStronglyMeasurable' m f μ),
μ.ae.EventuallyEq f (MeasureTheory.AEStronglyMeasurable'.mk f hfm)
The theorem `MeasureTheory.AEStronglyMeasurable'.ae_eq_mk` states that for any given types `α` and `β`, measurable spaces `m` and `m0` on `α`, a measure `μ` on `α`, a topological space structure on `β`, and a function `f` from `α` to `β` which is almost everywhere `m`-strongly measurable (denoted by `MeasureTheory.AEStronglyMeasurable' m f μ`), the function `f` is almost everywhere equal to the function obtained by applying the constructor `MeasureTheory.AEStronglyMeasurable'.mk` to `f` and the proof of its almost-everywhere `m`-strong measurability. Here, "almost everywhere" is with respect to the measure `μ`, which means that the set of points where the two functions disagree has measure zero.
More concisely: For any measurable spaces `m` and `m0`, measure `μ` on a type `α`, topological space `β`, and almost everywhere `m`-strongly measurable function `f : α → β`, `f` is almost everywhere equal to `MeasureTheory.AEStronglyMeasurable'.mk f μ`.
|
MeasureTheory.Memℒp.induction_stronglyMeasurable
theorem MeasureTheory.Memℒp.induction_stronglyMeasurable :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F],
m ≤ m0 →
p ≠ ⊤ →
∀ (P : (α → F) → Prop),
(∀ (c : F) ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s < ⊤ → P (s.indicator fun x => c)) →
(∀ ⦃f g : α → F⦄,
Disjoint (Function.support f) (Function.support g) →
MeasureTheory.Memℒp f p μ →
MeasureTheory.Memℒp g p μ →
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → P f → P g → P (f + g)) →
IsClosed {f | P ↑↑↑f} →
(∀ ⦃f g : α → F⦄, μ.ae.EventuallyEq f g → MeasureTheory.Memℒp f p μ → P f → P g) →
∀ ⦃f : α → F⦄, MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable' m f μ → P f
This theorem states that in order to prove a property for an arbitrary `Memℒp` function which is almost-everywhere strongly measurable with respect to a sub-measure algebra `m` in a normed space, it is sufficient to demonstrate the following:
- The property holds for multiples of characteristic functions that are measurable with respect to `m`.
- The property is preserved under addition of two `Memℒp` functions with disjoint support, each of which are strongly measurable and satisfy the property.
- The set of functions in the `Lᵖ` space strongly measurable with respect to `m` for which the property holds is closed.
- The property is preserved under the almost-everywhere equal relation; that is, if a function `f` almost-everywhere equals function `g`, and `f` has the property, then `g` will also have the property.
Here `Memℒp` is a property of a function, indicating that it is almost-everywhere strongly measurable, and its norm to the power `p` integrated with respect to the measure `μ` is finite. A characteristic function is a function that equals one on a specific set and zero otherwise; its multiple by `c` equals `c` on the set and zero otherwise. A function is said to be strongly measurable if it is the limit of a sequence of simple functions. Two elements or sets are said to be disjoint if their intersection is empty. A set is closed if it contains all its limit points.
More concisely: A property holds for any almost-everywhere strongly measurable `Memℒp` function with respect to a sub-measure algebra `m`, if it holds for multiples of measurable characteristic functions, is closable, preserved under addition of disjoint functions with the property, and is preserved under almost-everywhere equality.
|
MeasureTheory.AEStronglyMeasurable'.congr
theorem MeasureTheory.AEStronglyMeasurable'.congr :
∀ {α : Type u_1} {β : Type u_2} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f g : α → β},
MeasureTheory.AEStronglyMeasurable' m f μ → μ.ae.EventuallyEq f g → MeasureTheory.AEStronglyMeasurable' m g μ
The theorem `MeasureTheory.AEStronglyMeasurable'.congr` states that for any two functions `f` and `g` from a set `α` to a topological space `β`, with `α` equipped with two measurable spaces `m` and `m0` and a measure `μ`, if `f` is `μ`-almost everywhere equal to an `m`-strongly measurable function, and `f` is `μ`-almost everywhere equal to `g`, then `g` is also `μ`-almost everywhere equal to an `m`-strongly measurable function. Here, `μ`-almost everywhere equal means that the set where the two functions disagree has measure zero.
More concisely: If `f` is almost everywhere equal to an `m`-strongly measurable function and almost everywhere equal to `g`, then `g` is almost everywhere equal to an `m`-strongly measurable function. (Assuming `α` is a measurable space with respect to measures `m` and `m0`, and `β` is a topological space.)
|
MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim
theorem MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp F p (μ.trim hm))),
MeasureTheory.Memℒp.toLp ↑↑f ⋯ ∈ MeasureTheory.lpMeasSubgroup F m p μ
The theorem `MeasureTheory.mem_lpMeasSubgroup_toLp_of_trim` states that for any types `α` and `F`, a nonnegative extended real number `p`, an instance of `NormedAddCommGroup F`, measurable spaces `m` and `m0`, and a measure `μ` on `α`, if `m` is a subset of `m0` and `f` is an element of the `Lp` space corresponding to the trimmed measure `μ.trim hm`, then the function `f` also belongs to the subgroup `MeasureTheory.lpMeasSubgroup F m p μ` when converted to an `Lp` function using `MeasureTheory.Memℒp.toLp`. In other words, if a function is in the `Lp` space for a specific trimmed measure, it is also in the `Lp` space for the original measure.
More concisely: For any measurable spaces m and m0, measure μ, nonnegative extended real number p, and Normed Additive Commutative Group F, if m is a subset of m0 and f is an element of the Lp space of the trimmed measure μ.trim hm, then f is an element of the subgroup MeasureTheory.lpMeasSubgroup F m p μ when converted to an Lp function.
|
MeasureTheory.Lp.induction_stronglyMeasurable
theorem MeasureTheory.Lp.induction_stronglyMeasurable :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F] (hm : m ≤ m0),
p ≠ ⊤ →
∀ (P : ↥(MeasureTheory.Lp F p μ) → Prop),
(∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤),
P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)) →
(∀ ⦃f g : α → F⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ),
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g →
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 F p μ)), MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ → P f
This theorem, `MeasureTheory.Lp.induction_stronglyMeasurable`, provides a method to prove properties about $L^p$ functions that are almost everywhere strongly measurable with respect to a sub-sigma-algebra $m$ in a normed space. The theorem states that in order to prove a property $P$ for all such functions, it suffices to show three things:
1. The property holds for multiples of characteristic functions which are measurable with respect to $m$.
2. The property is preserved under addition, i.e., if the property holds for two functions $f$ and $g$ which are disjoint in their support (i.e., they do not both have non-zero values at the same points), then it also holds for their sum.
3. The set of $L^p$ functions that are strongly measurable with respect to $m$ and satisfy the property is closed.
The theorem assumes that the power $p$ in the $L^p$ space is less than infinity and that the ambient measurable space is greater or equal to $m$.
More concisely: If a property holds for all $L^p$ functions that are strongly measurable with respect to a sub-sigma-algebra $m$ in a normed space, it holds for multiples of characteristic functions measurable with respect to $m$, is closed under addition of disjoint functions, and the set of such functions is closed, then the property holds for all $L^p$ functions in the ambient measurable space.
|
MeasureTheory.Lp.induction_stronglyMeasurable_aux
theorem MeasureTheory.Lp.induction_stronglyMeasurable_aux :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_1 : Fact (1 ≤ p)] [inst_2 : NormedSpace ℝ F] (hm : m ≤ m0),
p ≠ ⊤ →
∀ (P : ↥(MeasureTheory.Lp F p μ) → Prop),
(∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : ↑↑μ s < ⊤),
P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p ⋯ ⋯ c)) →
(∀ ⦃f g : α → F⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ),
MeasureTheory.AEStronglyMeasurable' m f μ →
MeasureTheory.AEStronglyMeasurable' m g μ →
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 F p μ)), MeasureTheory.AEStronglyMeasurable' m (↑↑f) μ → P f
This theorem, `MeasureTheory.Lp.induction_stronglyMeasurable_aux`, is an auxiliary lemma used in the proof of another theorem: `Lp.induction_stronglyMeasurable`.
In natural language, it states that for any non-top extended nonnegative real number `p`, any types `α` and `F`, any instances of normed additive commutative group `F`, normed space `ℝ F`, and two measurable spaces `m` and `m0` on `α` such that `m` is less than or equal to `m0`, and a measure `μ`, under the assumptions that `p` is greater than or equal to 1, and `p` is not equal to the top element, we can define a property `P` on the elements of the Lp space such that:
- `P` holds for all constants `c` and sets `s` that are measurable and have finite measure.
- If `f` and `g` are two functions from `α` to `F` that belong to Lp space (`MeasureTheory.Memℒp f p μ` and `MeasureTheory.Memℒp g p μ`), are almost everywhere strongly measurable with respect to measure `m` (i.e., `MeasureTheory.AEStronglyMeasurable' m f μ` and `MeasureTheory.AEStronglyMeasurable' m g μ`), and their supports are disjoint, then if `P` holds for `f` and `g`, it also holds for their sum.
- The set of all elements for which `P` holds is closed.
Then for any function `f` in the Lp space that is almost everywhere strongly measurable with respect to measure `m`, `P` holds for `f`. This theorem provides a powerful tool for proving properties about functions in the Lp space using an induction-like process.
More concisely: Given a non-top extended nonnegative real number `p` greater than 1, measurable spaces `m` and `m0` on type `α` with `m ≤ m0`, normed space `ℝ F`, instances of normed additive commutative group `F`, measure `μ`, and a property `P` that holds for constants and measurable sets with finite measure and is closed and satisfies the sum property for almost everywhere strongly measurable functions in the Lp space with disjoint supports, then `P` holds for every almost everywhere strongly measurable function in the Lp space.
|
MeasureTheory.lpMeasSubgroupToLpTrim_norm_map
theorem MeasureTheory.lpMeasSubgroupToLpTrim_norm_map :
∀ {α : Type u_1} {F : Type u_3} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [hp : Fact (1 ≤ p)] (hm : m ≤ m0) (f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)),
‖MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖
This theorem, `MeasureTheory.lpMeasSubgroupToLpTrim_norm_map`, states that for any measure space `α`, any type `F` that forms a normed additively commutative group, any extended nonnegative real number `p` such that `p` is greater than or equal to 1, any two measurable spaces `m` and `m0` such that `m` is a sub-space of `m0`, any measure `μ` on `α`, and any element `f` from the `lpMeasSubgroup` associated with `F`, `m`, `p`, and `μ`, the norm of the image of `f` under the function `lpMeasSubgroupToLpTrim` (which maps from `lpMeasSubgroup` to `Lp F p (μ.trim hm)`) is equal to the norm of `f` itself. In other words, the `lpMeasSubgroupToLpTrim` function preserves the norm of `f`.
More concisely: For any measure space `α`, normed additively commutative group `F`, measure `μ`, sub-measure `μ0`, measurable function `f` in the `lpMeasSubgroup` of `F` with respect to `μ` and `μ0`, the norm of `f` under `lpMeasSubgroupToLpTrim` is equal to the norm of `f` itself.
|