# 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 of `Y : α → Ω` given `X : α → β`, where `Ω` is a standard Borel space.

## Main statements #

- `condDistrib_ae_eq_condExp`: 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⟧ 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))`.

source
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 μ] :
condDistrib Y X μ = (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).condKernel
source
@[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

source
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 μ)
source
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)` .

source
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)) μ
source
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 μ) :
(MeasureTheory.Measure.map X μ).bind ⇑(condDistrib Y X μ) = MeasureTheory.Measure.map Y μ
source
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') :
condDistrib Y X μ = condDistrib Y' X' μ
source
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') :
condDistrib Y X μ = condDistrib Y X' μ
source
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') :
condDistrib Y X μ = condDistrib Y' X μ
source
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
source
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)) μ)
source
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
source
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 μ)
source
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)) μ
source
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)
source
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)) μ
source
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 Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ

`condDistrib` is a.e. uniquely defined as the kernel satisfying the defining property of `condKernel`.

source
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 Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ

`condDistrib` is a.e. uniquely defined as the kernel satisfying the defining property of `condKernel`.

source
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 κ
source
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) :
⇑(condDistrib (f ∘ Y) X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑((condDistrib Y X μ).map f)
source
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) :
⇑(condDistrib (f ∘ X) X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑(Kernel.deterministic f hf)
source
theorem ProbabilityTheory.condDistrib_self {α : Type u_1} {Ω : Type u_3} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (Y : α → Ω) :
⇑(condDistrib Y Y μ) =ᵐ[MeasureTheory.Measure.map Y μ] ⇑Kernel.id
source
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) ⋯)
source
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) ν)
source
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 μ)
source
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 μ)
source
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) μ
source
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)
source
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))
source
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 μ)
source
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)) μ
source
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 μ)
source
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)‖) μ
source
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 μ)
source
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)) μ
source
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) :
∫⁻ (a : α) in X ⁻¹' t, ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)
source
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, ((condDistrib Y X μ) (X a)) s ∂μ = μ (t ∩ Y ⁻¹' s)
source
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`.

source
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)) μ)) :
μ[fun (a : α) => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(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.

source
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)) μ) :
μ[fun (a : α) => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(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.

source
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)) μ) :
μ[fun (a : α) => f (X a, Y a)|MeasurableSpace.comap X mβ] =ᵐ[μ] fun (a : α) => ∫ (y : Ω), f (X a, y) ∂(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.

source
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)
source
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 μ) :
μ[Y|MeasurableSpace.comap X mβ] =ᵐ[μ] fun (a : α) => ∫ (y : Ω), y ∂(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))`.

source
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 ω, ω)) μ)
source
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 ω, ω)) μ)
source
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 μ
source
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 μ
source
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 μ) :
μ[f|MeasurableSpace.comap X mβ] =ᵐ[μ] fun (a : Ω) => ∫ (y : Ω), f y ∂(condDistrib id X μ) (X a)