MeasureTheory.condexp_indicator
theorem MeasureTheory.condexp_indicator :
∀ {α : Type u_1} {E : Type u_3} {m m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α},
MeasureTheory.Integrable f μ →
MeasurableSet s →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (s.indicator f)) (s.indicator (MeasureTheory.condexp m μ f))
The theorem `MeasureTheory.condexp_indicator` states that for every type `α` and `E`, measure spaces `m` and `m0`, a normed additive commutative group `E` that is also a normed space over the real numbers and a complete space, a measure `μ` on `α`, a function `f` from `α` to `E`, and a set `s` of `α`, if the function `f` is integrable with respect to `μ` and the set `s` is measurable, then the conditional expectation of the indicator function of `s` with respect to `f` over the sigma algebra `m` is almost everywhere equal to the indicator function of the set `s` with respect to the conditional expectation of `f` over the sigma algebra `m`.
In simple terms, this theorem tells you that under certain conditions (the function being integrable and the set being measurable), the conditional expectation of an indicator function over a set is the same as the indicator function of the conditional expectation, almost everywhere.
More concisely: For measurable sets `s` and integrable functions `f` from a measure space to a complete, real normed space, the almost everywhere equality holds between the indicator function of `s` conditioned on `f` and the indicator function of the set of `f`'s conditional expectation.
|
MeasureTheory.condexp_indicator_aux
theorem MeasureTheory.condexp_indicator_aux :
∀ {α : Type u_1} {E : Type u_3} {m m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α},
MeasurableSet s →
(μ.restrict sᶜ).ae.EventuallyEq f 0 →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (s.indicator f)) (s.indicator (MeasureTheory.condexp m μ f))
This theorem, referred to as `MeasureTheory.condexp_indicator_aux`, states that for any types `α` and `E`, measurable spaces `m` and `m0` on `α`, a normed additive commutative group structure on `E`, a real normed space structure on `E`, a complete space structure on `E`, a measure `μ` on `α`, a function `f` from `α` to `E`, and a set `s` of type `α`, if `s` is a measurable set and the function `f` is almost everywhere equal to `0` with respect to the measure restricted to the complement of `s`, then the conditional expectation of the indicator function of `s` with respect to `f` is almost everywhere equal to the indicator function of `s` with respect to the conditional expectation of `f`.
In mathematical terms, the theorem says that if we have a set `s` which is measurable, and a function `f` that is almost everywhere `0` outside of `s`, then the conditional expectation of the indicator function of `s` times `f` is almost everywhere equal to the indicator function of `s` times the conditional expectation of `f`. This theorem is an auxiliary lemma used in the proof of the `condexp_indicator` theorem in the Measure Theory.
More concisely: If `s` is a measurable set and `f` is a measurable function almost everywhere equal to zero outside of `s` in a measurable space `(α, m)` with respect to a measure `μ`, then the conditional expectation of the indicator function of `s` with respect to `f` is almost everywhere equal to the indicator function of `s` times the conditional expectation of `f`.
|
MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on
theorem MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on :
∀ {α : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
{f : α → E} {s : Set α} {m m₂ m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m0)
[inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] [inst_4 : MeasureTheory.SigmaFinite (μ.trim hm₂)],
MeasurableSet s →
(∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)) →
(μ.restrict s).ae.EventuallyEq (MeasureTheory.condexp m μ f) (MeasureTheory.condexp m₂ μ f)
This theorem states that given measurable spaces `m`, `m₂` and `m0`, a normed additively commutative group `E`, a normed space `E` over the reals, a complete normed space `E`, a function `f` mapping `α` to `E`, a set `s` of type `α`, and a measure `μ` on `α`, if `m` and `m₂` are both sub-σ-algebras of `m0` and `μ` is σ-finite with respect to both `m` and `m₂`, then if `s` is a measurable set, and the restriction to `s` of `m` is the same as the restriction to `s` of `m₂` for all measurable sets `t` [(ie. the measurability of `s` intersect `t` is the same for both `m` and `m₂`)], then the conditional expectation of `f` with respect to `m` and `μ` is equal almost everywhere to the conditional expectation of `f` with respect to `m₂` and `μ` when restricted to `s`.
More concisely: Given measurable spaces `m`, `m₂`, a normed additively commutative group `E`, a complete normed space `E` over the reals, a function `f` mapping from a measurable set `α` to `E`, a measure `μ` on `α` that is σ-finite with respect to both `m` and `m₂`, if `s` is a measurable set such that the restriction of `m` and `m₂` to `s` agree on measurable sets and `m`, `m₂` are sub-σ-algebras of `m0`, then the conditional expectations of `f` with respect to `m` and `μ` and `m₂` and `μ` are equal almost everywhere on `s`.
|