Kernel associated with a conditional expectation

We define condExpKernel μ m, a kernel from Ω to Ω such that for all integrable functions f, μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω).

This kernel is defined if Ω is a standard Borel space. In general, μ⟦s | m⟧ 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 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.

Main definitions

• condExpKernel μ m: kernel such that μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω).

Main statements

• condExp_ae_eq_integral_condExpKernel: μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω).

theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id {Ω : Type u_1} {F : Type u_2} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → F} [TopologicalSpace F] (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun (x : Ω × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (id ω, id ω)) μ)

theorem MeasureTheory.Integrable.comp_snd_map_prod_id {Ω : Type u_1} {F : Type u_2} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → F} [NormedAddCommGroup F] (hm : m ≤ mΩ) (hf : Integrable f μ) : Integrable (fun (x : Ω × Ω) => f x.2) (Measure.map (fun (ω : Ω) => (id ω, id ω)) μ)

@[irreducible]

noncomputable def ProbabilityTheory.condExpKernel {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω) : Kernel Ω Ω

Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω). It is defined as the conditional distribution of the identity given the identity, where the second identity is understood as a map from Ω with the σ-algebra mΩ to Ω with σ-algebra m ⊓ mΩ. We use m ⊓ mΩ instead of m to ensure that it is a sub-σ-algebra of mΩ. We then use Kernel.comap to get a kernel from m to mΩ instead of from m ⊓ mΩ to mΩ.

Equations

• ProbabilityTheory.condExpKernel μ m = if _h : Nonempty Ω then (ProbabilityTheory.condDistrib id id μ).comap id ⋯ else 0

theorem ProbabilityTheory.condExpKernel_def {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω) : condExpKernel μ m = if _h : Nonempty Ω then (condDistrib id id μ).comap id ⋯ else 0

@[deprecated ProbabilityTheory.condExpKernel (since := "2025-01-21")]

def ProbabilityTheory.condexpKernel {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω) : Kernel Ω Ω

Alias of ProbabilityTheory.condExpKernel.

---

Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condExpKernel μ m ω). It is defined as the conditional distribution of the identity given the identity, where the second identity is understood as a map from Ω with the σ-algebra mΩ to Ω with σ-algebra m ⊓ mΩ. We use m ⊓ mΩ instead of m to ensure that it is a sub-σ-algebra of mΩ. We then use Kernel.comap to get a kernel from m to mΩ instead of from m ⊓ mΩ to mΩ.

Equations

• @ProbabilityTheory.condexpKernel = @ProbabilityTheory.condExpKernel

theorem ProbabilityTheory.condExpKernel_eq {Ω : Type u_1} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [h : Nonempty Ω] (m : MeasurableSpace Ω) : condExpKernel μ m = (condDistrib id id μ).comap id ⋯

@[deprecated ProbabilityTheory.condExpKernel_eq (since := "2025-01-21")]

theorem ProbabilityTheory.condexpKernel_eq {Ω : Type u_1} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [h : Nonempty Ω] (m : MeasurableSpace Ω) : condExpKernel μ m = (condDistrib id id μ).comap id ⋯

Alias of ProbabilityTheory.condExpKernel_eq.

theorem ProbabilityTheory.condExpKernel_apply_eq_condDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [Nonempty Ω] {ω : Ω} : (condExpKernel μ m) ω = (condDistrib id id μ) (id ω)

@[deprecated ProbabilityTheory.condExpKernel_apply_eq_condDistrib (since := "2025-01-21")]

theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [Nonempty Ω] {ω : Ω} : (condExpKernel μ m) ω = (condDistrib id id μ) (id ω)

Alias of ProbabilityTheory.condExpKernel_apply_eq_condDistrib.

instance ProbabilityTheory.instIsMarkovKernelCondExpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] : IsMarkovKernel (condExpKernel μ m)

theorem ProbabilityTheory.compProd_trim_condExpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) : (μ.trim hm).compProd (condExpKernel μ m) = MeasureTheory.Measure.map (fun (ω : Ω) => (id ω, id ω)) μ

theorem ProbabilityTheory.condExpKernel_comp_trim {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) : (μ.trim hm).bind ⇑(condExpKernel μ m) = μ

theorem ProbabilityTheory.measurable_condExpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : Measurable fun (ω : Ω) => ((condExpKernel μ m) ω) s

@[deprecated ProbabilityTheory.measurable_condExpKernel (since := "2025-01-21")]

theorem ProbabilityTheory.measurable_condexpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : Measurable fun (ω : Ω) => ((condExpKernel μ m) ω) s

Alias of ProbabilityTheory.measurable_condExpKernel.

theorem ProbabilityTheory.stronglyMeasurable_condExpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => ((condExpKernel μ m) ω) s

@[deprecated ProbabilityTheory.stronglyMeasurable_condExpKernel (since := "2025-01-21")]

