ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
theorem ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd :
∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
[inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β},
Measurable X →
Measurable Y →
∀ (κ : ↥(ProbabilityTheory.kernel β Ω)) [inst_4 : ProbabilityTheory.IsFiniteKernel κ],
MeasureTheory.Measure.map (fun x => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ →
∀ᵐ (x : β) ∂MeasureTheory.Measure.map X μ, κ x = (ProbabilityTheory.condDistrib Y X μ) x
This theorem, `condDistrib_ae_eq_of_measure_eq_compProd`, states that for all measurable spaces `α`, `β`, and `Ω`, where `Ω` is equipped with a `MeasurableSpace` and `StandardBorelSpace` structure and is nonempty, and for any `MeasurableSpace` on `α`, a measure `μ` on `α` that is finite, functions `X : α → β` and `Y : α → Ω`, and a `MeasurableSpace` on `β`, if `X` and `Y` are measurable functions, then for all kernels `κ` in the space of `ProbabilityTheory.kernel β Ω` that are finite, if the map of the measure `μ` under the function `(x => (X x, Y x))` equals the composition of `κ` with the map of the measure `μ` under `X`, then almost everywhere with respect to the measure given by mapping `μ` under `X`, `κ` equals the conditional distribution of `Y` given `X` under the measure `μ`.
More concisely: If `α`, `β`, and `Ω` are measurable spaces with `Ω` being nonempty and standard Borel, `μ` is a finite measure on `α`, `X : α → β` and `Y : α → Ω` are measurable functions, and `κ` is a finite kernel from `β` to `Ω`, then `κ` is the conditional distribution of `Y` given `X` under `μ` almost everywhere with respect to `μ` under `X` if and only if the pushforward measures of `μ` under `(x => (X x, Y x))` and the composition of `κ` with the pushforward measure of `μ` under `X` are equal.
|
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib'
theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib' :
∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω]
[inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω}
{mβ : MeasurableSpace β} {f : β × Ω → F} [inst_5 : NormedSpace ℝ F] [inst_6 : CompleteSpace F],
Measurable X →
AEMeasurable Y μ →
MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
μ.ae.EventuallyEq (MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) fun a =>
∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
The theorem `ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib'` states that, for a given function `f` of the product `(X, Y)`, the conditional expectation of `f` is almost everywhere equal to the integral of the function `y ↦ f(X, y)` with respect to the `condDistrib` kernel. This is under the conditions that `X` is measurable, `Y` is almost everywhere measurable with respect to measure `μ`, and `f` is integrable with respect to the pushforward measure of the function mapping `a` to `(X a, Y a)`. The "almost everywhere" equality is with respect to the measure space defined by `μ` and the condition is expressed in terms of the `condDistrib` of `Y` and `X` with respect to measure `μ`.
More concisely: For measurable functions `X` and almost everywhere measurable `Y` with respect to measure `μ`, and integrable `f` with respect to the pushforward measure of the map `a mapsto (X a, Y a)`, the almost everywhere equality holds between the conditional expectation of `f` given `Y` and the integral of `f(_, y)` with respect to the `condDistrib` kernel of `Y` with respect to `μ`.
|
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib
theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib :
∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω]
[inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω}
{mβ : MeasurableSpace β} {f : β × Ω → F} [inst_5 : NormedSpace ℝ F] [inst_6 : CompleteSpace F],
Measurable X →
AEMeasurable Y μ →
MeasureTheory.StronglyMeasurable f →
MeasureTheory.Integrable (fun a => f (X a, Y a)) μ →
μ.ae.EventuallyEq (MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) fun a =>
∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
The theorem `ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib` states that for a given function `f` of the product space `(X, Y)` where `X` is a measurable function from `α` to `β` and `Y` is an almost everywhere measurable function from `α` to `Ω`, the conditional expectation of `f` is almost everywhere equal to the integral of the function `y ↦ f(X, y)` against the `condDistrib` kernel. This is under the conditions that `f` is strongly measurable and integrable (meaning it is both almost everywhere strongly measurable and it has finite integral). The measurable spaces used are `mα` for `α`, `mβ` for `β`, and the measure theory employed is the finite measure `μ`.
More concisely: For strongly measurable and integrable functions `f` on the product space `(X, Y)` of measurable spaces `(α, mα)` and `(β, mβ)` with finite measure `μ`, the almost everywhere equality holds between the conditional expectation of `f` with respect to `Y` and the integral of `f(x, y)` with respect to the `condDistrib` kernel over `Y`.
|
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀
theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀ :
∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω]
[inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω}
{mβ : MeasurableSpace β} {f : β × Ω → F} [inst_5 : NormedSpace ℝ F] [inst_6 : CompleteSpace F],
Measurable X →
AEMeasurable Y μ →
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
MeasureTheory.Integrable (fun a => f (X a, Y a)) μ →
μ.ae.EventuallyEq (MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) fun a =>
∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
The theorem `ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀` states that for a function `f` of the product `(X, Y)` where `X` and `Y` are functions from a measure space `α`, given certain conditions, the conditional expectation of `f` is almost everywhere equal to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel.
The conditions are that `X` is measurable, `Y` is almost everywhere measurable with respect to a measure `μ`, `f` is strongly measurable almost everywhere with respect to the pushforward of `μ` under the mapping `(X , Y)`, and the function `(a => f(X a, Y a))` is integrable with respect to `μ`. The `condDistrib` kernel is a measure on the space `Ω` that relates to the conditional distribution of `Y` given `X`.
More concisely: Given measurable spaces `α`, a measure `μ` on `α`, functions `X:α→Ω` and `Y:α→ℝ` with `X` measurable, `Y` almost everywhere measurable, and a strongly measurable almost everywhere function `f:Ω→ℝ`, if `(a => f(X a, Y a))` is integrable with respect to `μ`, then `f` is almost everywhere equal to the integral of `y ↦ f(X, y)` with respect to the `condDistrib` kernel.
|
ProbabilityTheory.condDistrib_apply_of_ne_zero
theorem ProbabilityTheory.condDistrib_apply_of_ne_zero :
∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
[inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β}
[inst_4 : MeasurableSingletonClass β],
Measurable Y →
∀ (x : β),
↑↑(MeasureTheory.Measure.map X μ) {x} ≠ 0 →
∀ (s : Set Ω),
↑↑((ProbabilityTheory.condDistrib Y X μ) x) s =
(↑↑(MeasureTheory.Measure.map X μ) {x})⁻¹ *
↑↑(MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) ({x} ×ˢ s)
This theorem states that given any measurable function `Y` from `α` to `Ω`, if a singleton set `{x}` has a non-zero measure under the pushforward measure of a function `X` from `α` to `β`, then for any set `s` in `Ω`, the conditional distribution of `Y` given `X` at `x` and applied to `s` is equal to the inverse of the measure of `{x}` under the pushforward measure of `X` times the measure of the cartesian product of `{x}` and `s` under the pushforward measure of the function mapping `a` to the pair `(X a, Y a)`. Here, `α`, `β`, and `Ω` are types with `Ω` being a standard Borel space, `μ` is a finite measure on `α`, and `X` and `Y` are functions from `α` to `β` and `Ω`, respectively. The spaces `α` and `β` are equipped with measurable spaces `mα` and `mβ`, where `mβ` has the measurable singleton class property.
More concisely: Given a measurable function `Y` from a measurable space `α` to a standard Borel space `Ω`, a finite measure `μ` on `α`, and measurable functions `X: α → β`, if the singleton set `{x} ⊆ α` has non-zero measure under the pushforward measure of `X`, then the conditional distribution of `Y` given `X` at `x` is equal to the inverse of the measure of `{x}` under the pushforward measure of `X` times the measure of the cartesian product `{x} × s` under the pushforward measure of the function mapping `a` to `(X a, Y a)`, for any set `s ⊆ Ω`.
|
ProbabilityTheory.condDistrib_ae_eq_condexp
theorem ProbabilityTheory.condDistrib_ae_eq_condexp :
∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
[inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {s : Set Ω},
Measurable X →
Measurable Y →
MeasurableSet s →
μ.ae.EventuallyEq (fun a => (↑↑((ProbabilityTheory.condDistrib Y X μ) (X a)) s).toReal)
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ ((Y ⁻¹' s).indicator fun ω => 1))
This theorem states that for almost every `a` in the type `α`, the `condDistrib Y X μ` kernel (which describes the conditional distribution of `X` given `Y` with respect to measure `μ`) applied to `X a` and a measurable set `s` is equal to the conditional expectation of the indicator function of the preimage of `s` under `Y`. This holds under the conditions that `X` and `Y` are measurable functions, `s` is a measurable set, and the measure `μ` is finite. Essentially, this theorem connects the concepts of conditional distribution and conditional expectation in probability theory.
More concisely: For measurable functions X and Y, finite measure μ, and almost every a in α, the conditional distribution of X given Y applied to X(a) equals the conditional expectation of the indicator function of the preimage of a measurable set s under Y.
|
ProbabilityTheory.condexp_ae_eq_integral_condDistrib'
theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib' :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {mβ : MeasurableSpace β} {Ω : Type u_5}
[inst_1 : NormedAddCommGroup Ω] [inst_2 : NormedSpace ℝ Ω] [inst_3 : CompleteSpace Ω] [inst_4 : MeasurableSpace Ω]
[inst_5 : BorelSpace Ω] [inst_6 : SecondCountableTopology Ω] {Y : α → Ω},
Measurable X →
MeasureTheory.Integrable Y μ →
μ.ae.EventuallyEq (MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ Y) fun a =>
∫ (y : Ω), y ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
The theorem `ProbabilityTheory.condexp_ae_eq_integral_condDistrib'` states that for any measurable space `α`, measurable function `X: α → β`, measure `μ` on `α`, a normed add commutative group `Ω` with a complete space, a borel space, and a second countable topology, and another function `Y: α → Ω`, under the condition that `X` is measurable and `Y` is integrable with respect to `μ`, then almost everywhere with respect to `μ`, the conditional expectation of `Y` given the σ-algebra generated by `X` is equal to the integral of `y` with respect to the conditional distribution of `Y` given `X` at the point `X a`.
More concisely: For any measurable spaces α and β, measurable functions X: α → β and Y: α → Ω (a normed add commutative group with a complete space), a measure μ on α, and under the assumption that X is measurable, Y is integrable with respect to μ, almost everywhere with respect to μ, the conditional expectation of Y given the σ-algebra generated by X is equal to the integral of Y with respect to the conditional distribution of Y given X.
|