Documentation

Mathlib.Probability.Kernel.CondDistrib

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 #

Main statements #

@[irreducible]
noncomputable def ProbabilityTheory.condDistrib {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] :
{x : MeasurableSpace α} → [inst : MeasurableSpace β] → (αΩ)(αβ)(μ : MeasureTheory.Measure α) → [inst_1 : MeasureTheory.IsFiniteMeasure μ] → 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.

Equations
Instances For
    theorem ProbabilityTheory.condDistrib_def {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] :
    ∀ {x : MeasurableSpace α} [inst : MeasurableSpace β] (Y : αΩ) (X : αβ) (μ : MeasureTheory.Measure α) [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.condDistrib Y X μ = (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).condKernel
    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 ) (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) :
    ∫⁻ (a : α) in X ⁻¹' t, ((ProbabilityTheory.condDistrib Y X μ) (X a)) sμ = μ (X ⁻¹' t Y ⁻¹' s)
    @[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) :
    ∫⁻ (a : α) in X ⁻¹' t, ((ProbabilityTheory.condDistrib Y X μ) (X a)) sμ = μ (X ⁻¹' t Y ⁻¹' s)

    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 ) μ ((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 ) μ 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 ) μ 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 ) μ 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 ) μ 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 ) μ 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 Ω} [inst : TopologicalSpace F] {X : Ωβ} {μ : MeasureTheory.Measure Ω}, 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 Ω}, 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 ) μ f =ᵐ[μ] fun (a : Ω) => ∫ (y : Ω), f y(ProbabilityTheory.condDistrib id X μ) (X a)