Conditional expectation #
We build the conditional expectation of an integrable 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-strongly measurable
function μ[f|hm] which is integrable and verifies ∫ x in s, μ[f|hm] x ∂μ = ∫ x in s, f x ∂μ
for all 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 ofL². This is the orthogonal projection on the subspace of almost everywherem-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 sendsx ∈ Eto the conditional expectation of the indicator of the set with valuex. - Extend that map to
condexp_L1_clm : (α →₁[μ] E) →L[ℝ] (α →₁[μ] E). This is done using the same construction as the Bochner integral (see the filemeasure_theory/integral/set_to_L1). - Define the conditional expectation of a function
f : α → E, which is an integrable functionα → Eequal to 0 iffis not integrable, and equal to anm-measurable representative ofcondexp_L1_clmapplied to[f], the equivalence class offinL¹.
Main results #
The conditional expectation and its properties
condexp (m : measurable_space α) (μ : measure α) (f : α → E): conditional expectation offwith respect tom.integrable_condexp:condexpis integrable.strongly_measurable_condexp:condexpism-strongly-measurable.set_integral_condexp (hf : integrable f μ) (hs : measurable_set[m] s): ifm ≤ m0(the σ-algebra over which the measure is defined), then the conditional expectation verifies∫ x in s, condexp m μ f x ∂μ = ∫ x in s, f x ∂μfor anym-measurable sets.
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': twoLpfunctions verifying the equality of integrals defining the conditional expectation are equal.ae_eq_of_forall_set_integral_eq_of_sigma_finite': two functions verifying the equality of integrals defining the conditional expectation are equal almost 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 tocondexp.
Notations #
For a measure μ defined on a measurable space structure m0, another measurable space structure
m with hm : m ≤ m0 (a sub-σ-algebra) and a function f, we define the notation
μ[f|m] = condexp m μ f.
Implementation notes #
Most of the results in this file are valid for a complete real normed space F.
However, some lemmas also use 𝕜 : is_R_or_C:
condexp_L2is defined only for aninner_product_spacefor now, and we use𝕜for its field.- results about scalar multiplication are stated not only for
ℝbut also for𝕜if we happen to havenormed_space 𝕜 F.
Tags #
conditional expectation, conditional expected value
def
measure_theory.ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
[topological_space β]
(m : measurable_space α)
{m0 : measurable_space α}
(f : α → β)
(μ : measure_theory.measure α) :
Prop
A function f verifies ae_strongly_measurable' m f μ if it is μ-a.e. equal to
an m-strongly measurable function. This is similar to ae_strongly_measurable, but the
measurable_space structures used for the measurability statement and for the measure are
different.
Equations
- measure_theory.ae_strongly_measurable' m f μ = ∃ (g : α → β), measure_theory.strongly_measurable g ∧ f =ᵐ[μ] g
theorem
measure_theory.ae_strongly_measurable'.congr
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hfg : f =ᵐ[μ] g) :
theorem
measure_theory.ae_strongly_measurable'.add
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f g : α → β}
[has_add β]
[has_continuous_add β]
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hg : measure_theory.ae_strongly_measurable' m g μ) :
measure_theory.ae_strongly_measurable' m (f + g) μ
theorem
measure_theory.ae_strongly_measurable'.neg
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[add_group β]
[topological_add_group β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
theorem
measure_theory.ae_strongly_measurable'.sub
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
[add_group β]
[topological_add_group β]
{f g : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hgm : measure_theory.ae_strongly_measurable' m g μ) :
measure_theory.ae_strongly_measurable' m (f - g) μ
theorem
measure_theory.ae_strongly_measurable'.const_smul
{α : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
[has_smul 𝕜 β]
[has_continuous_const_smul 𝕜 β]
(c : 𝕜)
(hf : measure_theory.ae_strongly_measurable' m f μ) :
measure_theory.ae_strongly_measurable' m (c • f) μ
theorem
measure_theory.ae_strongly_measurable'.const_inner
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{𝕜 : Type u_2}
{β : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group β]
[inner_product_space 𝕜 β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(c : β) :
measure_theory.ae_strongly_measurable' m (λ (x : α), has_inner.inner c (f x)) μ
noncomputable
def
measure_theory.ae_strongly_measurable'.mk
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
(f : α → β)
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
α → β
An m-strongly measurable function almost everywhere equal to f.
Equations
theorem
measure_theory.ae_strongly_measurable'.strongly_measurable_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
theorem
measure_theory.ae_strongly_measurable'.ae_eq_mk
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{f : α → β}
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
theorem
measure_theory.ae_strongly_measurable'.continuous_comp
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space β]
{γ : Type u_3}
[topological_space γ]
{f : α → β}
{g : β → γ}
(hg : continuous g)
(hf : measure_theory.ae_strongly_measurable' m f μ) :
measure_theory.ae_strongly_measurable' m (g ∘ f) μ
theorem
measure_theory.ae_strongly_measurable'_of_ae_strongly_measurable'_trim
{α : Type u_1}
{β : Type u_2}
{m m0 m0' : measurable_space α}
[topological_space β]
(hm0 : m0 ≤ m0')
{μ : measure_theory.measure α}
{f : α → β}
(hf : measure_theory.ae_strongly_measurable' m f (μ.trim hm0)) :
theorem
measure_theory.strongly_measurable.ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
{m m0 : measurable_space α}
[topological_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measure_theory.strongly_measurable f) :
theorem
measure_theory.ae_eq_trim_iff_of_ae_strongly_measurable'
{α : Type u_1}
{β : Type u_2}
[topological_space β]
[topological_space.metrizable_space β]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → β}
(hm : m ≤ m0)
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hgm : measure_theory.ae_strongly_measurable' m g μ) :
measure_theory.ae_strongly_measurable'.mk f hfm =ᵐ[μ.trim hm] measure_theory.ae_strongly_measurable'.mk g hgm ↔ f =ᵐ[μ] g
theorem
measure_theory.ae_strongly_measurable.comp_ae_measurable'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space β]
{mα : measurable_space α}
{mγ : measurable_space γ}
{f : α → β}
{μ : measure_theory.measure γ}
{g : γ → α}
(hf : measure_theory.ae_strongly_measurable f (measure_theory.measure.map g μ))
(hg : ae_measurable g μ) :
measure_theory.ae_strongly_measurable' (measurable_space.comap g mα) (f ∘ g) μ
theorem
measure_theory.ae_strongly_measurable'.ae_strongly_measurable'_of_measurable_space_le_on
{α : Type u_1}
{E : Type u_2}
{m m₂ m0 : measurable_space α}
{μ : measure_theory.measure α}
[topological_space E]
[has_zero E]
(hm : m ≤ m0)
{s : set α}
{f : α → E}
(hs_m : measurable_set s)
(hs : ∀ (t : set α), measurable_set (s ∩ t) → measurable_set (s ∩ t))
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hf_zero : f =ᵐ[μ.restrict sᶜ] 0) :
If the restriction to a set s of a σ-algebra m is included in the restriction to s of
another σ-algebra m₂ (hypothesis hs), the set s is m measurable and a function f almost
everywhere supported on s is m-ae-strongly-measurable, then f is also
m₂-ae-strongly-measurable.
The subset Lp_meas of Lp functions a.e. measurable with respect to a sub-sigma-algebra #
def
measure_theory.Lp_meas_subgroup
{α : Type u_1}
(F : Type u_6)
[normed_add_comm_group F]
(m : measurable_space α)
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α) :
add_subgroup ↥(measure_theory.Lp F p μ)
Lp_meas_subgroup F m p μ is the subspace of Lp F p μ containing functions f verifying
ae_strongly_measurable' m f μ, i.e. functions which are μ-a.e. equal to
an m-strongly measurable function.
Equations
- measure_theory.Lp_meas_subgroup F m p μ = {carrier := {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}, add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for ↥measure_theory.Lp_meas_subgroup
def
measure_theory.Lp_meas
{α : Type u_1}
(F : Type u_6)
(𝕜 : Type u_11)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
(m : measurable_space α)
[measurable_space α]
(p : ennreal)
(μ : measure_theory.measure α) :
submodule 𝕜 ↥(measure_theory.Lp F p μ)
Lp_meas F 𝕜 m p μ is the subspace of Lp F p μ containing functions f verifying
ae_strongly_measurable' m f μ, i.e. functions which are μ-a.e. equal to
an m-strongly measurable function.
Equations
- measure_theory.Lp_meas F 𝕜 m p μ = {carrier := {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}, add_mem' := _, zero_mem' := _, smul_mem' := _}
Instances for ↥measure_theory.Lp_meas
theorem
measure_theory.mem_Lp_meas_subgroup_iff_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp F p μ)} :
f ∈ measure_theory.Lp_meas_subgroup F m p μ ↔ measure_theory.ae_strongly_measurable' m ⇑f μ
theorem
measure_theory.mem_Lp_meas_iff_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp F p μ)} :
f ∈ measure_theory.Lp_meas F 𝕜 m p μ ↔ measure_theory.ae_strongly_measurable' m ⇑f μ
theorem
measure_theory.Lp_meas.ae_strongly_measurable'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
theorem
measure_theory.mem_Lp_meas_self
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m0 : measurable_space α}
(μ : measure_theory.measure α)
(f : ↥(measure_theory.Lp F p μ)) :
f ∈ measure_theory.Lp_meas F 𝕜 m0 p μ
theorem
measure_theory.Lp_meas_subgroup_coe
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp_meas_subgroup F m p μ)} :
theorem
measure_theory.Lp_meas_coe
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)} :
theorem
measure_theory.mem_Lp_meas_indicator_const_Lp
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(hm : m ≤ m0)
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
{c : F} :
measure_theory.indicator_const_Lp p _ hμs c ∈ measure_theory.Lp_meas F 𝕜 m p μ
The subspace Lp_meas is complete. #
We define an isometry_equiv 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).
theorem
measure_theory.mem_ℒp_trim_of_mem_Lp_meas_subgroup
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p μ))
(hf_meas : f ∈ measure_theory.Lp_meas_subgroup F m p μ) :
measure_theory.mem_ℒp (Exists.some _) p (μ.trim hm)
If f belongs to Lp_meas_subgroup F m p μ, then the measurable function it is almost
everywhere equal to (given by ae_measurable.mk) belongs to ℒp for the measure μ.trim hm.
theorem
measure_theory.mem_Lp_meas_subgroup_to_Lp_of_trim
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
If f belongs to Lp for the measure μ.trim hm, then it belongs to the subgroup
Lp_meas_subgroup F m p μ.
noncomputable
def
measure_theory.Lp_meas_subgroup_to_Lp_trim
{α : Type u_1}
(F : Type u_6)
(p : ennreal)
[normed_add_comm_group F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
↥(measure_theory.Lp F p (μ.trim hm))
Map from Lp_meas_subgroup to Lp F p (μ.trim hm).
Equations
noncomputable
def
measure_theory.Lp_meas_to_Lp_trim
{α : Type u_1}
(F : Type u_6)
(𝕜 : Type u_11)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
↥(measure_theory.Lp F p (μ.trim hm))
Map from Lp_meas to Lp F p (μ.trim hm).
Equations
- measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f = measure_theory.mem_ℒp.to_Lp (Exists.some _) _
noncomputable
def
measure_theory.Lp_trim_to_Lp_meas_subgroup
{α : Type u_1}
(F : Type u_6)
(p : ennreal)
[normed_add_comm_group F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
↥(measure_theory.Lp_meas_subgroup F m p μ)
Map from Lp F p (μ.trim hm) to Lp_meas_subgroup, inverse of
Lp_meas_subgroup_to_Lp_trim.
Equations
- measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm f = ⟨measure_theory.mem_ℒp.to_Lp ⇑f _, _⟩
noncomputable
def
measure_theory.Lp_trim_to_Lp_meas
{α : Type u_1}
(F : Type u_6)
(𝕜 : Type u_11)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
↥(measure_theory.Lp_meas F 𝕜 m p μ)
Map from Lp F p (μ.trim hm) to Lp_meas, inverse of Lp_meas_to_Lp_trim.
Equations
- measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm f = ⟨measure_theory.mem_ℒp.to_Lp ⇑f _, _⟩
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_ae_eq
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
⇑(measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_trim_to_Lp_meas_subgroup_ae_eq
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
⇑(measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_meas_to_Lp_trim_ae_eq
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
⇑(measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_trim_to_Lp_meas_ae_eq
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp F p (μ.trim hm))) :
⇑(measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm f) =ᵐ[μ] ⇑f
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_right_inv
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
Lp_trim_to_Lp_meas_subgroup is a right inverse of Lp_meas_subgroup_to_Lp_trim.
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_left_inv
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
Lp_trim_to_Lp_meas_subgroup is a left inverse of Lp_meas_subgroup_to_Lp_trim.
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_add
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm (f + g) = measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f + measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm g
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_neg
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm (-f) = -measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_sub
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm (f - g) = measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm f - measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm g
theorem
measure_theory.Lp_meas_to_Lp_trim_smul
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(c : 𝕜)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ)) :
measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm (c • f) = c • measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm f
theorem
measure_theory.Lp_meas_subgroup_to_Lp_trim_norm_map
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas_subgroup F m p μ)) :
Lp_meas_subgroup_to_Lp_trim preserves the norm.
theorem
measure_theory.isometry_Lp_meas_subgroup_to_Lp_trim
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
(hm : m ≤ m0) :
noncomputable
def
measure_theory.Lp_meas_subgroup_to_Lp_trim_iso
{α : Type u_1}
(F : Type u_6)
(p : ennreal)
[normed_add_comm_group F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
[hp : fact (1 ≤ p)]
(hm : m ≤ m0) :
↥(measure_theory.Lp_meas_subgroup F m p μ) ≃ᵢ ↥(measure_theory.Lp F p (μ.trim hm))
Lp_meas_subgroup and Lp F p (μ.trim hm) are isometric.
Equations
- measure_theory.Lp_meas_subgroup_to_Lp_trim_iso F p μ hm = {to_equiv := {to_fun := measure_theory.Lp_meas_subgroup_to_Lp_trim F p μ hm, inv_fun := measure_theory.Lp_trim_to_Lp_meas_subgroup F p μ hm, left_inv := _, right_inv := _}, isometry_to_fun := _}
noncomputable
def
measure_theory.Lp_meas_subgroup_to_Lp_meas_iso
{α : Type u_1}
(F : Type u_6)
(𝕜 : Type u_11)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
[hp : fact (1 ≤ p)] :
↥(measure_theory.Lp_meas_subgroup F m p μ) ≃ᵢ ↥(measure_theory.Lp_meas F 𝕜 m p μ)
Lp_meas_subgroup and Lp_meas are isometric.
Equations
noncomputable
def
measure_theory.Lp_meas_to_Lp_trim_lie
{α : Type u_1}
(F : Type u_6)
(𝕜 : Type u_11)
(p : ennreal)
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
(μ : measure_theory.measure α)
[hp : fact (1 ≤ p)]
(hm : m ≤ m0) :
↥(measure_theory.Lp_meas F 𝕜 m p μ) ≃ₗᵢ[𝕜] ↥(measure_theory.Lp F p (μ.trim hm))
Lp_meas and Lp F p (μ.trim hm) are isometric, with a linear equivalence.
Equations
- measure_theory.Lp_meas_to_Lp_trim_lie F 𝕜 p μ hm = {to_linear_equiv := {to_fun := measure_theory.Lp_meas_to_Lp_trim F 𝕜 p μ hm, map_add' := _, map_smul' := _, inv_fun := measure_theory.Lp_trim_to_Lp_meas F 𝕜 p μ hm, left_inv := _, right_inv := _}, norm_map' := _}
@[protected, instance]
def
measure_theory.Lp_meas_subgroup.complete_space
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hm : fact (m ≤ m0)]
[complete_space F]
[hp : fact (1 ≤ p)] :
@[protected, nolint, instance]
def
measure_theory.Lp_meas.complete_space
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hm : fact (m ≤ m0)]
[complete_space F]
[hp : fact (1 ≤ p)] :
complete_space ↥(measure_theory.Lp_meas F 𝕜 m p μ)
theorem
measure_theory.is_complete_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
[complete_space F]
(hm : m ≤ m0) :
is_complete {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}
theorem
measure_theory.is_closed_ae_strongly_measurable'
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[hp : fact (1 ≤ p)]
[complete_space F]
(hm : m ≤ m0) :
is_closed {f : ↥(measure_theory.Lp F p μ) | measure_theory.ae_strongly_measurable' m ⇑f μ}
theorem
measure_theory.Lp_meas.ae_fin_strongly_measurable'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas F 𝕜 m p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤) :
We do not get ae_fin_strongly_measurable f (μ.trim hm), since we don't have
f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f but only the weaker
f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f.
theorem
measure_theory.Lp_meas_to_Lp_trim_lie_symm_indicator
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
[one_le_p : fact (1 ≤ p)]
[normed_space ℝ F]
{hm : m ≤ m0}
{s : set α}
{μ : measure_theory.measure α}
(hs : measurable_set s)
(hμs : ⇑(μ.trim hm) s ≠ ⊤)
(c : F) :
↑(⇑((measure_theory.Lp_meas_to_Lp_trim_lie F ℝ p μ hm).symm) (measure_theory.indicator_const_Lp p hs hμs c)) = measure_theory.indicator_const_Lp p _ _ c
When applying the inverse of Lp_meas_to_Lp_trim_lie (which takes a function in the Lp space of
the sub-sigma algebra and returns its version in the larger Lp space) to an indicator of the
sub-sigma-algebra, we obtain an indicator in the Lp space of the larger sigma-algebra.
theorem
measure_theory.Lp_meas_to_Lp_trim_lie_symm_to_Lp
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[one_le_p : fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(f : α → F)
(hf : measure_theory.mem_ℒp f p (μ.trim hm)) :
↑(⇑((measure_theory.Lp_meas_to_Lp_trim_lie F ℝ p μ hm).symm) (measure_theory.mem_ℒp.to_Lp f hf)) = measure_theory.mem_ℒp.to_Lp f _
theorem
measure_theory.Lp.induction_strongly_measurable_aux
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(measure_theory.Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : set α} (hs : measurable_set s) (hμs : ⇑μ s < ⊤), P ↑(measure_theory.Lp.simple_func.indicator_const p _ _ c))
(h_add : ∀ ⦃f g : α → F⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), measure_theory.ae_strongly_measurable' m f μ → measure_theory.ae_strongly_measurable' m g μ → disjoint (function.support f) (function.support g) → P (measure_theory.mem_ℒp.to_Lp f hf) → P (measure_theory.mem_ℒp.to_Lp g hg) → P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg))
(h_closed : is_closed {f : ↥(measure_theory.Lp_meas F ℝ m p μ) | P ↑f})
(f : ↥(measure_theory.Lp F p μ)) :
measure_theory.ae_strongly_measurable' m ⇑f μ → P f
Auxiliary lemma for Lp.induction_strongly_measurable.
theorem
measure_theory.Lp.induction_strongly_measurable
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : ↥(measure_theory.Lp F p μ) → Prop)
(h_ind : ∀ (c : F) {s : set α} (hs : measurable_set s) (hμs : ⇑μ s < ⊤), P ↑(measure_theory.Lp.simple_func.indicator_const p _ _ c))
(h_add : ∀ ⦃f g : α → F⦄ (hf : measure_theory.mem_ℒp f p μ) (hg : measure_theory.mem_ℒp g p μ), measure_theory.strongly_measurable f → measure_theory.strongly_measurable g → disjoint (function.support f) (function.support g) → P (measure_theory.mem_ℒp.to_Lp f hf) → P (measure_theory.mem_ℒp.to_Lp g hg) → P (measure_theory.mem_ℒp.to_Lp f hf + measure_theory.mem_ℒp.to_Lp g hg))
(h_closed : is_closed {f : ↥(measure_theory.Lp_meas F ℝ m p μ) | P ↑f})
(f : ↥(measure_theory.Lp F p μ)) :
measure_theory.ae_strongly_measurable' m ⇑f μ → P f
To prove something for an Lp function a.e. strongly measurable with respect to a
sub-σ-algebra m in a normed space, it suffices to show that
- the property holds for (multiples of) characteristic functions which are measurable w.r.t.
m; - is closed under addition;
- the set of functions in
Lpstrongly measurable w.r.t.mfor which the property holds is closed.
theorem
measure_theory.mem_ℒp.induction_strongly_measurable
{α : Type u_1}
{F : Type u_6}
{p : ennreal}
[normed_add_comm_group F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[fact (1 ≤ p)]
[normed_space ℝ F]
(hm : m ≤ m0)
(hp_ne_top : p ≠ ⊤)
(P : (α → F) → Prop)
(h_ind : ∀ (c : F) ⦃s : set α⦄, measurable_set s → ⇑μ s < ⊤ → P (s.indicator (λ (_x : α), c)))
(h_add : ∀ ⦃f g : α → F⦄, disjoint (function.support f) (function.support g) → measure_theory.mem_ℒp f p μ → measure_theory.mem_ℒp g p μ → measure_theory.strongly_measurable f → measure_theory.strongly_measurable g → P f → P g → P (f + g))
(h_closed : is_closed {f : ↥(measure_theory.Lp_meas F ℝ m p μ) | P ⇑f})
(h_ae : ∀ ⦃f g : α → F⦄, f =ᵐ[μ] g → measure_theory.mem_ℒp f p μ → P f → P g)
⦃f : α → F⦄
(hf : measure_theory.mem_ℒp f p μ)
(hfm : measure_theory.ae_strongly_measurable' m f μ) :
P f
To prove something for an arbitrary mem_ℒp function a.e. strongly measurable with respect
to a sub-σ-algebra m in a normed space, it suffices to show that
- the property holds for (multiples of) characteristic functions which are measurable w.r.t.
m; - is closed under addition;
- the set of functions in the
Lᵖspace strongly measurable w.r.t.mfor which the property holds is closed. - the property is closed under the almost-everywhere equal relation.
Uniqueness of the conditional expectation #
theorem
measure_theory.Lp_meas.ae_eq_zero_of_forall_set_integral_eq_zero
{α : Type u_1}
{E' : Type u_5}
{𝕜 : Type u_11}
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp_meas E' 𝕜 m p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑f s μ)
(hf_zero : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, ⇑f x ∂μ = 0) :
theorem
measure_theory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero'
{α : Type u_1}
{E' : Type u_5}
(𝕜 : Type u_11)
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E' p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑f s μ)
(hf_zero : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, ⇑f x ∂μ = 0)
(hf_meas : measure_theory.ae_strongly_measurable' m ⇑f μ) :
theorem
measure_theory.Lp.ae_eq_of_forall_set_integral_eq'
{α : Type u_1}
{E' : Type u_5}
(𝕜 : Type u_11)
{p : ennreal}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp E' p μ))
(hp_ne_zero : p ≠ 0)
(hp_ne_top : p ≠ ⊤)
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑f s μ)
(hg_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on ⇑g s μ)
(hfg : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, ⇑f x ∂μ = ∫ (x : α) in s, ⇑g x ∂μ)
(hf_meas : measure_theory.ae_strongly_measurable' m ⇑f μ)
(hg_meas : measure_theory.ae_strongly_measurable' m ⇑g μ) :
Uniqueness of the conditional expectation
theorem
measure_theory.ae_eq_of_forall_set_integral_eq_of_sigma_finite'
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on f s μ)
(hg_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on g s μ)
(hfg_eq : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ)
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hgm : measure_theory.ae_strongly_measurable' m g μ) :
theorem
measure_theory.integral_norm_le_of_forall_fin_meas_integral_eq
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
{f g : α → ℝ}
(hf : measure_theory.strongly_measurable f)
(hfi : measure_theory.integrable_on f s μ)
(hg : measure_theory.strongly_measurable g)
(hgi : measure_theory.integrable_on g s μ)
(hgf : ∀ (t : set α), measurable_set t → ⇑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
Let m be a sub-σ-algebra of m0, f a m0-measurable function and g a m-measurable
function, such that their integrals coincide on m-measurable sets with finite measure.
Then ∫ x in s, ‖g x‖ ∂μ ≤ ∫ x in s, ‖f x‖ ∂μ on all m-measurable sets with finite measure.
theorem
measure_theory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
{f g : α → ℝ}
(hf : measure_theory.strongly_measurable f)
(hfi : measure_theory.integrable_on f s μ)
(hg : measure_theory.strongly_measurable g)
(hgi : measure_theory.integrable_on g s μ)
(hgf : ∀ (t : set α), measurable_set t → ⇑μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
Let m be a sub-σ-algebra of m0, f a m0-measurable function and g a m-measurable
function, such that their integrals coincide on m-measurable sets with finite measure.
Then ∫⁻ x in s, ‖g x‖₊ ∂μ ≤ ∫⁻ x in s, ‖f x‖₊ ∂μ on all m-measurable sets with finite
measure.
Conditional expectation in L2 #
We define a conditional expectation in L2: it is the orthogonal projection on the subspace
Lp_meas.
noncomputable
def
measure_theory.condexp_L2
{α : Type u_1}
{E : Type u_4}
(𝕜 : Type u_11)
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
↥(measure_theory.Lp E 2 μ) →L[𝕜] ↥(measure_theory.Lp_meas E 𝕜 m 2 μ)
Conditional expectation of a function in L2 with respect to a sigma-algebra
Equations
- measure_theory.condexp_L2 𝕜 hm = orthogonal_projection (measure_theory.Lp_meas E 𝕜 m 2 μ)
theorem
measure_theory.ae_strongly_measurable'_condexp_L2
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
theorem
measure_theory.integrable_on_condexp_L2_of_measure_ne_top
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hμs : ⇑μ s ≠ ⊤)
(f : ↥(measure_theory.Lp E 2 μ)) :
measure_theory.integrable_on ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) s μ
theorem
measure_theory.integrable_condexp_L2_of_is_finite_measure
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.is_finite_measure μ]
{f : ↥(measure_theory.Lp E 2 μ)} :
measure_theory.integrable ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) μ
theorem
measure_theory.norm_condexp_L2_le_one
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0) :
‖measure_theory.condexp_L2 𝕜 hm‖ ≤ 1
theorem
measure_theory.norm_condexp_L2_le
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
theorem
measure_theory.snorm_condexp_L2_le
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
measure_theory.snorm ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) 2 μ ≤ measure_theory.snorm ⇑f 2 μ
theorem
measure_theory.norm_condexp_L2_coe_le
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ)) :
theorem
measure_theory.inner_condexp_L2_left_eq_right
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
{f g : ↥(measure_theory.Lp E 2 μ)} :
has_inner.inner ↑(⇑(measure_theory.condexp_L2 𝕜 hm) f) g = has_inner.inner f ↑(⇑(measure_theory.condexp_L2 𝕜 hm) g)
theorem
measure_theory.condexp_L2_indicator_of_measurable
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : E) :
↑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 _ hμs c)) = measure_theory.indicator_const_Lp 2 _ hμs c
theorem
measure_theory.inner_condexp_L2_eq_inner_fun
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f g : ↥(measure_theory.Lp E 2 μ))
(hg : measure_theory.ae_strongly_measurable' m ⇑g μ) :
has_inner.inner ↑(⇑(measure_theory.condexp_L2 𝕜 hm) f) g = has_inner.inner f g
theorem
measure_theory.integral_condexp_L2_eq_of_fin_meas_real
{α : Type u_1}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
(f : ↥(measure_theory.Lp 𝕜 2 μ))
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
theorem
measure_theory.lintegral_nnnorm_condexp_L2_le
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(f : ↥(measure_theory.Lp ℝ 2 μ)) :
theorem
measure_theory.condexp_L2_ae_eq_zero_of_ae_eq_zero
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
{f : ↥(measure_theory.Lp ℝ 2 μ)}
(hf : ⇑f =ᵐ[μ.restrict s] 0) :
theorem
measure_theory.lintegral_nnnorm_condexp_L2_indicator_le_real
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(ht : measurable_set t)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.condexp_L2_const_inner
{α : Type u_1}
{E : Type u_4}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E 2 μ))
(c : E) :
⇑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.mem_ℒp.to_Lp (λ (a : α), has_inner.inner c (⇑f a)) _)) =ᵐ[μ] λ (a : α), has_inner.inner c (⇑(⇑(measure_theory.condexp_L2 𝕜 hm) f) a)
condexp_L2 commutes with taking inner products with constants. See the lemma
condexp_L2_comp_continuous_linear_map for a more general result about commuting with continuous
linear maps.
theorem
measure_theory.integral_condexp_L2_eq
{α : Type u_1}
{E' : Type u_5}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(f : ↥(measure_theory.Lp E' 2 μ))
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
condexp_L2 verifies the equality of integrals defining the conditional expectation.
theorem
measure_theory.condexp_L2_comp_continuous_linear_map
{α : Type u_1}
{E' : Type u_5}
(𝕜 : Type u_11)
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{E'' : Type u_12}
(𝕜' : Type u_13)
[is_R_or_C 𝕜']
[normed_add_comm_group E'']
[inner_product_space 𝕜' E'']
[complete_space E'']
[normed_space ℝ E'']
(hm : m ≤ m0)
(T : E' →L[ℝ] E'')
(f : ↥(measure_theory.Lp E' 2 μ)) :
theorem
measure_theory.condexp_L2_indicator_ae_eq_smul
{α : Type u_1}
{E' : Type u_5}
(𝕜 : Type u_11)
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E') :
⇑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 hs hμs x)) =ᵐ[μ] λ (a : α), ⇑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1)) a • x
theorem
measure_theory.condexp_L2_indicator_eq_to_span_singleton_comp
{α : Type u_1}
{E' : Type u_5}
(𝕜 : Type u_11)
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E') :
↑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 hs hμs x)) = (continuous_linear_map.to_span_singleton ℝ x).comp_Lp ↑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
theorem
measure_theory.set_lintegral_nnnorm_condexp_L2_indicator_le
{α : Type u_1}
{E' : Type u_5}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E')
{t : set α}
(ht : measurable_set t)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.lintegral_nnnorm_condexp_L2_indicator_le
{α : Type u_1}
{E' : Type u_5}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E')
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.integrable_condexp_L2_indicator
{α : Type u_1}
{E' : Type u_5}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group E']
[inner_product_space 𝕜 E']
[complete_space E']
[normed_space ℝ E']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E') :
measure_theory.integrable ⇑(⇑(measure_theory.condexp_L2 𝕜 hm) (measure_theory.indicator_const_Lp 2 hs hμs x)) μ
If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.
noncomputable
def
measure_theory.condexp_ind_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
↥(measure_theory.Lp G 2 μ)
Conditional expectation of the indicator of a measurable set with finite measure, in L2.
Equations
- measure_theory.condexp_ind_smul hm hs hμs x = ⇑(continuous_linear_map.comp_LpL 2 μ (continuous_linear_map.to_span_singleton ℝ x)) ↑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
theorem
measure_theory.ae_strongly_measurable'_condexp_ind_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.ae_strongly_measurable' m ⇑(measure_theory.condexp_ind_smul hm hs hμs x) μ
theorem
measure_theory.condexp_ind_smul_add
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x y : G) :
measure_theory.condexp_ind_smul hm hs hμs (x + y) = measure_theory.condexp_ind_smul hm hs hμs x + measure_theory.condexp_ind_smul hm hs hμs y
theorem
measure_theory.condexp_ind_smul_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : ℝ)
(x : G) :
measure_theory.condexp_ind_smul hm hs hμs (c • x) = c • measure_theory.condexp_ind_smul hm hs hμs x
theorem
measure_theory.condexp_ind_smul_smul'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : 𝕜)
(x : F) :
measure_theory.condexp_ind_smul hm hs hμs (c • x) = c • measure_theory.condexp_ind_smul hm hs hμs x
theorem
measure_theory.condexp_ind_smul_ae_eq_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
⇑(measure_theory.condexp_ind_smul hm hs hμs x) =ᵐ[μ] λ (a : α), ⇑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1)) a • x
theorem
measure_theory.set_lintegral_nnnorm_condexp_ind_smul_le
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G)
{t : set α}
(ht : measurable_set t)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.lintegral_nnnorm_condexp_ind_smul_le
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G)
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.integrable_condexp_ind_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.integrable ⇑(measure_theory.condexp_ind_smul hm hs hμs x) μ
If the measure μ.trim hm is sigma-finite, then the conditional expectation of a measurable set
with finite measure is integrable.
theorem
measure_theory.condexp_ind_smul_empty
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_space ℝ G]
{hm : m ≤ m0}
{x : G} :
theorem
measure_theory.set_integral_condexp_L2_indicator
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤) :
theorem
measure_theory.set_integral_condexp_ind_smul
{α : Type u_1}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space ℝ G']
[complete_space G']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(x : G') :
theorem
measure_theory.condexp_L2_indicator_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hm : m ≤ m0)
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
[measure_theory.sigma_finite (μ.trim hm)] :
0 ≤ᵐ[μ] ⇑(⇑(measure_theory.condexp_L2 ℝ hm) (measure_theory.indicator_const_Lp 2 hs hμs 1))
theorem
measure_theory.condexp_ind_smul_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
{E : Type u_2}
[normed_lattice_add_comm_group E]
[normed_space ℝ E]
[ordered_smul ℝ E]
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x) :
0 ≤ᵐ[μ] ⇑(measure_theory.condexp_ind_smul hm hs hμs x)
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.
noncomputable
def
measure_theory.condexp_ind_L1_fin
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
↥(measure_theory.Lp G 1 μ)
Conditional expectation of the indicator of a measurable set with finite measure, as a function in L1.
Equations
- measure_theory.condexp_ind_L1_fin hm hs hμs x = measure_theory.integrable.to_L1 ⇑(measure_theory.condexp_ind_smul hm hs hμs x) _
theorem
measure_theory.condexp_ind_L1_fin_ae_eq_condexp_ind_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
⇑(measure_theory.condexp_ind_L1_fin hm hs hμs x) =ᵐ[μ] ⇑(measure_theory.condexp_ind_smul hm hs hμs x)
theorem
measure_theory.condexp_ind_L1_fin_add
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x y : G) :
measure_theory.condexp_ind_L1_fin hm hs hμs (x + y) = measure_theory.condexp_ind_L1_fin hm hs hμs x + measure_theory.condexp_ind_L1_fin hm hs hμs y
theorem
measure_theory.condexp_ind_L1_fin_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : ℝ)
(x : G) :
measure_theory.condexp_ind_L1_fin hm hs hμs (c • x) = c • measure_theory.condexp_ind_L1_fin hm hs hμs x
theorem
measure_theory.condexp_ind_L1_fin_smul'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : 𝕜)
(x : F) :
measure_theory.condexp_ind_L1_fin hm hs hμs (c • x) = c • measure_theory.condexp_ind_L1_fin hm hs hμs x
theorem
measure_theory.norm_condexp_ind_L1_fin_le
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
theorem
measure_theory.condexp_ind_L1_fin_disjoint_union
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G) :
measure_theory.condexp_ind_L1_fin hm _ _ x = measure_theory.condexp_ind_L1_fin hm hs hμs x + measure_theory.condexp_ind_L1_fin hm ht hμt x
noncomputable
def
measure_theory.condexp_ind_L1
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
[normed_space ℝ G]
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
(s : set α)
[measure_theory.sigma_finite (μ.trim hm)]
(x : G) :
↥(measure_theory.Lp G 1 μ)
Conditional expectation of the indicator of a set, as a function in L1. Its value for sets which are not both measurable and of finite measure is not used: we set it to 0.
Equations
- measure_theory.condexp_ind_L1 hm μ s x = dite (measurable_set s ∧ ⇑μ s ≠ ⊤) (λ (hs : measurable_set s ∧ ⇑μ s ≠ ⊤), measure_theory.condexp_ind_L1_fin hm _ _ x) (λ (hs : ¬(measurable_set s ∧ ⇑μ s ≠ ⊤)), 0)
theorem
measure_theory.condexp_ind_L1_of_measurable_set_of_measure_ne_top
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s x = measure_theory.condexp_ind_L1_fin hm hs hμs x
theorem
measure_theory.condexp_ind_L1_of_measure_eq_top
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hμs : ⇑μ s = ⊤)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s x = 0
theorem
measure_theory.condexp_ind_L1_of_not_measurable_set
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : ¬measurable_set s)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s x = 0
theorem
measure_theory.condexp_ind_L1_add
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(x y : G) :
measure_theory.condexp_ind_L1 hm μ s (x + y) = measure_theory.condexp_ind_L1 hm μ s x + measure_theory.condexp_ind_L1 hm μ s y
theorem
measure_theory.condexp_ind_L1_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(c : ℝ)
(x : G) :
measure_theory.condexp_ind_L1 hm μ s (c • x) = c • measure_theory.condexp_ind_L1 hm μ s x
theorem
measure_theory.condexp_ind_L1_smul'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(c : 𝕜)
(x : F) :
measure_theory.condexp_ind_L1 hm μ s (c • x) = c • measure_theory.condexp_ind_L1 hm μ s x
theorem
measure_theory.norm_condexp_ind_L1_le
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(x : G) :
theorem
measure_theory.continuous_condexp_ind_L1
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
continuous (λ (x : G), measure_theory.condexp_ind_L1 hm μ s x)
theorem
measure_theory.condexp_ind_L1_disjoint_union
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G) :
measure_theory.condexp_ind_L1 hm μ (s ∪ t) x = measure_theory.condexp_ind_L1 hm μ s x + measure_theory.condexp_ind_L1 hm μ t x
noncomputable
def
measure_theory.condexp_ind
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
[normed_space ℝ G]
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)]
(s : set α) :
G →L[ℝ] ↥(measure_theory.Lp G 1 μ)
Conditional expectation of the indicator of a set, as a linear map from G to L1.
Equations
- measure_theory.condexp_ind hm μ s = {to_linear_map := {to_fun := measure_theory.condexp_ind_L1 hm μ s _inst_21, map_add' := _, map_smul' := _}, cont := _}
theorem
measure_theory.condexp_ind_ae_eq_condexp_ind_smul
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
⇑(⇑(measure_theory.condexp_ind hm μ s) x) =ᵐ[μ] ⇑(measure_theory.condexp_ind_smul hm hs hμs x)
theorem
measure_theory.ae_strongly_measurable'_condexp_ind
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : G) :
measure_theory.ae_strongly_measurable' m ⇑(⇑(measure_theory.condexp_ind hm μ s) x) μ
@[simp]
theorem
measure_theory.condexp_ind_empty
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
measure_theory.condexp_ind hm μ ∅ = 0
theorem
measure_theory.condexp_ind_smul'
{α : Type u_1}
{F : Type u_6}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F]
[normed_space 𝕜 F]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
[normed_space ℝ F]
[smul_comm_class ℝ 𝕜 F]
(c : 𝕜)
(x : F) :
⇑(measure_theory.condexp_ind hm μ s) (c • x) = c • ⇑(measure_theory.condexp_ind hm μ s) x
theorem
measure_theory.norm_condexp_ind_apply_le
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(x : G) :
theorem
measure_theory.norm_condexp_ind_le
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.condexp_ind_disjoint_union_apply
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅)
(x : G) :
⇑(measure_theory.condexp_ind hm μ (s ∪ t)) x = ⇑(measure_theory.condexp_ind hm μ s) x + ⇑(measure_theory.condexp_ind hm μ t) x
theorem
measure_theory.condexp_ind_disjoint_union
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(hst : s ∩ t = ∅) :
measure_theory.condexp_ind hm μ (s ∪ t) = measure_theory.condexp_ind hm μ s + measure_theory.condexp_ind hm μ t
theorem
measure_theory.dominated_fin_meas_additive_condexp_ind
{α : Type u_1}
(G : Type u_8)
[normed_add_comm_group G]
{m m0 : measurable_space α}
[normed_space ℝ G]
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.set_integral_condexp_ind
{α : Type u_1}
{G' : Type u_9}
[normed_add_comm_group G']
[normed_space ℝ G']
[complete_space G']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(ht : measurable_set t)
(hμs : ⇑μ s ≠ ⊤)
(hμt : ⇑μ t ≠ ⊤)
(x : G') :
theorem
measure_theory.condexp_ind_of_measurable
{α : Type u_1}
{G : Type u_8}
[normed_add_comm_group G]
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
[normed_space ℝ G]
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : G) :
⇑(measure_theory.condexp_ind hm μ s) c = measure_theory.indicator_const_Lp 1 _ hμs c
theorem
measure_theory.condexp_ind_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{E : Type u_2}
[normed_lattice_add_comm_group E]
[normed_space ℝ E]
[ordered_smul ℝ E]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : E)
(hx : 0 ≤ x) :
0 ≤ ⇑(measure_theory.condexp_ind hm μ s) x
noncomputable
def
measure_theory.condexp_L1_clm
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)] :
↥(measure_theory.Lp F' 1 μ) →L[ℝ] ↥(measure_theory.Lp F' 1 μ)
Conditional expectation of a function as a linear map from α →₁[μ] F' to itself.
Equations
theorem
measure_theory.condexp_L1_clm_smul
{α : Type u_1}
{F' : Type u_7}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F']
[normed_space 𝕜 F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(c : 𝕜)
(f : ↥(measure_theory.Lp F' 1 μ)) :
⇑(measure_theory.condexp_L1_clm hm μ) (c • f) = c • ⇑(measure_theory.condexp_L1_clm hm μ) f
theorem
measure_theory.condexp_L1_clm_indicator_const_Lp
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : F') :
⇑(measure_theory.condexp_L1_clm hm μ) (measure_theory.indicator_const_Lp 1 hs hμs x) = ⇑(measure_theory.condexp_ind hm μ s) x
theorem
measure_theory.condexp_L1_clm_indicator_const
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(x : F') :
⇑(measure_theory.condexp_L1_clm hm μ) ↑(measure_theory.Lp.simple_func.indicator_const 1 hs hμs x) = ⇑(measure_theory.condexp_ind hm μ s) x
theorem
measure_theory.set_integral_condexp_L1_clm_of_measure_ne_top
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(f : ↥(measure_theory.Lp F' 1 μ))
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤) :
Auxiliary lemma used in the proof of set_integral_condexp_L1_clm.
theorem
measure_theory.set_integral_condexp_L1_clm
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{s : set α}
(f : ↥(measure_theory.Lp F' 1 μ))
(hs : measurable_set s) :
The integral of the conditional expectation condexp_L1_clm over an m-measurable set is equal
to the integral of f on that set. See also set_integral_condexp, the similar statement for
condexp.
theorem
measure_theory.ae_strongly_measurable'_condexp_L1_clm
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : ↥(measure_theory.Lp F' 1 μ)) :
theorem
measure_theory.condexp_L1_clm_Lp_meas
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : ↥(measure_theory.Lp_meas F' ℝ m 1 μ)) :
⇑(measure_theory.condexp_L1_clm hm μ) ↑f = ↑f
theorem
measure_theory.condexp_L1_clm_of_ae_strongly_measurable'
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : ↥(measure_theory.Lp F' 1 μ))
(hfm : measure_theory.ae_strongly_measurable' m ⇑f μ) :
⇑(measure_theory.condexp_L1_clm hm μ) f = f
noncomputable
def
measure_theory.condexp_L1
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
(hm : m ≤ m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
↥(measure_theory.Lp F' 1 μ)
Conditional expectation of a function, in L1. Its value is 0 if the function is not
integrable. The function-valued condexp should be used instead in most cases.
Equations
- measure_theory.condexp_L1 hm μ f = measure_theory.set_to_fun μ (measure_theory.condexp_ind hm μ) _ f
theorem
measure_theory.condexp_L1_undef
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hf : ¬measure_theory.integrable f μ) :
measure_theory.condexp_L1 hm μ f = 0
theorem
measure_theory.condexp_L1_eq
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hf : measure_theory.integrable f μ) :
measure_theory.condexp_L1 hm μ f = ⇑(measure_theory.condexp_L1_clm hm μ) (measure_theory.integrable.to_L1 f hf)
@[simp]
theorem
measure_theory.condexp_L1_zero
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)] :
measure_theory.condexp_L1 hm μ 0 = 0
@[simp]
theorem
measure_theory.condexp_L1_measure_zero
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{f : α → F'}
(hm : m ≤ m0) :
measure_theory.condexp_L1 hm 0 f = 0
theorem
measure_theory.ae_strongly_measurable'_condexp_L1
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'} :
theorem
measure_theory.condexp_L1_congr_ae
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → F'}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(h : f =ᵐ[μ] g) :
measure_theory.condexp_L1 hm μ f = measure_theory.condexp_L1 hm μ g
theorem
measure_theory.integrable_condexp_L1
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
theorem
measure_theory.set_integral_condexp_L1
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
{s : set α}
(hf : measure_theory.integrable f μ)
(hs : measurable_set s) :
The integral of the conditional expectation condexp_L1 over an m-measurable set is equal to
the integral of f on that set. See also set_integral_condexp, the similar statement for
condexp.
theorem
measure_theory.condexp_L1_add
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp_L1 hm μ (f + g) = measure_theory.condexp_L1 hm μ f + measure_theory.condexp_L1 hm μ g
theorem
measure_theory.condexp_L1_neg
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
measure_theory.condexp_L1 hm μ (-f) = -measure_theory.condexp_L1 hm μ f
theorem
measure_theory.condexp_L1_smul
{α : Type u_1}
{F' : Type u_7}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F']
[normed_space 𝕜 F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
(c : 𝕜)
(f : α → F') :
measure_theory.condexp_L1 hm μ (c • f) = c • measure_theory.condexp_L1 hm μ f
theorem
measure_theory.condexp_L1_sub
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp_L1 hm μ (f - g) = measure_theory.condexp_L1 hm μ f - measure_theory.condexp_L1 hm μ g
theorem
measure_theory.condexp_L1_of_ae_strongly_measurable'
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hfm : measure_theory.ae_strongly_measurable' m f μ)
(hfi : measure_theory.integrable f μ) :
⇑(measure_theory.condexp_L1 hm μ f) =ᵐ[μ] f
theorem
measure_theory.condexp_L1_mono
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{hm : m ≤ m0}
[measure_theory.sigma_finite (μ.trim hm)]
{E : Type u_2}
[normed_lattice_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
[ordered_smul ℝ E]
{f g : α → E}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ)
(hfg : f ≤ᵐ[μ] g) :
⇑(measure_theory.condexp_L1 hm μ f) ≤ᵐ[μ] ⇑(measure_theory.condexp_L1 hm μ g)
Conditional expectation of a function #
@[irreducible]
noncomputable
def
measure_theory.condexp
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
(m : measurable_space α)
{m0 : measurable_space α}
(μ : measure_theory.measure α)
(f : α → F') :
α → F'
Conditional expectation of a function. It is defined as 0 if any one of the following conditions is true:
mis not a sub-σ-algebra ofm0,μis not σ-finite with respect tom,fis not integrable.
Equations
- measure_theory.condexp m μ f = dite (m ≤ m0) (λ (hm : m ≤ m0), dite (measure_theory.sigma_finite (μ.trim hm) ∧ measure_theory.integrable f μ) (λ (h : measure_theory.sigma_finite (μ.trim hm) ∧ measure_theory.integrable f μ), ite (measure_theory.strongly_measurable f) f (measure_theory.ae_strongly_measurable'.mk ⇑(measure_theory.condexp_L1 hm μ f) _)) (λ (h : ¬(measure_theory.sigma_finite (μ.trim hm) ∧ measure_theory.integrable f μ)), 0)) (λ (hm : ¬m ≤ m0), 0)
theorem
measure_theory.condexp_of_not_le
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
(hm_not : ¬m ≤ m0) :
measure_theory.condexp m μ f = 0
theorem
measure_theory.condexp_of_not_sigma_finite
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
(hm : m ≤ m0)
(hμm_not : ¬measure_theory.sigma_finite (μ.trim hm)) :
measure_theory.condexp m μ f = 0
theorem
measure_theory.condexp_of_sigma_finite
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
(hm : m ≤ m0)
[hμm : measure_theory.sigma_finite (μ.trim hm)] :
theorem
measure_theory.condexp_of_strongly_measurable
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[hμm : measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hf : measure_theory.strongly_measurable f)
(hfi : measure_theory.integrable f μ) :
measure_theory.condexp m μ f = f
theorem
measure_theory.condexp_const
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
(c : F')
[measure_theory.is_finite_measure μ] :
measure_theory.condexp m μ (λ (x : α), c) = λ (_x : α), c
theorem
measure_theory.condexp_ae_eq_condexp_L1
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[hμm : measure_theory.sigma_finite (μ.trim hm)]
(f : α → F') :
measure_theory.condexp m μ f =ᵐ[μ] ⇑(measure_theory.condexp_L1 hm μ f)
theorem
measure_theory.condexp_ae_eq_condexp_L1_clm
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hf : measure_theory.integrable f μ) :
measure_theory.condexp m μ f =ᵐ[μ] ⇑(⇑(measure_theory.condexp_L1_clm hm μ) (measure_theory.integrable.to_L1 f hf))
theorem
measure_theory.condexp_undef
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
(hf : ¬measure_theory.integrable f μ) :
measure_theory.condexp m μ f = 0
@[simp]
theorem
measure_theory.condexp_zero
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α} :
measure_theory.condexp m μ 0 = 0
theorem
measure_theory.strongly_measurable_condexp
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'} :
theorem
measure_theory.condexp_congr_ae
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → F'}
(h : f =ᵐ[μ] g) :
measure_theory.condexp m μ f =ᵐ[μ] measure_theory.condexp m μ g
theorem
measure_theory.condexp_of_ae_strongly_measurable'
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[hμm : measure_theory.sigma_finite (μ.trim hm)]
{f : α → F'}
(hf : measure_theory.ae_strongly_measurable' m f μ)
(hfi : measure_theory.integrable f μ) :
measure_theory.condexp m μ f =ᵐ[μ] f
theorem
measure_theory.integrable_condexp
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'} :
theorem
measure_theory.set_integral_condexp
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
{s : set α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
(hf : measure_theory.integrable f μ)
(hs : measurable_set s) :
The integral of the conditional expectation μ[f|hm] over an m-measurable set is equal to
the integral of f on that set.
theorem
measure_theory.integral_condexp
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f : α → F'}
(hm : m ≤ m0)
[hμm : measure_theory.sigma_finite (μ.trim hm)]
(hf : measure_theory.integrable f μ) :
theorem
measure_theory.ae_eq_condexp_of_forall_set_integral_eq
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg_int_finite : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → measure_theory.integrable_on g s μ)
(hg_eq : ∀ (s : set α), measurable_set s → ⇑μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ)
(hgm : measure_theory.ae_strongly_measurable' m g μ) :
g =ᵐ[μ] measure_theory.condexp m μ f
Uniqueness of the conditional expectation
If a function is a.e. m-measurable, verifies an integrability condition and has same integral
as f on all m-measurable sets, then it is a.e. equal to μ[f|hm].
theorem
measure_theory.condexp_bot'
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[hμ : μ.ae.ne_bot]
(f : α → F') :
theorem
measure_theory.condexp_bot_ae_eq
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m0 : measurable_space α}
{μ : measure_theory.measure α}
(f : α → F') :
theorem
measure_theory.condexp_bot
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.is_probability_measure μ]
(f : α → F') :
theorem
measure_theory.condexp_add
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp m μ (f + g) =ᵐ[μ] measure_theory.condexp m μ f + measure_theory.condexp m μ g
theorem
measure_theory.condexp_finset_sum
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
{s : finset ι}
{f : ι → α → F'}
(hf : ∀ (i : ι), i ∈ s → measure_theory.integrable (f i) μ) :
measure_theory.condexp m μ (s.sum (λ (i : ι), f i)) =ᵐ[μ] s.sum (λ (i : ι), measure_theory.condexp m μ (f i))
theorem
measure_theory.condexp_smul
{α : Type u_1}
{F' : Type u_7}
{𝕜 : Type u_11}
[is_R_or_C 𝕜]
[normed_add_comm_group F']
[normed_space 𝕜 F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(c : 𝕜)
(f : α → F') :
measure_theory.condexp m μ (c • f) =ᵐ[μ] c • measure_theory.condexp m μ f
theorem
measure_theory.condexp_neg
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(f : α → F') :
measure_theory.condexp m μ (-f) =ᵐ[μ] -measure_theory.condexp m μ f
theorem
measure_theory.condexp_sub
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{f g : α → F'}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ) :
measure_theory.condexp m μ (f - g) =ᵐ[μ] measure_theory.condexp m μ f - measure_theory.condexp m μ g
theorem
measure_theory.condexp_condexp_of_le
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{f : α → F'}
{m₁ m₂ m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm₁₂ : m₁ ≤ m₂)
(hm₂ : m₂ ≤ m0)
[measure_theory.sigma_finite (μ.trim hm₂)] :
measure_theory.condexp m₁ μ (measure_theory.condexp m₂ μ f) =ᵐ[μ] measure_theory.condexp m₁ μ f
theorem
measure_theory.condexp_mono
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_lattice_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
[ordered_smul ℝ E]
{f g : α → E}
(hf : measure_theory.integrable f μ)
(hg : measure_theory.integrable g μ)
(hfg : f ≤ᵐ[μ] g) :
measure_theory.condexp m μ f ≤ᵐ[μ] measure_theory.condexp m μ g
theorem
measure_theory.condexp_nonneg
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_lattice_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
[ordered_smul ℝ E]
{f : α → E}
(hf : 0 ≤ᵐ[μ] f) :
0 ≤ᵐ[μ] measure_theory.condexp m μ f
theorem
measure_theory.condexp_nonpos
{α : Type u_1}
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
{E : Type u_2}
[normed_lattice_add_comm_group E]
[complete_space E]
[normed_space ℝ E]
[ordered_smul ℝ E]
{f : α → E}
(hf : f ≤ᵐ[μ] 0) :
measure_theory.condexp m μ f ≤ᵐ[μ] 0
theorem
measure_theory.tendsto_condexp_L1_of_dominated_convergence
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(hm : m ≤ m0)
[measure_theory.sigma_finite (μ.trim hm)]
{fs : ℕ → α → F'}
{f : α → F'}
(bound_fs : α → ℝ)
(hfs_meas : ∀ (n : ℕ), measure_theory.ae_strongly_measurable (fs n) μ)
(h_int_bound_fs : measure_theory.integrable bound_fs μ)
(hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x)
(hfs : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), fs n x) filter.at_top (nhds (f x))) :
filter.tendsto (λ (n : ℕ), measure_theory.condexp_L1 hm μ (fs n)) filter.at_top (nhds (measure_theory.condexp_L1 hm μ f))
Lebesgue dominated convergence theorem: sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their image by
condexp_L1.
theorem
measure_theory.tendsto_condexp_unique
{α : Type u_1}
{F' : Type u_7}
[normed_add_comm_group F']
[normed_space ℝ F']
[complete_space F']
{m m0 : measurable_space α}
{μ : measure_theory.measure α}
(fs gs : ℕ → α → F')
(f g : α → F')
(hfs_int : ∀ (n : ℕ), measure_theory.integrable (fs n) μ)
(hgs_int : ∀ (n : ℕ), measure_theory.integrable (gs n) μ)
(hfs : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), fs n x) filter.at_top (nhds (f x)))
(hgs : ∀ᵐ (x : α) ∂μ, filter.tendsto (λ (n : ℕ), gs n x) filter.at_top (nhds (g x)))
(bound_fs : α → ℝ)
(h_int_bound_fs : measure_theory.integrable bound_fs μ)
(bound_gs : α → ℝ)
(h_int_bound_gs : measure_theory.integrable bound_gs μ)
(hfs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖fs n x‖ ≤ bound_fs x)
(hgs_bound : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖gs n x‖ ≤ bound_gs x)
(hfg : ∀ (n : ℕ), measure_theory.condexp m μ (fs n) =ᵐ[μ] measure_theory.condexp m μ (gs n)) :
measure_theory.condexp m μ f =ᵐ[μ] measure_theory.condexp m μ g
If two sequences of functions have a.e. equal conditional expectations at each step, converge and verify dominated convergence hypotheses, then the conditional expectations of their limits are a.e. equal.