Documentation

Mathlib.Probability.Kernel.Condexp

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 #

Main statements #

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

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 to Ω with σ-algebra m ⊓ mΩ. We use m ⊓ mΩ instead of m to ensure that it is a sub-σ-algebra of . We then use Kernel.comap to get a kernel from m to instead of from m ⊓ mΩ to .

Equations
Instances For
    theorem ProbabilityTheory.condexpKernel_ae_eq_condexp' {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) :
    (fun (ω : Ω) => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ] MeasureTheory.condexp (m ) μ (s.indicator fun (ω : Ω) => 1)
    theorem ProbabilityTheory.condexpKernel_ae_eq_condexp {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ) {s : Set Ω} (hs : MeasurableSet s) :
    (fun (ω : Ω) => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ] MeasureTheory.condexp m μ (s.indicator fun (ω : Ω) => 1)
    theorem ProbabilityTheory.condexpKernel_ae_eq_trim_condexp {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ) {s : Set Ω} (hs : MeasurableSet s) :
    (fun (ω : Ω) => (((ProbabilityTheory.condexpKernel μ m) ω) s).toReal) =ᵐ[μ.trim hm] MeasureTheory.condexp m μ (s.indicator fun (ω : Ω) => 1)
    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 ) (hf_int : MeasureTheory.Integrable f μ) :
    MeasureTheory.condexp m μ f =ᵐ[μ] fun (ω : Ω) => ∫ (y : Ω), f y(ProbabilityTheory.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 ω).