Pull-out property of the conditional expectation

Let Ω be endowed with a measurable space structure mΩ, and let m : MeasurableSpace Ω such that m ≤ mΩ. Let μ be a measure over Ω. Let B : F →L[ℝ] E →L[ℝ] G a continuous bilinear map, f : Ω → F and g : Ω → E such that fun ω ↦ B (f ω) (g ω) is integrable, g is integrable and f is AEStronglyMeasurable with respect to m. The pull-out property of the conditional expectation states that almost surely, μ[B f g|m] = B f μ[g|m].

We specialize this statement to the cases where B is scalar multiplication and multiplication.

Main statements

• condExp_bilin_of_aestronglyMeasurable_left: The pull-out property of the conditional expectation: almost surely, μ[B f g|m] = B f μ[g|m].
• condExp_smul_of_aestronglyMeasurable_left: The pull-out property of the conditional expectation: almost surely, μ[f • g|m] = f • μ[g|m].
• condExp_mul_of_aestronglyMeasurable_left: The pull-out property of the conditional expectation: almost surely, μ[f * g|m] = f * μ[g|m].

Tags

conditional expectation, pull-out, bilinear map

theorem MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E] (hm : m ≤ mΩ) (f : SimpleFunc Ω F) {g : Ω → E} (hg : Integrable g μ) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (f ω)) (μ[g|m] ω)

Auxiliary lemma for condExp_bilin_of_stronglyMeasurable_left.

theorem MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E] (hm : m ≤ mΩ) [IsFiniteMeasure μ] {f : Ω → F} {g : Ω → E} (hf : StronglyMeasurable f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (f ω)) (μ[g|m] ω)

theorem MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E] (hm : m ≤ mΩ) [IsFiniteMeasure μ] {f : Ω → F} {g : Ω → E} (hf : AEStronglyMeasurable f μ) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (f ω)) (μ[g|m] ω)

theorem MeasureTheory.condExp_bilin_of_stronglyMeasurable_left {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E] {f : Ω → F} {g : Ω → E} (hf : StronglyMeasurable f) (hfg : Integrable (fun (ω : Ω) => (B (f ω)) (g ω)) μ) (hg : Integrable g μ) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (f ω)) (μ[g|m] ω)

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_bilin_of_stronglyMeasurable_right {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace F] {f : Ω → F} {g : Ω → E} (hg : StronglyMeasurable g) (hfg : Integrable (fun (ω : Ω) => (B (f ω)) (g ω)) μ) (hf : Integrable f μ) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (μ[f|m] ω)) (g ω)

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E] {f : Ω → F} {g : Ω → E} (hf : AEStronglyMeasurable f μ) (hfg : Integrable (fun (ω : Ω) => (B (f ω)) (g ω)) μ) (hg : Integrable g μ) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (f ω)) (μ[g|m] ω)

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace F] {f : Ω → F} {g : Ω → E} (hg : AEStronglyMeasurable g μ) (hfg : Integrable (fun (ω : Ω) => (B (f ω)) (g ω)) μ) (hf : Integrable f μ) : μ[fun (ω : Ω) => (B (f ω)) (g ω)|m] =ᶠ[ae μ] fun (ω : Ω) => (B (μ[f|m] ω)) (g ω)

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_smul_of_aestronglyMeasurable_left {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → ℝ} {g : Ω → E} (hf : AEStronglyMeasurable f μ) (hfg : Integrable (f • g) μ) (hg : Integrable g μ) : μ[f • g|m] =ᶠ[ae μ] f • μ[g|m]

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_smul_of_aestronglyMeasurable_right {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → ℝ} {g : Ω → E} (hf : Integrable f μ) (hfg : Integrable (f • g) μ) (hg : AEStronglyMeasurable g μ) : μ[f • g|m] =ᶠ[ae μ] μ[f|m] • g

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_mul_of_aestronglyMeasurable_left {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f g : Ω → ℝ} (hf : AEStronglyMeasurable f μ) (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_mul_of_aestronglyMeasurable_right {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f g : Ω → ℝ} (hg : AEStronglyMeasurable g μ) (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : μ[f * g|m] =ᶠ[ae μ] μ[f|m] * g

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_mul_of_stronglyMeasurable_left {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f g : Ω → ℝ} (hf : StronglyMeasurable f) (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_mul_of_stronglyMeasurable_right {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f g : Ω → ℝ} (hg : StronglyMeasurable g) (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : μ[f * g|m] =ᶠ[ae μ] μ[f|m] * g

Pull-out property of the conditional expectation.

theorem MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} (hm : m ≤ mΩ) (f : SimpleFunc Ω ℝ) {g : Ω → ℝ} (hg : Integrable g μ) : μ[⇑f * g|m] =ᶠ[ae μ] ⇑f * μ[g|m]

theorem MeasureTheory.condExp_stronglyMeasurable_mul_of_bound {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} (hm : m ≤ mΩ) [IsFiniteMeasure μ] {f g : Ω → ℝ} (hf : StronglyMeasurable f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

theorem MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} (hm : m ≤ mΩ) [IsFiniteMeasure μ] {f g : Ω → ℝ} (hf : AEStronglyMeasurable f μ) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c) : μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]