MeasureTheory.condexp_sub
theorem MeasureTheory.condexp_sub :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → F'},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (f - g))
(MeasureTheory.condexp m μ f - MeasureTheory.condexp m μ g)
The theorem `MeasureTheory.condexp_sub` states that for any two functions `f` and `g` from a type `α` to a normed additively commutative group `F'`, equipped with a normed space structure and complete space structure, and given two measurable spaces `m` and `m0` and a measure `μ`, if `f` and `g` are both integrable with respect to `μ`, then the conditional expectation of the difference of `f` and `g` is almost everywhere equal to the difference of the conditional expectations of `f` and `g` with respect to the measure `μ`. This means, intuitively, that the operation of taking conditional expectations is linear: the expectation of a difference is the difference of the expectations.
More concisely: For measurable functions `f` and `g` from a measure space to a normed additively commutative group, if both are integrable, then their conditional expectations with respect to a measure `μ` differ almost everywhere by the difference of their unconditional expectations.
|
MeasureTheory.condexp_undef
theorem MeasureTheory.condexp_undef :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'},
¬MeasureTheory.Integrable f μ → MeasureTheory.condexp m μ f = 0
The theorem `MeasureTheory.condexp_undef` states that for any types `α` and `F'`, with `F'` being a normed additive commutative group, a normed space over the real numbers, and a complete space, and given measurable spaces `m` and `m0`, a measure `μ`, and a function `f` from `α` to `F'`, if `f` is not integrable with respect to the measure `μ`, then the conditional expectation of `f` (as defined by `MeasureTheory.condexp`) is zero. In other words, if the integral of the norm of `f` (with respect to `μ`) is not finite, then the conditional expectation of `f` is zero.
More concisely: If `μ` is a measure on the measurable spaces `(α, Σ)` and `(F', Σ')`, `F'` is a normed additive commutative group and a complete normed space over the real numbers, `f: α → F'` is measurable and not integrable with respect to `μ`, then `MeasureTheory.condexp f μ μ0 = 0`.
|
MeasureTheory.ae_eq_condexp_of_forall_set_integral_eq
theorem MeasureTheory.ae_eq_condexp_of_forall_set_integral_eq :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
[inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] {f g : α → F'},
MeasureTheory.Integrable f μ →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → MeasureTheory.IntegrableOn g s μ) →
(∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ) →
MeasureTheory.AEStronglyMeasurable' m g μ → μ.ae.EventuallyEq g (MeasureTheory.condexp m μ f)
This theorem states the **uniqueness of the conditional expectation**. Given a function `g` that is almost everywhere `m`-measurable, it says that if `g` satisfies an integrability condition and has the same integral as another function `f` on all `m`-measurable sets, then `g` is almost everywhere equal to the conditional expectation of `f` with respect to measure `μ` and sub-σ-algebra `m`. In other words, if two functions have the same integral on every measurable set, and they are both almost everywhere `m`-measurable and integrable, then they must be almost everywhere equal to each other. This theorem is crucial in the theory of conditional expectations in measure theory.
More concisely: Given two almost everywhere equal and integrable, almost everywhere `m`-measurable functions `f` and `g` with the same integral under a measure `μ` on an `m`-sigma algebra, `g` is the conditional expectation of `f` with respect to `μ` and `m`.
|
MeasureTheory.condexp_condexp_of_le
theorem MeasureTheory.condexp_condexp_of_le :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {f : α → F'} {m₁ m₂ m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
m₁ ≤ m₂ →
∀ (hm₂ : m₂ ≤ m0) [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm₂)],
μ.ae.EventuallyEq (MeasureTheory.condexp m₁ μ (MeasureTheory.condexp m₂ μ f))
(MeasureTheory.condexp m₁ μ f)
The theorem `MeasureTheory.condexp_condexp_of_le` states that for any types `α` and `F'` with `F'` a complete normed addition-commutative group with a `ℝ` normed space structure, and any function `f` from `α` to `F'`, given three measurable spaces `m₁`, `m₂`, and `m0`, and a measure `μ` on `α`, if `m₁` is a sub-σ-algebra of `m₂`, and `m₂` is also a sub-σ-algebra of `m0` such that `μ` is σ-finite with respect to the trimmed measure space `m₂`, the conditional expectation of the conditional expectation of `f` on `m₁` with respect to `μ` is almost everywhere (with respect to the measure `μ`) equal to the conditional expectation of `f` on `m₁` with respect to `μ`. This essentially says that we can "pull back" the conditional expectation through another conditional expectation under these conditions, and the result will still be equal almost everywhere to the original conditional expectation.
More concisely: For measurable spaces `m₁`, `m₂`, and `m0`, and a σ-finite measure `μ` on a complete normed additive-commutative group `F'`, if `m₁` is a sub-σ-algebra of both `m₂` and `m0`, and `f` is a function from a type `α` to `F'`, then the conditional expectation of the conditional expectation of `f` with respect to `μ` and `m₂` is almost everywhere equal to the conditional expectation of `f` with respect to `μ` and `m₁`.
|
MeasureTheory.condexp_of_sigmaFinite
theorem MeasureTheory.condexp_of_sigmaFinite :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm : m ≤ m0)
[hμm : MeasureTheory.SigmaFinite (μ.trim hm)],
MeasureTheory.condexp m μ f =
if MeasureTheory.Integrable f μ then
if MeasureTheory.StronglyMeasurable f then f
else MeasureTheory.AEStronglyMeasurable'.mk ↑↑(MeasureTheory.condexpL1 hm μ f) ⋯
else 0
The theorem `MeasureTheory.condexp_of_sigmaFinite` states that for any types `α` and `F'` with `α` being the type of outcomes and `F'` being a normed add commutative group that is also a normed space over the reals and complete space, given measurable spaces `m` and `m0`, a measure `μ` on `α`, and a function `f` from `α` to `F'`, if `m` is a sub σ-algebra of `m0` and `μ` is σ-finite with respect to `m`, then the conditional expectation of `f` with respect to `m` and `μ` is as follows:
If `f` is integrable with respect to `μ`, then if `f` is strongly measurable, the conditional expectation is `f` itself, otherwise it is a function that is `m`-strongly measurable and almost everywhere equal to `f`;
If `f` is not integrable, then the conditional expectation is `0`. Here, integrability of a function means that it is measurable and the integral of its norm is finite, and a function is strongly measurable if it is the limit of simple functions.
More concisely: Given measurable spaces `(α, Σα)`, `(α', Σα')`, a σ-finite measure `μ` on `(α, Σα)`, a normed add commutative group `F'` being a normed space over the reals and complete, and a function `f : α → F'`, if `μ` is σ-finite with respect to the sub-σ-algebra `m ⊆ Σα'` and `f` is integrable with respect to `μ`, then the conditional expectation of `f` with respect to `m` is `f` itself if `f` is strongly measurable, or a function equal to `f` almost everywhere; otherwise, it is `0`.
|
MeasureTheory.condexp_zero
theorem MeasureTheory.condexp_zero :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
MeasureTheory.condexp m μ 0 = 0
The theorem `MeasureTheory.condexp_zero` states that for any types `α` and `F'`, where `F'` is a normed additive commutative group and also a real normed space, and `α` is associated with two measurable spaces `m` and `m0` and a measure `μ`, the conditional expectation of the zero function (a function that maps every element of `α` to zero in `F'`) is always the zero function, regardless of the underlying measurable spaces and measure. In mathematical terms, this is saying that $E[0 | \mathcal{F}] = 0$, where $E$ denotes the expectation, 0 denotes the zero function and $\mathcal{F}$ denotes the σ-algebra.
More concisely: For any measurable spaces `m` and `m0` with measure `μ`, and any normed additive commutative group `F'` that is also a real normed space, the conditional expectation of the zero function from `α` to `F'` is the zero function.
|
MeasureTheory.stronglyMeasurable_condexp
theorem MeasureTheory.stronglyMeasurable_condexp :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'},
MeasureTheory.StronglyMeasurable (MeasureTheory.condexp m μ f)
The theorem `MeasureTheory.stronglyMeasurable_condexp` states that for any types `α` and `F'`, where `F'` forms a Normed Additive Commutative Group, a Normed Space over the real numbers ℝ, and is complete, and for any measurable spaces `m` and `m0` over `α`, any measure `μ` over `α`, and any function `f` from `α` to `F'`, the conditional expectation of `f` with respect to measure `μ` and measurable space `m` is strongly measurable. In mathematical terms, this means the conditional expectation of `f` is the limit of a sequence of simple functions.
More concisely: For any measurable spaces `(α, m)`, measure `μ` over `α`, complete Normed Additive Commutative Group `F'`, Normed Space over ℝ, and function `f : α → F'`, the conditional expectation of `f` with respect to `μ` is a strongly measurable function.
|
MeasureTheory.integrable_condexp
theorem MeasureTheory.integrable_condexp :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'},
MeasureTheory.Integrable (MeasureTheory.condexp m μ f) μ
The theorem `MeasureTheory.integrable_condexp` states that for any type `α` and any type `F'` that forms a normed additive commutative group and a normed space over the reals with complete space, for any measurable spaces `m` and `m0` over α, for any measure `μ` on `α`, and for any function `f` from `α` to `F'`, the conditional expectation of `f` (denoted as `MeasureTheory.condexp m μ f`) is integrable with respect to the measure `μ`. In other words, the conditional expectation of `f` is both measurable and has a finite integral.
More concisely: For any measurable space `(α, m)`, measure `μ`, normed additive commutative group and normed space `(F', ||·||)` over the reals with complete space, and measurable function `f: α → F'`, the conditional expectation `MeasureTheory.condexp m μ f` is an integrable function with respect to `μ`.
|
MeasureTheory.condexp_of_not_sigmaFinite
theorem MeasureTheory.condexp_of_not_sigmaFinite :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} (hm : m ≤ m0),
¬MeasureTheory.SigmaFinite (μ.trim hm) → MeasureTheory.condexp m μ f = 0
The theorem `MeasureTheory.condexp_of_not_sigmaFinite` states that for any types `α` and `F'`, if we have a normed add commutative group structure, normed real space structure, and complete space structure on `F'`, and given `m` and `m0` as measurable spaces on `α`, `μ` as a measure on `α`, and `f` as a function mapping from `α` to `F'`, if `m` is a sub-σ-algebra of `m0` (denoted by hm : m ≤ m0) and if `μ` trimmed by `m` is not σ-finite (denoted by ¬MeasureTheory.SigmaFinite (μ.trim hm)), then the conditional expectation of `f` with respect to `m` and `μ`, denoted by `MeasureTheory.condexp m μ f`, is equal to zero.
More concisely: If `m` is a sub-σ-algebra of `m0`, `μ` is a measure on `α`, `f` is a function from `α` to a normed add commutative group with a complete normed real space and complete space structure, and `μ.trim hm` is not σ-finite, then `MeasureTheory.condexp m μ f = 0`.
|
MeasureTheory.condexp_mono
theorem MeasureTheory.condexp_mono :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5}
[inst : NormedLatticeAddCommGroup E] [inst_1 : CompleteSpace E] [inst_2 : NormedSpace ℝ E]
[inst_3 : OrderedSMul ℝ E] {f g : α → E},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ →
μ.ae.EventuallyLE f g → μ.ae.EventuallyLE (MeasureTheory.condexp m μ f) (MeasureTheory.condexp m μ g)
The theorem `MeasureTheory.condexp_mono` states that for any types `α` and `E`, any measurable spaces `m` and `m0`, any measure `μ` on `α`, and any two functions `f` and `g` from `α` to `E` (where `E` is a complete normed lattice-additive commutative group and a normed space over the real numbers), if `f` and `g` are both integrable with respect to measure `μ` and `f` is almost everywhere less than or equal to `g` (with respect to the measure's almost everywhere filter), then the conditional expectation of `f` is almost everywhere less than or equal to the conditional expectation of `g` (again, with respect to the measure's almost everywhere filter).
More concisely: If `f` and `g` are integrable functions from a measurable space to a complete normed lattice-additive commutative group, with `f ≤ g` almost everywhere, then `E[f|m] ≤ E[g|m]` almost everywhere with respect to the measure's almost everywhere filter.
|
MeasureTheory.condexp_add
theorem MeasureTheory.condexp_add :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → F'},
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable g μ →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (f + g))
(MeasureTheory.condexp m μ f + MeasureTheory.condexp m μ g)
This theorem, `MeasureTheory.condexp_add`, states that, for any types `α` and `F'`, where `F'` is a normed additive commutative group, and `α` is a type with a specified measure, under the assumption that `F'` is a normed space over the field of real numbers and is also a complete space. If we have two measurable spaces `m` and `m0`, a measure `μ`, and two functions `f` and `g` mapping from `α` to `F'`, and both `f` and `g` are integrable with respect to `μ`, then the conditional expectation of the sum of `f` and `g` is almost everywhere equal to the sum of the conditional expectations of `f` and `g` with respect to the measure `μ`. Here, "almost everywhere" is with respect to the filter of co-null sets of `μ`. In other words, this theorem asserts the linearity of the conditional expectation in the setting of measure theory.
More concisely: Given measurable spaces `m`, `m0`, a complete normed additive commutative group `F'`, a measure `μ` on `α`, and integrable functions `f` and `g` from `α` to `F'`, the conditional expectations of `f + g` and `f + g` almost everywhere equal each other with respect to `μ`.
|
MeasureTheory.set_integral_condexp
theorem MeasureTheory.set_integral_condexp :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'} {s : Set α}
(hm : m ≤ m0) [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)],
MeasureTheory.Integrable f μ →
MeasurableSet s → ∫ (x : α) in s, MeasureTheory.condexp m μ f x ∂μ = ∫ (x : α) in s, f x ∂μ
The theorem `MeasureTheory.set_integral_condexp` states that given a set `s` of elements of a certain type `α`, a measure `μ`, a function `f` from `α` to a normed add commutative group `F'`, and a measurable space `m` that is a sub-space of `m0`, if `f` is integrable and `s` is a measurable set, then the integral of the conditional expectation `μ[f|hm]` over the `m`-measurable set `s` is the same as the integral of `f` over the set `s`. Here, `μ[f|hm]` denotes the conditional expectation of `f` with respect to the measure `μ` and the measurable space `m`. The sigma-finite measure condition ensures that the measure `μ` is finite when restricted to subsets of `α` that are in the sigma algebra generated by the measurable space `m`.
More concisely: Given a measure `μ`, a set `s` in the sigma-algebra of a measurable space `(α, Σ)`, a function `f` integrable with respect to `μ`, and a measurable sub-space `m` of `Σ`, the integral of the conditional expectation `μ[f|m]` over `s` equals the integral of `f` over `s`.
|
MeasureTheory.tendsto_condexpL1_of_dominated_convergence
theorem MeasureTheory.tendsto_condexpL1_of_dominated_convergence :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
[inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] {fs : ℕ → α → F'} {f : α → F'} (bound_fs : α → ℝ),
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ) →
MeasureTheory.Integrable bound_fs μ →
(∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) →
Filter.Tendsto (fun n => MeasureTheory.condexpL1 hm μ (fs n)) Filter.atTop
(nhds (MeasureTheory.condexpL1 hm μ f))
**Lebesgue Dominated Convergence Theorem**: This theorem provides the sufficient conditions for almost everywhere convergence of a sequence of functions to imply the convergence of their conditional expectations. Given a sequence of functions `{fs : ℕ → α → F'}` and a function `f`, if every function in the sequence is `AEStronglyMeasurable` (almost everywhere equal to the limit of a sequence of simple functions) and a function `bound_fs` is integrable (meaning that it is measurable and the integral over its norm is finite), and for almost all `x`, the norm of `fs n x` is less than or equal to `bound_fs x` and the sequence `fs n x` converges to `f x`, then the sequence of conditional expectations of the functions in the sequence converges to the conditional expectation of `f`.
More concisely: If a sequence of almost everywhere convergent, integrable, and dominated functions converges pointwise almost everywhere to a limit function, then their sequence of conditional expectations converges to the conditional expectation of the limit function.
|
MeasureTheory.condexp_of_stronglyMeasurable
theorem MeasureTheory.condexp_of_stronglyMeasurable :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0)
[hμm : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → F'},
MeasureTheory.StronglyMeasurable f → MeasureTheory.Integrable f μ → MeasureTheory.condexp m μ f = f
This theorem states that for any types `α` and `F'` with `F'` being a normed additive commutative group, a normed space over the field of real numbers, and a complete space, and given measurable spaces `m` and `m0` and a measure `μ` such that `m` is a sub-sigma-algebra of `m0`, and `μ` is sigma-finite with respect to the trimmed measure, for any function `f` from `α` to `F'`, if `f` is strongly measurable and integrable with respect to `μ`, then the conditional expectation of `f` with respect to `μ` and `m` is equal to `f` itself. In mathematical terms, if a function is both strongly measurable and has a finite integral, then its conditional expectation is the function itself.
More concisely: If `α` is a type, `F'` is a complete, normed additive commutative group over the real numbers, `m` is a sub-σ-algebra of a σ-finite measure space `(m0, μ)`, and `f: α → F'` is a strongly measurable and integrable function, then `μ-cond(f) = f`, where `μ-cond(f)` denotes the conditional expectation of `f` with respect to `m`.
|
MeasureTheory.tendsto_condexp_unique
theorem MeasureTheory.tendsto_condexp_unique :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (fs gs : ℕ → α → F')
(f g : α → F'),
(∀ (n : ℕ), MeasureTheory.Integrable (fs n) μ) →
(∀ (n : ℕ), MeasureTheory.Integrable (gs n) μ) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => gs n x) Filter.atTop (nhds (g x))) →
∀ (bound_fs : α → ℝ),
MeasureTheory.Integrable bound_fs μ →
∀ (bound_gs : α → ℝ),
MeasureTheory.Integrable bound_gs μ →
(∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x) →
(∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x) →
(∀ (n : ℕ),
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (fs n)) (MeasureTheory.condexp m μ (gs n))) →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ f) (MeasureTheory.condexp m μ g)
This theorem, `MeasureTheory.tendsto_condexp_unique`, states that if we have two sequences of functions (denoted `fs` and `gs`) such that for each step the conditional expectations of the corresponding functions are almost everywhere equal, and both sequences converge (the limit functions being `f` and `g` respectively), and the sequences also satisfy the conditions of the Dominated Convergence Theorem (each sequence is dominated by an integrable function `bound_fs` or `bound_gs`), then the conditional expectations of their limit functions `f` and `g` are almost everywhere equal.
In other words, if two sequences of functions are such that their conditional expectations are the same at each step, they converge, and they satisfy the requirements of the Dominated Convergence Theorem, then the conditional expectations of the limits of the sequences are the same almost everywhere.
More concisely: If two sequences of measurable functions with almost everywhere equal conditional expectations and integrable dominating functions converge almost everywhere, then their limit functions have almost everywhere equal conditional expectations.
|
MeasureTheory.condexp_neg
theorem MeasureTheory.condexp_neg :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → F'),
μ.ae.EventuallyEq (MeasureTheory.condexp m μ (-f)) (-MeasureTheory.condexp m μ f)
This theorem, `MeasureTheory.condexp_neg`, states that for any given type `α` and `F'` (where `F'` forms a complete normed space over the real numbers and also forms a normed additive commutative group), along with two measurable spaces `m` and `m0` over `α`, a measure `μ` over `α`, and a function `f` from `α` to `F'`, the conditional expectation of the negative of `f` is almost everywhere (with respect to the measure `μ`) equal to the negative of the conditional expectation of `f`. In mathematical terms, we have that $E[-f|\mathcal{F}] = -E[f|\mathcal{F}]$ almost everywhere.
More concisely: For measurable spaces `m` and `m0` over type `α`, a measure `μ` over `α`, a complete normed space `F'` over the real numbers, and a measurable function `f` from `α` to `F'`, the conditional expectations of the negatives of `f` and `f` are almost everywhere equal: $E[-f|\mathcal{F}] = -E[f|\mathcal{F}]$ almost everywhere.
|
MeasureTheory.condexp_of_not_le
theorem MeasureTheory.condexp_of_not_le :
∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F']
[inst_2 : CompleteSpace F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → F'},
¬m ≤ m0 → MeasureTheory.condexp m μ f = 0
This theorem is about the conditional expectation of a function in measure theory. It says that for any types `α` and `F'`, where `F'` is a normed addition commutative group, a real normed space, and a complete space, given two measurable spaces `m` and `m0` on `α`, a measure `μ` on `α`, and a function `f` from `α` to `F'`, if `m` is not a sub-σ-algebra of `m0`, then the conditional expectation of `f` with respect to the measure space `m` and measure `μ` is equal to 0. This is in line with the definition of the conditional expectation in Lean, which is defined to be 0 if `m` is not a sub-σ-algebra of `m0`.
More concisely: If `μ` is a measure on the measurable spaces `(α, m)` and `(α, m0)`, `f : α → F'` is a measurable function, and `m` is not a sub-σ-algebra of `m0`, then the conditional expectation of `f` with respect to `(α, m, μ)` is equal to the zero function.
|