theorem ProbabilityTheory.stronglyMeasurable_condexpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => ((condExpKernel μ m) ω) s

Alias of ProbabilityTheory.stronglyMeasurable_condExpKernel.

theorem MeasureTheory.StronglyMeasurable.integral_condExpKernel' {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : StronglyMeasurable f) : StronglyMeasurable fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω

theorem MeasureTheory.StronglyMeasurable.integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : StronglyMeasurable f) : StronglyMeasurable fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω

theorem MeasureTheory.AEStronglyMeasurable.integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ

@[deprecated MeasureTheory.AEStronglyMeasurable.integral_condExpKernel (since := "2025-01-21")]

theorem MeasureTheory.AEStronglyMeasurable.integral_condexpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ

Alias of MeasureTheory.AEStronglyMeasurable.integral_condExpKernel.

theorem ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

@[deprecated ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel (since := "2025-01-24")]

theorem ProbabilityTheory.aestronglyMeasurable'_integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Alias of ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel.

@[deprecated ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel (since := "2025-01-21")]

theorem ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Alias of ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel.

theorem ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} (hm : m ≤ mΩ) (hf : MeasureTheory.AEStronglyMeasurable f μ) : ∀ᵐ (ω : Ω) ∂μ.trim hm, f =ᵐ[(condExpKernel μ m) ω] MeasureTheory.AEStronglyMeasurable.mk f hf

theorem MeasureTheory.Integrable.condExpKernel_ae {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} (hf_int : Integrable f μ) : ∀ᵐ (ω : Ω) ∂μ, Integrable f ((ProbabilityTheory.condExpKernel μ m) ω)

@[deprecated MeasureTheory.Integrable.condExpKernel_ae (since := "2025-01-21")]

theorem MeasureTheory.Integrable.condexpKernel_ae {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} (hf_int : Integrable f μ) : ∀ᵐ (ω : Ω) ∂μ, Integrable f ((ProbabilityTheory.condExpKernel μ m) ω)

Alias of MeasureTheory.Integrable.condExpKernel_ae.

theorem MeasureTheory.Integrable.integral_norm_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} (hf_int : Integrable f μ) : Integrable (fun (ω : Ω) => ∫ (y : Ω), ‖f y‖ ∂(ProbabilityTheory.condExpKernel μ m) ω) μ

@[deprecated MeasureTheory.Integrable.integral_norm_condExpKernel (since := "2025-01-21")]

theorem MeasureTheory.Integrable.integral_norm_condexpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} (hf_int : Integrable f μ) : Integrable (fun (ω : Ω) => ∫ (y : Ω), ‖f y‖ ∂(ProbabilityTheory.condExpKernel μ m) ω) μ

Alias of MeasureTheory.Integrable.integral_norm_condExpKernel.

theorem MeasureTheory.Integrable.norm_integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf_int : Integrable f μ) : Integrable (fun (ω : Ω) => ‖∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω‖) μ

@[deprecated MeasureTheory.Integrable.norm_integral_condExpKernel (since := "2025-01-21")]

theorem MeasureTheory.Integrable.norm_integral_condexpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf_int : Integrable f μ) : Integrable (fun (ω : Ω) => ‖∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω‖) μ

Alias of MeasureTheory.Integrable.norm_integral_condExpKernel.

theorem MeasureTheory.Integrable.integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf_int : Integrable f μ) : Integrable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ

@[deprecated MeasureTheory.Integrable.integral_condExpKernel (since := "2025-01-21")]

