ProbabilityTheory.condexpKernel_def
theorem ProbabilityTheory.condexpKernel_def :
∀ {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω] [inst_1 : Nonempty Ω]
(μ : MeasureTheory.Measure Ω) [inst_2 : MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω),
ProbabilityTheory.condexpKernel μ m =
ProbabilityTheory.kernel.comap (ProbabilityTheory.condDistrib id id μ) id ⋯
This theorem defines the conditional expectation kernel in probability theory. For every type `Ω` with `MeasurableSpace` and `StandardBorelSpace`, given a measure `μ` on `Ω` which is a finite measure and a `MeasurableSpace m`, the conditional expectation kernel of `μ` and `m` is equal to the comap of the kernel of conditional distribution with identity function. The theorem is applicable under the assumption that the type `Ω` is nonempty.
More concisely: For any nonempty `Ω` with `MeasurableSpace` and `StandardBorelSpace`, the conditional expectation kernel of a finite measure `μ` on `Ω` and a `MeasurableSpace` `m` is equal to the composition of the kernel of the conditional distribution of `μ` and the identity function.
|
ProbabilityTheory.condexpKernel_apply_eq_condDistrib
theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
[inst_1 : Nonempty Ω] {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ] {ω : Ω},
(ProbabilityTheory.condexpKernel μ m) ω = (ProbabilityTheory.condDistrib id id μ) (id ω)
This theorem states that for any type `Ω` that is both a measurable and standard Borel space, and given a finite measure `μ` on this space, the conditional expectation kernel at any point `ω` in `Ω` is equal to the conditional distribution at that same point `ω`. The identity function is used as the measurable functions for both the kernel and distribution.
More concisely: For any measurable and standard Borel space `(Ω, Σ, μ)`, the conditional expectation kernel and conditional distribution coincide, both using the identity function as measurable maps: `E[f|Σ] = D(f|Σ)` for all `f: Ω → ℝ`.
|
ProbabilityTheory.condexp_ae_eq_integral_condexpKernel
theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel :
∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
[inst_1 : Nonempty Ω] {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ]
[inst_3 : NormedAddCommGroup F] {f : Ω → F} [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F],
m ≤ mΩ →
MeasureTheory.Integrable f μ →
μ.ae.EventuallyEq (MeasureTheory.condexp m μ f) fun ω =>
∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω
The theorem `ProbabilityTheory.condexp_ae_eq_integral_condexpKernel` states that for any measurable space `Ω` with a σ-algebra `m`, a standard Borel space, a finite measure `μ`, a normed add-commutative group `F`, a function `f : Ω → F`, and given that `m` is a sub-σ-algebra of the measurable space `mΩ` and `f` is integrable, the conditional expectation of `f` with respect to σ-algebra `m` is almost everywhere equal to the integral of `f` with respect to the conditional expectation kernel. In mathematical terms, this means that $\mu$-almost everywhere, the conditional expectation of `f` with respect to `m` is equal to $\int y, f(y) \, d(\text{condexpKernel}\, \mu\, m\, \omega)$.
More concisely: For any measurable space `(Ω, m)` with finite measure `μ`, a normed add-commutative group `F`, integrable function `f : Ω → F`, and sub-σ-algebra `m`, the conditional expectation of `f` with respect to `m` is almost everywhere equal to the integral of `f` with respect to the conditional expectation kernel with respect to `μ` and `m`. In symbols, $\mu$-almost everywhere, $\mathbb{E}[f\mid m](\omega) = \int y, f(y) \, d(\text{condexpKernel}\, \mu\, m\, \omega)$.
|
MeasureTheory.Integrable.comp_snd_map_prod_id
theorem MeasureTheory.Integrable.comp_snd_map_prod_id :
∀ {Ω : Type u_1} {F : Type u_2} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → F}
[inst : NormedAddCommGroup F],
m ≤ mΩ →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (fun x => f x.2) (MeasureTheory.Measure.map (fun ω => (id ω, id ω)) μ)
This theorem states that for any types `Ω` and `F`, measurable spaces `m` and `mΩ` on `Ω`, a measure `μ` on `Ω`, and a function `f : Ω → F`, under the condition that `m` is less than or equal to `mΩ` and `f` is integrable with respect to `μ`, then the function which maps each pair `x` to `f x.2` is integrable with respect to the pushforward of the measure `μ` under the function that maps each `ω` in `Ω` to the pair `(id ω, id ω)`. Here, `x.2` represents the second element of pair `x`, and `id ω` is just `ω` itself, meaning the mapping function just duplicates each element in `Ω` into a pair. This theorem characterizes a specific situation where the process of mapping measures preserves the property of integrability.
More concisely: If `μ` is a measure on `Ω`, `m` and `mΩ` are measurable spaces on `Ω`, `f : Ω → F` is integrable with respect to `μ` and `m(Ω) ≤ mΩ(Ω)`, then the function mapping each pair `(ω, ω)` to `f ω.2` is integrable with respect to the pushforward of `μ` under the diagonal mapping from `Ω` to `Ω × Ω`.
|