Regular conditional probability distribution #
We define the regular conditional probability distribution of Y : α → Ω given X : α → β, where
Ω is a standard Borel space. This is a kernel β Ω such that for almost all a, condDistrib
evaluated at X a and a measurable set s is equal to the conditional expectation
μ⟦Y ⁻¹' s | mβ.comap X⟧ evaluated at a.
μ⟦Y ⁻¹' s | mβ.comap X⟧ maps a measurable set s to a function α → ℝ≥0∞, and for all s that
map is unique up to a μ-null set. For all a, the map from sets to ℝ≥0∞ that we obtain that way
verifies some of the properties of a measure, but in general the fact that the μ-null set depends
on s can prevent us from finding versions of the conditional expectation that combine into a true
measure. The standard Borel space assumption on Ω allows us to do so.
The case Y = X = id is developed in more detail in Probability/Kernel/Condexp.lean: here X is
understood as a map from Ω with a sub-σ-algebra m to Ω with its default σ-algebra and the
conditional distribution defines a kernel associated with the conditional expectation with respect
to m.
Main definitions #
condDistrib Y X μ: regular conditional probability distribution ofY : α → ΩgivenX : α → β, whereΩis a standard Borel space.
Main statements #
condDistrib_ae_eq_condexp: for almost alla,condDistribevaluated atX aand a measurable setsis equal to the conditional expectationμ⟦Y ⁻¹' s | mβ.comap X⟧ a.condexp_prod_ae_eq_integral_condDistrib: the conditional expectationμ[(fun a => f (X a, Y a)) | X; mβ]is almost everywhere equal to the integral∫ y, f (X a, y) ∂(condDistrib Y X μ (X a)).
@[irreducible]
noncomputable def
ProbabilityTheory.condDistrib
{α : Type u_5}
{β : Type u_6}
{Ω : Type u_7}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
:
{x : MeasurableSpace α} →
[inst : MeasurableSpace β] →
(α → Ω) →
(α → β) →
(μ : MeasureTheory.Measure α) →
[inst_1 : MeasureTheory.IsFiniteMeasure μ] → { x // x ∈ ProbabilityTheory.kernel β Ω }
Regular conditional probability distribution: kernel associated with the conditional
expectation of Y given X.
For almost all a, condDistrib Y X μ evaluated at X a and a measurable set s is equal to
the conditional expectation μ⟦Y ⁻¹' s | mβ.comap X⟧ a. It also satisfies the equality
μ[(fun a => f (X a, Y a)) | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂(condDistrib Y X μ (X a))
for all integrable functions f.
Instances For
theorem
ProbabilityTheory.condDistrib_def
{α : Type u_5}
{β : Type u_6}
{Ω : Type u_7}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
:
∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] (Y : α → Ω) (X : α → β) (μ : MeasureTheory.Measure α)
[inst_1 : MeasureTheory.IsFiniteMeasure μ],
ProbabilityTheory.condDistrib Y X μ = MeasureTheory.Measure.condKernel (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ)
instance
ProbabilityTheory.instIsMarkovKernelCondDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
[MeasurableSpace β]
:
theorem
ProbabilityTheory.measurable_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hs : MeasurableSet s)
:
Measurable fun a => ↑↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) s
theorem
MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ))
:
((∀ᵐ (a : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable fun ω => f (a, ω)) ∧ MeasureTheory.Integrable fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂↑(ProbabilityTheory.condDistrib Y X μ) a) ↔ MeasureTheory.Integrable f
theorem
MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ))
:
MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) x)
(MeasureTheory.Measure.map X μ)
theorem
MeasureTheory.AEStronglyMeasurable.integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ))
:
MeasureTheory.AEStronglyMeasurable (fun a => ∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.aestronglyMeasurable'_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ))
:
MeasureTheory.AEStronglyMeasurable' (MeasurableSpace.comap X mβ)
(fun a => ∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.integrable_toReal_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : AEMeasurable X)
(hs : MeasurableSet s)
:
MeasureTheory.Integrable fun a => ENNReal.toReal (↑↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) s)
theorem
MeasureTheory.Integrable.condDistrib_ae_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ, MeasureTheory.Integrable fun ω => f (b, ω)
theorem
MeasureTheory.Integrable.condDistrib_ae
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable fun ω => f (X a, ω)
theorem
MeasureTheory.Integrable.integral_norm_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂↑(ProbabilityTheory.condDistrib Y X μ) x
theorem
MeasureTheory.Integrable.integral_norm_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun a => ∫ (y : Ω), ‖f (X a, y)‖ ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
theorem
MeasureTheory.Integrable.norm_integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun x => ‖∫ (y : Ω), f (x, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) x‖
theorem
MeasureTheory.Integrable.norm_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun a => ‖∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)‖
theorem
MeasureTheory.Integrable.integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun x => ∫ (y : Ω), f (x, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) x
theorem
MeasureTheory.Integrable.integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : AEMeasurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun a => ∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
theorem
ProbabilityTheory.set_lintegral_preimage_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
{t : Set β}
(hX : Measurable X)
(hY : AEMeasurable Y)
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
theorem
ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : Measurable X)
(hY : AEMeasurable Y)
(hs : MeasurableSet s)
{t : Set α}
(ht : MeasurableSet t)
:
∫⁻ (a : α) in t, ↑↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) s ∂μ = ↑↑μ (t ∩ Y ⁻¹' s)
theorem
ProbabilityTheory.condDistrib_ae_eq_condexp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hs : MeasurableSet s)
:
(fun a => ENNReal.toReal (↑↑(↑(ProbabilityTheory.condDistrib Y X μ) (X a)) s)) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ (Set.indicator (Y ⁻¹' s) fun ω => 1)
For almost every a : α, the condDistrib Y X μ kernel applied to X a and a measurable set
s is equal to the conditional expectation of the indicator of Y ⁻¹' s.
theorem
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib'
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
(hf_int : MeasureTheory.Integrable f)
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a =>
∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
The conditional expectation of a function f of the product (X, Y) is almost everywhere equal
to the integral of y ↦ f(X, y) against the condDistrib kernel.
theorem
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ))
(hf_int : MeasureTheory.Integrable fun a => f (X a, Y a))
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a =>
∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
The conditional expectation of a function f of the product (X, Y) is almost everywhere equal
to the integral of y ↦ f(X, y) against the condDistrib kernel.
theorem
ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable fun a => f (X a, Y a))
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (X a, Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a =>
∫ (y : Ω), f (X a, y) ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
The conditional expectation of a function f of the product (X, Y) is almost everywhere equal
to the integral of y ↦ f(X, y) against the condDistrib kernel.
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
[NormedSpace ℝ F]
[CompleteSpace F]
(hX : Measurable X)
(hY : AEMeasurable Y)
{f : Ω → F}
(hf : MeasureTheory.StronglyMeasurable f)
(hf_int : MeasureTheory.Integrable fun a => f (Y a))
:
(MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ fun a => f (Y a)) =ᶠ[MeasureTheory.Measure.ae μ] fun a =>
∫ (y : Ω), f y ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
[NormedAddCommGroup Ω]
[NormedSpace ℝ Ω]
[CompleteSpace Ω]
[MeasurableSpace Ω]
[BorelSpace Ω]
[TopologicalSpace.SecondCountableTopology Ω]
{Y : α → Ω}
(hX : Measurable X)
(hY_int : MeasureTheory.Integrable Y)
:
MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ Y =ᶠ[MeasureTheory.Measure.ae μ] fun a =>
∫ (y : Ω), y ∂↑(ProbabilityTheory.condDistrib Y X μ) (X a)
The conditional expectation of Y given X is almost everywhere equal to the integral
∫ y, y ∂(condDistrib Y X μ (X a)).
theorem
MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk
{β : Type u_2}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : MeasureTheory.Measure Ω}
[TopologicalSpace F]
{f : Ω → F}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.AEStronglyMeasurable (fun x => f x.snd) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ)
theorem
MeasureTheory.Integrable.comp_snd_map_prod_mk
{β : Type u_2}
{F : Type u_4}
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : MeasureTheory.Measure Ω}
{f : Ω → F}
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.Integrable fun x => f x.snd
theorem
ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff
{β : Type u_2}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
:
∀ {x : MeasurableSpace Ω} [inst : TopologicalSpace F] {X : Ω → β} {μ : MeasureTheory.Measure Ω},
Measurable X →
∀ {f : Ω → F},
MeasureTheory.AEStronglyMeasurable (fun x => f x.snd) (MeasureTheory.Measure.map (fun ω => (X ω, ω)) μ) ↔ MeasureTheory.AEStronglyMeasurable f μ
theorem
ProbabilityTheory.integrable_comp_snd_map_prod_mk_iff
{β : Type u_2}
{F : Type u_4}
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
{Ω : Type u_5}
:
∀ {x : MeasurableSpace Ω} {X : Ω → β} {μ : MeasureTheory.Measure Ω},
Measurable X → ∀ {f : Ω → F}, (MeasureTheory.Integrable fun x => f x.snd) ↔ MeasureTheory.Integrable f
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib_id
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[TopologicalSpace Ω]
[MeasurableSpace Ω]
[PolishSpace Ω]
[BorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
[NormedSpace ℝ F]
[CompleteSpace F]
{X : Ω → β}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : Measurable X)
{f : Ω → F}
(hf_int : MeasureTheory.Integrable f)
:
MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ f =ᶠ[MeasureTheory.Measure.ae μ] fun a =>
∫ (y : Ω), f y ∂↑(ProbabilityTheory.condDistrib id X μ) (X a)