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)).
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 μ]
:
@[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 μ]
:
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.
Equations
- ProbabilityTheory.condDistrib Y X μ = (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).condKernel
Instances For
instance
ProbabilityTheory.instIsMarkovKernelCondDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
[MeasurableSpace β]
:
IsMarkovKernel (condDistrib Y X μ)
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 Ω)
:
((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.compProd_map_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
(hY : AEMeasurable Y μ)
:
(MeasureTheory.Measure.map X μ).compProd (condDistrib Y X μ) = MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ
theorem
ProbabilityTheory.condDistrib_comp_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
:
theorem
ProbabilityTheory.condDistrib_congr
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{X' : α → β}
{Y' : α → Ω}
(hY : Y =ᵐ[μ] Y')
(hX : X =ᵐ[μ] X')
:
theorem
ProbabilityTheory.condDistrib_congr_right
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{X' : α → β}
(hX : X =ᵐ[μ] X')
:
theorem
ProbabilityTheory.condDistrib_congr_left
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{Y' : α → Ω}
(hY : Y =ᵐ[μ] Y')
:
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 : α) => ((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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y μ)
(hf : AEStronglyMeasurable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
(∀ᵐ (a : β) ∂Measure.map X μ, Integrable (fun (ω : Ω) => f (a, ω)) ((ProbabilityTheory.condDistrib Y X μ) a)) ∧ Integrable (fun (a : β) => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(ProbabilityTheory.condDistrib Y X μ) a) (Measure.map X μ) ↔ Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ)
theorem
MeasureTheory.StronglyMeasurable.integral_condDistrib
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
{F : Type u_4}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
[NormedAddCommGroup F]
{mα : MeasurableSpace α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hf : StronglyMeasurable f)
:
StronglyMeasurable fun (x : β) => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x
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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hY : AEMeasurable Y μ)
(hf : AEStronglyMeasurable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
AEStronglyMeasurable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x) (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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf : AEStronglyMeasurable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
AEStronglyMeasurable (fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.stronglyMeasurable_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]
(hf : MeasureTheory.StronglyMeasurable f)
:
MeasureTheory.StronglyMeasurable fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(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 (fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a)) μ
theorem
ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable
{α : 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)
{κ : Kernel β Ω}
[IsFiniteKernel κ]
(hκ : MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ)
:
condDistrib is a.e. uniquely defined as the kernel satisfying the defining property of
condKernel.
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 μ]
{Y : α → Ω}
{mβ : MeasurableSpace β}
(X : α → β)
(hY : AEMeasurable Y μ)
{κ : Kernel β Ω}
[IsFiniteKernel κ]
(hκ : MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ)
:
condDistrib is a.e. uniquely defined as the kernel satisfying the defining property of
condKernel.
theorem
ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{Y : α → Ω}
{mβ : MeasurableSpace β}
(X : α → β)
(hY : AEMeasurable Y μ)
(κ : Kernel β Ω)
[IsFiniteKernel κ]
:
⇑(condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ ↔ MeasureTheory.Measure.map (fun (x : α) => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ
theorem
ProbabilityTheory.condDistrib_comp
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{Y : α → Ω}
{mβ : MeasurableSpace β}
{Ω' : Type u_5}
{mΩ' : MeasurableSpace Ω'}
[StandardBorelSpace Ω']
[Nonempty Ω']
(X : α → β)
(hY : AEMeasurable Y μ)
{f : Ω → Ω'}
(hf : Measurable f)
:
theorem
ProbabilityTheory.condDistrib_comp_self
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{mβ : MeasurableSpace β}
(X : α → β)
{f : β → Ω}
(hf : Measurable f)
:
theorem
ProbabilityTheory.condDistrib_self
{α : Type u_1}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(Y : α → Ω)
:
theorem
ProbabilityTheory.condDistrib_const
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{mβ : MeasurableSpace β}
(X : α → β)
(c : Ω)
:
⇑(condDistrib (fun (x : α) => c) X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(Kernel.deterministic (fun (x : β) => c) ⋯)
theorem
ProbabilityTheory.condDistrib_map
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
{ν : MeasureTheory.Measure γ}
[MeasureTheory.IsFiniteMeasure ν]
{f : γ → α}
(hX : AEMeasurable X (MeasureTheory.Measure.map f ν))
(hY : AEMeasurable Y (MeasureTheory.Measure.map f ν))
(hf : AEMeasurable f ν)
:
⇑(condDistrib Y X (MeasureTheory.Measure.map f ν)) =ᵐ[MeasureTheory.Measure.map (X ∘ f) ν] ⇑(condDistrib (Y ∘ f) (X ∘ f) ν)
theorem
ProbabilityTheory.condDistrib_fst_prod
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{Y : α → Ω}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(X : α → β)
(hY : AEMeasurable Y μ)
(ν : MeasureTheory.Measure γ)
[MeasureTheory.IsProbabilityMeasure ν]
:
⇑(condDistrib (fun (ω : α × γ) => Y ω.1) (fun (ω : α × γ) => X ω.1) (μ.prod ν)) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(condDistrib Y X μ)
theorem
ProbabilityTheory.condDistrib_snd_prod
{α : Type u_1}
{β : Type u_2}
{Ω : Type u_3}
[MeasurableSpace Ω]
[StandardBorelSpace Ω]
[Nonempty Ω]
{mα : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{Y : α → Ω}
{mβ : MeasurableSpace β}
{γ : Type u_5}
{mγ : MeasurableSpace γ}
(X : α → β)
(hY : AEMeasurable Y μ)
(ν : MeasureTheory.Measure γ)
[MeasureTheory.IsProbabilityMeasure ν]
:
⇑(condDistrib (fun (ω : γ × α) => Y ω.2) (fun (ω : γ × α) => X ω.2) (ν.prod μ)) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(condDistrib Y X μ)
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 : α) => ((condDistrib Y X μ) (X a)).real s) μ
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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
∀ᵐ (b : β) ∂Measure.map X μ, 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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
∀ᵐ (a : α) ∂μ, 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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
Integrable (fun (x : β) => ∫ (y : Ω), ‖f (x, y)‖ ∂(ProbabilityTheory.condDistrib Y X μ) x) (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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
Integrable (fun (x : β) => ‖∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x‖) (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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
Integrable (fun (x : β) => ∫ (y : Ω), f (x, y) ∂(ProbabilityTheory.condDistrib Y X μ) x) (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 α}
{μ : Measure α}
[IsFiniteMeasure μ]
{X : α → β}
{Y : α → Ω}
{mβ : MeasurableSpace β}
{f : β × Ω → F}
[NormedSpace ℝ F]
(hX : AEMeasurable X μ)
(hY : AEMeasurable Y μ)
(hf_int : Integrable f (Measure.map (fun (a : α) => (X a, Y a)) μ))
:
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)
:
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)
:
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 : α) => ((condDistrib Y X μ) (X a)).real s) =ᵐ[μ] μ[(Y ⁻¹' s).indicator fun (ω : α) => 1|MeasurableSpace.comap X mβ]
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)) μ))
:
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)) μ)
:
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)) μ)
:
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)) μ)
:
μ[fun (a : α) => f (Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun (a : α) => ∫ (y : Ω), f y ∂(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 μ)
:
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_prodMk
{β : Type u_2}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : Measure Ω}
[TopologicalSpace F]
{f : Ω → F}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : β × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
@[deprecated MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk (since := "2025-03-05")]
theorem
MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk
{β : Type u_2}
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{F : Type u_6}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : Measure Ω}
[TopologicalSpace F]
{f : Ω → F}
(hf : AEStronglyMeasurable f μ)
:
AEStronglyMeasurable (fun (x : β × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
Alias of MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk.
theorem
MeasureTheory.Integrable.comp_snd_map_prodMk
{β : Type u_2}
{F : Type u_4}
[NormedAddCommGroup F]
{mβ : MeasurableSpace β}
{Ω : Type u_5}
{mΩ : MeasurableSpace Ω}
(X : Ω → β)
{μ : Measure Ω}
{f : Ω → F}
(hf_int : Integrable f μ)
:
Integrable (fun (x : β × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
@[deprecated MeasureTheory.Integrable.comp_snd_map_prodMk (since := "2025-03-05")]
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 : Ω → β)
{μ : Measure Ω}
{f : Ω → F}
(hf_int : Integrable f μ)
:
Integrable (fun (x : β × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (X ω, ω)) μ)
theorem
ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_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 μ
@[deprecated ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff (since := "2025-03-05")]
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 μ
Alias of ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff.
theorem
ProbabilityTheory.integrable_comp_snd_map_prodMk_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 μ
@[deprecated ProbabilityTheory.integrable_comp_snd_map_prodMk_iff (since := "2025-03-05")]
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 μ
Alias of ProbabilityTheory.integrable_comp_snd_map_prodMk_iff.
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 μ)
: