MeasureTheory.Integrable.uniformIntegrable_condexp
theorem MeasureTheory.Integrable.uniformIntegrable_condexp :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_2}
[inst : MeasureTheory.IsFiniteMeasure μ] {g : α → ℝ},
MeasureTheory.Integrable g μ →
∀ {ℱ : ι → MeasurableSpace α},
(∀ (i : ι), ℱ i ≤ m0) → MeasureTheory.UniformIntegrable (fun i => MeasureTheory.condexp (ℱ i) μ g) 1 μ
The theorem `MeasureTheory.Integrable.uniformIntegrable_condexp` states that given an integrable function `g`, the sequence of its conditional expectations with respect to a sequence of sub-σ-algebras is uniformly integrable. This means that for any `g` which is integrable, and for any sequence of sub-σ-algebras `ℱ` (each one is a subset of `m0`), the family of functions obtained by taking the conditional expectation of `g` with respect to each sub-σ-algebra in `ℱ` is uniformly integrable.
More concisely: Given an integrable function `g` and a sequence of sub-σ-algebras `ℱ`, the family of functions obtained by taking the conditional expectation of `g` with respect to each sub-σ-algebra in `ℱ` is uniformly integrable.
|
MeasureTheory.condexp_stronglyMeasurable_mul
theorem MeasureTheory.condexp_stronglyMeasurable_mul :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
MeasureTheory.StronglyMeasurable f →
MeasureTheory.Integrable (f * g) μ →
MeasureTheory.Integrable g μ →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (f * g)) (f * MeasureTheory.condexp m μ g)
The theorem `MeasureTheory.condexp_stronglyMeasurable_mul` states that, given two real-valued functions `f` and `g` on some measure space, if `f` is `StronglyMeasurable` (meaning it can be approximated by a sequence of simple functions) and both `f*g` and `g` are `Integrable` (meaning they are measurable and their norms have finite integrals), then almost everywhere the conditional expectation of `f*g` equals the product of `f` and the conditional expectation of `g`. In simpler terms, under these conditions, we can "pull out" `f` from the conditional expectation of the product `f*g`.
More concisely: If `f` is Strongly Measurable and both `f*g` and `g` are Integrable, then almost everywhere, `E[f*g] = E[f] * E[g]` where `E` denotes the conditional expectation.
|
MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul
theorem MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
m ≤ m0 →
∀ (f : MeasureTheory.SimpleFunc α ℝ) {g : α → ℝ},
MeasureTheory.Integrable g μ →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (↑f * g)) (↑f * MeasureTheory.condexp m μ g)
The theorem `MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul` is an auxiliary lemma for `condexp_stronglyMeasurable_mul`. It states that for any measure space `α`, measurable spaces `m` and `m0`, measure `μ`, and a simple function `f` from `α` to `ℝ`, if `m` is a sub-σ-algebra of `m0` and a function `g` from `α` to `ℝ` is integrable with respect to `μ`, then almost everywhere with respect to `μ`, the conditional expectation of the product of `f` and `g` is equal to the product of `f` and the conditional expectation of `g`. Here, "almost everywhere" means except on a set of measure zero and "conditional expectation" is used in the measure-theoretic sense, specific to the measure theory in mathematics.
More concisely: For any measure space, measurable spaces, measure, and simple function, if a function is integrable and `m` is a sub-σ-algebra of `m0`, then almost everywhere, the conditional expectation of their product equals the product of their respective conditional expectations.
|
MeasureTheory.ae_bdd_condexp_of_ae_bdd
theorem MeasureTheory.ae_bdd_condexp_of_ae_bdd :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : NNReal} {f : α → ℝ},
(∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R) → ∀ᵐ (x : α) ∂μ, |MeasureTheory.condexp m μ f x| ≤ ↑R
The theorem `MeasureTheory.ae_bdd_condexp_of_ae_bdd` states that for any real-valued function `f` defined on a type `α`, under the measurable spaces `m` and `m0`, and a measure `μ`, if almost every value `x` in `α` satisfies that the absolute value of `f(x)` is less than or equal to a nonnegative real number `R`, then the same is true for the conditional expectation of `f`. In other words, if `f` is bounded almost everywhere by `R`, then its conditional expectation is also bounded almost everywhere by `R`.
More concisely: If a real-valued function `f` on a measurable space is almost everywhere bounded by `R`, then its conditional expectation is also almost everywhere bounded by `R`.
|
MeasureTheory.condexp_stronglyMeasurable_mul₀
theorem MeasureTheory.condexp_stronglyMeasurable_mul₀ :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ℝ},
MeasureTheory.AEStronglyMeasurable' m f μ →
MeasureTheory.Integrable (f * g) μ →
MeasureTheory.Integrable g μ →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (f * g)) (f * MeasureTheory.condexp m μ g)
This theorem, named "condexp_stronglyMeasurable_mul₀", states the pull-out property of conditional expectation in measure theory. Specifically, given two functions `f` and `g` mapping from a type `α` to real numbers, and considering measure spaces `m` and `m0` and a measure `μ`, if `f` is `μ`-almost everywhere equal to an `m`-strongly measurable function, and both the product of `f` and `g` and `g` itself are integrable with respect to `μ`, then the conditional expectation of the product of `f` and `g` is `μ`-almost everywhere equal to the product of `f` and the conditional expectation of `g`. In other words, if certain conditions are met, we can pull out `f` from the conditional expectation of the product of `f` and `g`.
More concisely: If `f` is almost everywhere equal to an strongly measurable function and both `fg` and `g` are integrable, then `E[f * g] = f * E[g]` almost everywhere.
|