theorem MeasureTheory.Integrable.integral_condexpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] (hf_int : Integrable f μ) : Integrable (fun (ω : Ω) => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ

Alias of MeasureTheory.Integrable.integral_condExpKernel.

theorem ProbabilityTheory.integrable_toReal_condExpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : MeasureTheory.Integrable (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) μ

@[deprecated ProbabilityTheory.integrable_toReal_condExpKernel (since := "2025-01-21")]

theorem ProbabilityTheory.integrable_toReal_condexpKernel {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : MeasureTheory.Integrable (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) μ

Alias of ProbabilityTheory.integrable_toReal_condExpKernel.

theorem ProbabilityTheory.condExpKernel_ae_eq_condExp' {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun (ω : Ω) => 1|m ⊓ mΩ]

@[deprecated ProbabilityTheory.condExpKernel_ae_eq_condExp' (since := "2025-01-21")]

theorem ProbabilityTheory.condexpKernel_ae_eq_condexp' {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) : (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun (ω : Ω) => 1|m ⊓ mΩ]

Alias of ProbabilityTheory.condExpKernel_ae_eq_condExp'.

theorem ProbabilityTheory.condExpKernel_ae_eq_condExp {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) : (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun (ω : Ω) => 1|m]

@[deprecated ProbabilityTheory.condExpKernel_ae_eq_condExp (since := "2025-01-21")]

theorem ProbabilityTheory.condexpKernel_ae_eq_condexp {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) : (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun (ω : Ω) => 1|m]

Alias of ProbabilityTheory.condExpKernel_ae_eq_condExp.

theorem ProbabilityTheory.condExpKernel_ae_eq_trim_condExp {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) : (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) =ᵐ[μ.trim hm] μ[s.indicator fun (ω : Ω) => 1|m]

@[deprecated ProbabilityTheory.condExpKernel_ae_eq_trim_condExp (since := "2025-01-21")]

theorem ProbabilityTheory.condexpKernel_ae_eq_trim_condexp {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) : (fun (ω : Ω) => ((condExpKernel μ m) ω).real s) =ᵐ[μ.trim hm] μ[s.indicator fun (ω : Ω) => 1|m]

Alias of ProbabilityTheory.condExpKernel_ae_eq_trim_condExp.

theorem ProbabilityTheory.condExp_ae_eq_integral_condExpKernel' {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hf_int : MeasureTheory.Integrable f μ) : μ[f|m ⊓ mΩ] =ᵐ[μ] fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

@[deprecated ProbabilityTheory.condExp_ae_eq_integral_condExpKernel' (since := "2025-01-21")]

theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel' {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hf_int : MeasureTheory.Integrable f μ) : μ[f|m ⊓ mΩ] =ᵐ[μ] fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Alias of ProbabilityTheory.condExp_ae_eq_integral_condExpKernel'.

theorem ProbabilityTheory.condExp_ae_eq_integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf_int : MeasureTheory.Integrable f μ) : μ[f|m] =ᵐ[μ] fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to the integral ∫ y, f y ∂(condExpKernel μ m ω).

@[deprecated ProbabilityTheory.condExp_ae_eq_integral_condExpKernel (since := "2025-01-21")]

theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf_int : MeasureTheory.Integrable f μ) : μ[f|m] =ᵐ[μ] fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Alias of ProbabilityTheory.condExp_ae_eq_integral_condExpKernel.

---

The conditional expectation of f with respect to a σ-algebra m is almost everywhere equal to the integral ∫ y, f y ∂(condExpKernel μ m ω).

theorem ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf : MeasureTheory.StronglyMeasurable f) (hf_int : MeasureTheory.Integrable f μ) : μ[f|m] =ᵐ[μ.trim hm] fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Auxiliary lemma for condExp_ae_eq_trim_integral_condExpKernel.

theorem ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup F] {f : Ω → F} [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf_int : MeasureTheory.Integrable f μ) : μ[f|m] =ᵐ[μ.trim hm] fun (ω : Ω) => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

The conditional expectation of f with respect to a σ-algebra m is (μ.trim hm)-almost everywhere equal to the integral ∫ y, f y ∂(condExpKernel μ m ω).

Relation between conditional expectation, conditional kernel and the conditional measure.

theorem ProbabilityTheory.condExp_generateFrom_singleton {Ω : Type u_1} {F : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (hs : MeasurableSet s) {f : Ω → F} (hf : MeasureTheory.Integrable f μ) : μ[f|MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun (x : Ω) => ∫ (x : Ω), f x ∂μ[|s]

@[deprecated ProbabilityTheory.condExp_generateFrom_singleton (since := "2025-01-21")]

theorem ProbabilityTheory.condexp_generateFrom_singleton {Ω : Type u_1} {F : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (hs : MeasurableSet s) {f : Ω → F} (hf : MeasureTheory.Integrable f μ) : μ[f|MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun (x : Ω) => ∫ (x : Ω), f x ∂μ[|s]

Alias of ProbabilityTheory.condExp_generateFrom_singleton.

theorem ProbabilityTheory.condExp_set_generateFrom_singleton {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : μ[t.indicator fun (ω : Ω) => 1|MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun (x : Ω) => μ[|s].real t

@[deprecated ProbabilityTheory.condExp_set_generateFrom_singleton (since := "2025-01-21")]

theorem ProbabilityTheory.condexp_set_generateFrom_singleton {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} (hs : MeasurableSet s) (ht : MeasurableSet t) : μ[t.indicator fun (ω : Ω) => 1|MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun (x : Ω) => μ[|s].real t

Alias of ProbabilityTheory.condExp_set_generateFrom_singleton.

theorem ProbabilityTheory.condExpKernel_singleton_ae_eq_cond {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} [StandardBorelSpace Ω] (hs : MeasurableSet s) (ht : MeasurableSet t) : ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

@[deprecated ProbabilityTheory.condExpKernel_singleton_ae_eq_cond (since := "2025-01-21")]

theorem ProbabilityTheory.condexpKernel_singleton_ae_eq_cond {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s t : Set Ω} [StandardBorelSpace Ω] (hs : MeasurableSet s) (ht : MeasurableSet t) : ∀ᵐ (ω : Ω) ∂μ.restrict s, ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Alias of ProbabilityTheory.condExpKernel_singleton_ae_eq_cond.