Conditional expectation #

We build the conditional expectation of a function f with value in a Banach space with respect to a measure μ (defined on a measurable space structure m0) and a measurable space structure m with hm : m ≤ m0 (a sub-sigma-algebra). This is an m-measurable function μ[f|hm] which is integrable and verifies ∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ for any m-measurable sets s. It is unique as an element of L¹.

The construction is done in four steps:

• Define the conditional expectation of an L² function, as an element of L². This is the orthogonal projection on the subspace of almost everywhere m-measurable functions.
• Show that the conditional expectation of the indicator of a measurable set with finite measure is integrable and define a map set α → (E →L[ℝ] (α →₁[μ] E)) which to a set associates a linear map. That linear map sends x ∈ E to the conditional expectation of the indicator of the set with value x.
• Extend that map to condexp_L1_clm : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the file measure_theory/integral/set_to_L1).
• Define the conditional expectation of a function f : α → E, which is an integrable function α → E equal to 0 if f is not integrable, and equal to an m-measurable representative of condexp_L1_clm applied to [f], the equivalence class of f in L¹.

Main results #

The conditional expectation and its properties

• condexp (hm : m ≤ m0) (μ : measure α) (f : α → E): conditional expectation of f with respect to m.
• integrable_condexp : condexp is integrable.
• measurable_condexp : condexp is m-measurable.
• set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s) : the conditional expectation verifies ∫ x in s, condexp hm μ f x ∂μ = ∫ x in s, f x ∂μ for any m-measurable set s.

While condexp is function-valued, we also define condexp_L1 with value in L1 and a continuous linear map condexp_L1_clm from L1 to L1. condexp should be used in most cases.

Uniqueness of the conditional expectation

• Lp.ae_eq_of_forall_set_integral_eq': two Lp functions verifying the equality of integrals defining the conditional expectation are equal everywhere.
• ae_eq_of_forall_set_integral_eq_of_sigma_finite': two functions verifying the equality of integrals defining the conditional expectation are equal everywhere. Requires [sigma_finite (μ.trim hm)].
• ae_eq_condexp_of_forall_set_integral_eq: an a.e. m-measurable function which verifies the equality of integrals is a.e. equal to condexp.

Notations #

For a measure μ defined on a measurable space structure m0, another measurable space structure m with hm : m ≤ m0 (a sub-sigma-algebra) and a function f, we define the notation

• μ[f|hm] = condexp hm μ f.

Implementation notes #

Most of the results in this file are valid for a second countable, borel, real normed space F. However, some lemmas also use 𝕜 : is_R_or_C:

• condexp_L2 is defined only for an inner_product_space for now, and we use 𝕜 for its field.
• results about scalar multiplication are stated not only for ℝ but also for 𝕜 if we happen to have normed_space 𝕜 F.

Tags #

conditional expectation, conditional expected value

The subset Lp_meas of Lp functions a.e. measurable with respect to a sub-sigma-algebra #

The subspace Lp_meas is complete. #

We define an isometric between Lp_meas_subgroup and the Lp space corresponding to the measure μ.trim hm. As a consequence, the completeness of Lp implies completeness of Lp_meas_subgroup (and Lp_meas).

Uniqueness of the conditional expectation #

Conditional expectation in L2 #

We define a conditional expectation in L2: it is the orthogonal projection on the subspace Lp_meas.

Conditional expectation of an indicator as a continuous linear map. #

The goal of this section is to build condexp_ind (hm : m ≤ m0) (μ : measure α) (s : set s) : G →L[ℝ] α →₁[μ] G, which takes x : G to the conditional expectation of the indicator of the set s with value x, seen as an element of α →₁[μ] G.