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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(Y : α → Ω)
(X : α → β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
:
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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(Y : α → Ω)
(X : α → β)
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
:
ProbabilityTheory.condDistrib Y X μ = (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).condKernel
instance
ProbabilityTheory.instIsMarkovKernelCondDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
[MeasurableSpace β]
:
Equations
- ⋯ = ⋯
theorem
ProbabilityTheory.condDistrib_apply_of_ne_zero
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
[MeasurableSingletonClass β]
(hY : Measurable Y)
(x : β)
(hX : (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)
If the singleton {x} has non-zero mass for μ.map X, then for all s : Set Ω,
condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s) .
theorem
ProbabilityTheory.measurable_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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, ω)) ((ProbabilityTheory.condDistrib Y X μ) a)) ∧ MeasureTheory.Integrable (fun (a : β) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(ProbabilityTheory.condDistrib Y X μ) a)
(MeasureTheory.Measure.map X μ) ↔ MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ)
theorem
MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ 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.condDistrib_ae_eq_of_measure_eq_compProd
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
(hX : Measurable X)
(hY : Measurable Y)
(κ : ProbabilityTheory.Kernel β Ω)
[ProbabilityTheory.IsFiniteKernel κ]
(hκ : 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
condDistrib is a.e. uniquely defined as the kernel satisfying the defining property of
condKernel.
theorem
ProbabilityTheory.integrable_toReal_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : AEMeasurable X μ)
(hs : MeasurableSet s)
:
MeasureTheory.Integrable (fun (a : α) => (((ProbabilityTheory.condDistrib Y X μ) (X a)) s).toReal) μ
theorem
MeasureTheory.Integrable.condDistrib_ae_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y μ)
(hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
∀ᵐ (b : β) ∂MeasureTheory.Measure.map X μ,
MeasureTheory.Integrable (fun (ω : Ω) => f (b, ω)) ((ProbabilityTheory.condDistrib Y X μ) b)
theorem
MeasureTheory.Integrable.condDistrib_ae
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun (ω : Ω) => f (X a, ω)) ((ProbabilityTheory.condDistrib Y X μ) (X a))
theorem
MeasureTheory.Integrable.integral_norm_condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y μ)
(hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.Integrable (fun (x : β) => ∫ (y : Ω), ‖f (x, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) x)
(MeasureTheory.Measure.map X μ)
theorem
MeasureTheory.Integrable.integral_norm_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hY : AEMeasurable Y μ)
(hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.Integrable (fun (x : β) => ‖∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x‖)
(MeasureTheory.Measure.map X μ)
theorem
MeasureTheory.Integrable.norm_integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hY : AEMeasurable Y μ)
(hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.Integrable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x)
(MeasureTheory.Measure.map X μ)
theorem
MeasureTheory.Integrable.integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf_int : MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
MeasureTheory.Integrable (fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.setLIntegral_preimage_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)
:
@[deprecated ProbabilityTheory.setLIntegral_preimage_condDistrib]
theorem
ProbabilityTheory.set_lintegral_preimage_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)
:
Alias of ProbabilityTheory.setLIntegral_preimage_condDistrib.
theorem
ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)
@[deprecated ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet]
theorem
ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)
Alias of ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet.
theorem
ProbabilityTheory.condDistrib_ae_eq_condexp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{s : Set Ω}
(hX : Measurable X)
(hY : Measurable Y)
(hs : MeasurableSet s)
:
(fun (a : α) => (((ProbabilityTheory.condDistrib Y X μ) (X a)) s).toReal) =ᵐ[μ] MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ ((Y ⁻¹' s).indicator 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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.Measure.map (fun (a : α) => (X a, Y a)) μ))
:
(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 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)) =ᵐ[μ] 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)) =ᵐ[μ] 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}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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)) =ᵐ[μ] 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 Ω]
[SecondCountableTopology Ω]
{Y : α → Ω}
(hX : Measurable X)
(hY_int : MeasureTheory.Integrable Y μ)
:
MeasureTheory.condexp (MeasurableSpace.comap X mβ) μ Y =ᵐ[μ] 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.2) (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.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
theorem
ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff
{β : Type u_2}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
{x✝ : MeasurableSpace Ω}
[TopologicalSpace F]
{X : Ω → β}
{μ : MeasureTheory.Measure Ω}
(hX : Measurable X)
{f : Ω → F}
:
MeasureTheory.AEStronglyMeasurable (fun (x : β × Ω) => f x.2) (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 Ω}
(hX : Measurable X)
{f : Ω → F}
:
MeasureTheory.Integrable (fun (x : β × Ω) => f x.2) (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, ω)) μ) ↔ MeasureTheory.Integrable f μ
theorem
ProbabilityTheory.condexp_ae_eq_integral_condDistrib_id
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[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 =ᵐ[μ] fun (a : Ω) =>
∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib id X μ) (X a)