MeasureTheory.Filtration.le
theorem MeasureTheory.Filtration.le :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m)
(i : ι), ↑f i ≤ m
This theorem states that for any type `Ω`, any type `ι` with a preorder, a measurable space `m` on `Ω`, and a filtration `f` on `m` indexed by `ι`, the measure theory defined by the filtration at any index `i` is less than or equal to `m`. In mathematical terms, if `f` represents a filtration of sigma algebras or measurable subsets of a set `Ω` indexed by a preordered set `ι`, then the sigma algebra at any index `i` is a sub sigma algebra of `m`.
More concisely: For any preordered type `ι`, type `Ω` with a measurable structure `m`, and filtration `f` on `m` indexed by `ι`, the sigma algebra in `f` at any index `i` is a sub-σ-algebra of `m`.
|
MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd
theorem MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {R : NNReal} {p : ENNReal} {F : Type u_5}
[inst : NormedAddCommGroup F] {ℱ : MeasureTheory.Filtration ℕ m} {f : ℕ → Ω → F},
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
(∀ (n : ℕ), MeasureTheory.snorm (f n) p μ ≤ ↑R) →
MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ
The theorem `MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd` states that, for a measure space `Ω` with measure `μ`, a nonnegative real number `R`, an extended nonnegative real number `p`, a normed additive commutative group `F` and a filtration `ℱ` of the measurable space, if we have a sequence of functions `f : ℕ → Ω → F` such that each function `f n` is almost everywhere strongly measurable with respect to measure `μ`, and the `ℒp` seminorm of each function `f n` measured with respect to `μ` is less than or equal to `R`, then the limit process of the sequence of functions `f` with respect to the filtration `ℱ` and measure `μ` is in `ℒp` space, i.e., it is almost everywhere strongly measurable and its `ℒp` seminorm is finite.
More concisely: Given a measure space `(Ω, μ)`, a normed additive commutative group `F`, a filtration `ℱ`, a real number `R`, and a sequence of almost everywhere strongly measurable functions `f : ℕ → Ω → F` with `ℒp` seminorms less than `R`, the limit process of `f` with respect to `ℱ` and `μ` is an almost everywhere strongly measurable function in `ℒp(Ω, μ, F)` with a finite `ℒp` seminorm.
|
MeasureTheory.Integrable.uniformIntegrable_condexp_filtration
theorem MeasureTheory.Integrable.uniformIntegrable_condexp_filtration :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {μ : MeasureTheory.Measure Ω}
[inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : MeasureTheory.Filtration ι m} {g : Ω → ℝ},
MeasureTheory.Integrable g μ → MeasureTheory.UniformIntegrable (fun i => MeasureTheory.condexp (↑f i) μ g) 1 μ
The theorem `MeasureTheory.Integrable.uniformIntegrable_condexp_filtration` states that for a given pre-ordered set `ι`, a measurable space `Ω`, a measure `μ` on `Ω` which is finite, a filtration `f` over the measurable space `Ω` indexed by `ι`, and an integrable function `g` mapping `Ω` to real numbers, if the function `g` is integrable with respect to the measure `μ`, then the conditional expectations of `g` with respect to the filtration `f` constitute a uniformly integrable family of functions. In other words, the family of functions obtained by taking the conditional expectation of `g` with respect to each element of the filtration `f` is such that all the functions in the family are almost everywhere strongly measurable, the family is uniformly integrable in the measure theory sense and there exists a constant `C` such that the seminorm of each function in the family is less than or equal to `C`.
More concisely: Given a finite measure `μ` on a measurable space `(Ω, Σ)`, a filtration `(F_i : i ∈ ι)` of sub-σ-algebras, and an integrable function `g : Ω → ℝ`, the family of conditional expectations `(��朱_i g) : i ∈ ι` is uniformly integrable.
|
MeasureTheory.Filtration.mono
theorem MeasureTheory.Filtration.mono :
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {i j : ι}
(f : MeasureTheory.Filtration ι m), i ≤ j → ↑f i ≤ ↑f j
The theorem `MeasureTheory.Filtration.mono` states that for any measurable space `Ω`, any type `ι` (with a preorder defined on it), and any filtration `f` of `m` indexed by `ι`, for any two indices `i` and `j` from `ι`, if `i` is less than or equal to `j` (i.e., `i ≤ j`), then the measure space at index `i` is a subset of the measure space at index `j` (i.e., `↑f i ≤ ↑f j`). In other words, this theorem is about the monotonocity of filtrations in measure theory, indicating that as we progress through the indexing set `ι` in non-decreasing order, the corresponding measure spaces do not decrease.
More concisely: For any measurable space and any filtration indexed by a preordered type, the measure space at a smaller index is included in the measure space at a larger index.
|