feat(Probability/Kernel/Condexp): some properties of condexpKernel (#6109)

`condexpKernel` is a Markov kernel, is strongly measurable and is a.e. equal to the conditional expectation.



Co-authored-by: RemyDegenne <Remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -60,6 +60,9 @@ theorem congr (hf : AEStronglyMeasurable' m f μ) (hfg : f =ᵐ[μ] g) : AEStron
   by obtain ⟨f', hf'_meas, hff'⟩ := hf; exact ⟨f', hf'_meas, hfg.symm.trans hff'⟩
 #align measure_theory.ae_strongly_measurable'.congr MeasureTheory.AEStronglyMeasurable'.congr
 
+theorem mono (hf : AEStronglyMeasurable' m f μ) (hm : m ≤ m') : AEStronglyMeasurable' m' f μ := by
+  obtain ⟨f', hf'_meas, hff'⟩ := hf; exact ⟨f', hf'_meas.mono hm, hff'⟩
+
 theorem add [Add β] [ContinuousAdd β] (hf : AEStronglyMeasurable' m f μ)
     (hg : AEStronglyMeasurable' m g μ) : AEStronglyMeasurable' m (f + g) μ := by
   rcases hf with ⟨f', h_f'_meas, hff'⟩

Mathlib/MeasureTheory/MeasurableSpace.lean

@@ -225,6 +225,10 @@ theorem Measurable.mono {ma ma' : MeasurableSpace α} {mb mb' : MeasurableSpace
   fun _t ht => ha _ <| hf <| hb _ ht
 #align measurable.mono Measurable.mono
 
+theorem measurable_id'' {m mα : MeasurableSpace α} (hm : m ≤ mα) : @Measurable α α mα m id :=
+  measurable_id.mono le_rfl hm
+#align probability_theory.measurable_id'' measurable_id''
+
 -- porting note: todo: add TC `DiscreteMeasurable` + instances
 
 @[measurability]

Mathlib/MeasureTheory/Measure/AEMeasurable.lean

@@ -16,9 +16,7 @@ We discuss several of its properties that are analogous to properties of measura
 -/
 
 
-open MeasureTheory MeasureTheory.Measure Filter Set Function
-
-open MeasureTheory Filter Classical ENNReal Interval
+open MeasureTheory MeasureTheory.Measure Filter Set Function Classical ENNReal
 
 variable {ι α β γ δ R : Type*} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ]
   [MeasurableSpace δ] {f g : α → β} {μ ν : Measure α}
@@ -41,6 +39,11 @@ theorem aemeasurable_zero_measure : AEMeasurable f (0 : Measure α) := by
   exact ⟨fun _ => f default, measurable_const, rfl⟩
 #align ae_measurable_zero_measure aemeasurable_zero_measure
 
+theorem aemeasurable_id'' (μ : Measure α) {m : MeasurableSpace α} (hm : m ≤ m0) :
+    @AEMeasurable α α m m0 id μ :=
+  @Measurable.aemeasurable α α m0 m id μ (measurable_id'' hm)
+#align probability_theory.ae_measurable_id'' aemeasurable_id''
+
 namespace AEMeasurable
 
 theorem mono_measure (h : AEMeasurable f μ) (h' : ν ≤ μ) : AEMeasurable f ν :=

Mathlib/Probability/Kernel/Condexp.lean

@@ -41,16 +41,6 @@ section AuxLemmas
 
 variable {Ω F : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → F}
 
--- Porting note: todo: move to `MeasureTheory/MeasurableSpace`, after `Measurable.mono`
-theorem measurable_id'' (hm : m ≤ mΩ) : @Measurable Ω Ω mΩ m id :=
-  measurable_id.mono le_rfl hm
-#align probability_theory.measurable_id'' ProbabilityTheory.measurable_id''
-
--- Porting note: todo: move to `MeasureTheory/MeasurableSpace`, after `Measurable.mono`
-theorem aemeasurable_id'' (μ : Measure Ω) (hm : m ≤ mΩ) : @AEMeasurable Ω Ω m mΩ id μ :=
-  @Measurable.aemeasurable Ω Ω mΩ m id μ (measurable_id'' hm)
-#align probability_theory.ae_measurable_id'' ProbabilityTheory.aemeasurable_id''
-
 theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id [TopologicalSpace F]
     (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x : Ω × Ω => f x.2)
       (@Measure.map Ω (Ω × Ω) (m.prod mΩ) mΩ (fun ω => (id ω, id ω)) μ) := by
@@ -71,91 +61,144 @@ end AuxLemmas
 
 variable {Ω F : Type*} [TopologicalSpace Ω] {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω]
   [PolishSpace Ω] [BorelSpace Ω] [Nonempty Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
-  [NormedAddCommGroup F] {f : Ω → F}
 
 /-- Kernel associated with the conditional expectation with respect to a σ-algebra. It satisfies
 `μ[f | m] =ᵐ[μ] fun ω => ∫ y, f y ∂(condexpKernel μ m ω)`.
 It is defined as the conditional distribution of the identity given the identity, where the second
-identity is understood as a map from `Ω` with the σ-algebra `mΩ` to `Ω` with σ-algebra `m`. -/
+identity is understood as a map from `Ω` with the σ-algebra `mΩ` to `Ω` with σ-algebra `m ⊓ mΩ`.
+We use `m ⊓ mΩ` instead of `m` to ensure that it is a sub-σ-algebra of `mΩ`. We then use
+`kernel.comap` to get a kernel from `m` to `mΩ` instead of from `m ⊓ mΩ` to `mΩ`. -/
 noncomputable irreducible_def condexpKernel (μ : Measure Ω) [IsFiniteMeasure μ]
     (m : MeasurableSpace Ω) : @kernel Ω Ω m mΩ :=
-  @condDistrib Ω Ω Ω _ mΩ _ _ _ mΩ m id id μ _
+  kernel.comap (@condDistrib Ω Ω Ω _ mΩ _ _ _ mΩ (m ⊓ mΩ) id id μ _) id
+    (measurable_id'' (inf_le_left : m ⊓ mΩ ≤ m))
 #align probability_theory.condexp_kernel ProbabilityTheory.condexpKernel
 
+lemma condexpKernel_apply_eq_condDistrib :
+    condexpKernel μ m ω = @condDistrib Ω Ω Ω _ mΩ _ _ _ mΩ (m ⊓ mΩ) id id μ _ (id ω) := by
+  simp_rw [condexpKernel, kernel.comap_apply]
+
+instance : IsMarkovKernel (condexpKernel μ m) := by simp only [condexpKernel]; infer_instance
+
 section Measurability
 
+variable [NormedAddCommGroup F] {f : Ω → F}
+
 theorem measurable_condexpKernel {s : Set Ω} (hs : MeasurableSet s) :
     Measurable[m] fun ω => condexpKernel μ m ω s := by
-  rw [condexpKernel]; convert measurable_condDistrib (μ := μ) hs; rw [MeasurableSpace.comap_id]
+  simp_rw [condexpKernel_apply_eq_condDistrib]
+  refine Measurable.mono ?_ (inf_le_left : m ⊓ mΩ ≤ m) le_rfl
+  convert measurable_condDistrib (μ := μ) hs
+  rw [MeasurableSpace.comap_id]
 #align probability_theory.measurable_condexp_kernel ProbabilityTheory.measurable_condexpKernel
 
+theorem stronglyMeasurable_condexpKernel {s : Set Ω} (hs : MeasurableSet s) :
+    StronglyMeasurable[m] fun ω => condexpKernel μ m ω s :=
+  Measurable.stronglyMeasurable (measurable_condexpKernel hs)
+
 theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condexpKernel [NormedSpace ℝ F]
-    [CompleteSpace F] (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) :
+    [CompleteSpace F] (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable (fun ω => ∫ y, f y ∂condexpKernel μ m ω) μ := by
-  rw [condexpKernel]
-  exact AEStronglyMeasurable.integral_condDistrib (aemeasurable_id'' μ hm) aemeasurable_id
-    (hf.comp_snd_map_prod_id hm)
+  simp_rw [condexpKernel_apply_eq_condDistrib]
+  exact AEStronglyMeasurable.integral_condDistrib
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
+    (hf.comp_snd_map_prod_id inf_le_right)
 #align measure_theory.ae_strongly_measurable.integral_condexp_kernel MeasureTheory.AEStronglyMeasurable.integral_condexpKernel
 
 theorem aestronglyMeasurable'_integral_condexpKernel [NormedSpace ℝ F] [CompleteSpace F]
-    (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) :
+    (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable' m (fun ω => ∫ y, f y ∂condexpKernel μ m ω) μ := by
   rw [condexpKernel]
-  have h := aestronglyMeasurable'_integral_condDistrib (aemeasurable_id'' μ hm) aemeasurable_id
-    (hf.comp_snd_map_prod_id hm)
-  rwa [MeasurableSpace.comap_id] at h
+  have h := aestronglyMeasurable'_integral_condDistrib
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
+    (hf.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
+  rw [MeasurableSpace.comap_id] at h
+  exact AEStronglyMeasurable'.mono h inf_le_left
 #align probability_theory.ae_strongly_measurable'_integral_condexp_kernel ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel
 
 end Measurability
 
 section Integrability
 
-theorem _root_.MeasureTheory.Integrable.condexpKernel_ae (hm : m ≤ mΩ) (hf_int : Integrable f μ) :
+variable [NormedAddCommGroup F] {f : Ω → F}
+
+theorem _root_.MeasureTheory.Integrable.condexpKernel_ae (hf_int : Integrable f μ) :
     ∀ᵐ ω ∂μ, Integrable f (condexpKernel μ m ω) := by
   rw [condexpKernel]
-  exact Integrable.condDistrib_ae (aemeasurable_id'' μ hm) aemeasurable_id
-    (hf_int.comp_snd_map_prod_id hm)
+  exact Integrable.condDistrib_ae
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
+    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
 #align measure_theory.integrable.condexp_kernel_ae MeasureTheory.Integrable.condexpKernel_ae
 
-theorem _root_.MeasureTheory.Integrable.integral_norm_condexpKernel (hm : m ≤ mΩ)
-    (hf_int : Integrable f μ) : Integrable (fun ω => ∫ y, ‖f y‖ ∂condexpKernel μ m ω) μ := by
+theorem _root_.MeasureTheory.Integrable.integral_norm_condexpKernel (hf_int : Integrable f μ) :
+    Integrable (fun ω => ∫ y, ‖f y‖ ∂condexpKernel μ m ω) μ := by
   rw [condexpKernel]
-  exact Integrable.integral_norm_condDistrib (aemeasurable_id'' μ hm) aemeasurable_id
-    (hf_int.comp_snd_map_prod_id hm)
+  exact Integrable.integral_norm_condDistrib
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
+    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
 #align measure_theory.integrable.integral_norm_condexp_kernel MeasureTheory.Integrable.integral_norm_condexpKernel
 
 theorem _root_.MeasureTheory.Integrable.norm_integral_condexpKernel [NormedSpace ℝ F]
-    [CompleteSpace F] (hm : m ≤ mΩ) (hf_int : Integrable f μ) :
+    [CompleteSpace F] (hf_int : Integrable f μ) :
     Integrable (fun ω => ‖∫ y, f y ∂condexpKernel μ m ω‖) μ := by
   rw [condexpKernel]
-  exact Integrable.norm_integral_condDistrib (aemeasurable_id'' μ hm) aemeasurable_id
-    (hf_int.comp_snd_map_prod_id hm)
+  exact Integrable.norm_integral_condDistrib
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
+    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
 #align measure_theory.integrable.norm_integral_condexp_kernel MeasureTheory.Integrable.norm_integral_condexpKernel
 
 theorem _root_.MeasureTheory.Integrable.integral_condexpKernel [NormedSpace ℝ F] [CompleteSpace F]
-    (hm : m ≤ mΩ) (hf_int : Integrable f μ) :
+    (hf_int : Integrable f μ) :
     Integrable (fun ω => ∫ y, f y ∂condexpKernel μ m ω) μ := by
   rw [condexpKernel]
-  exact Integrable.integral_condDistrib (aemeasurable_id'' μ hm) aemeasurable_id
-    (hf_int.comp_snd_map_prod_id hm)
+  exact Integrable.integral_condDistrib
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
+    (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
 #align measure_theory.integrable.integral_condexp_kernel MeasureTheory.Integrable.integral_condexpKernel
 
-theorem integrable_toReal_condexpKernel (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
+theorem integrable_toReal_condexpKernel {s : Set Ω} (hs : MeasurableSet s) :
     Integrable (fun ω => (condexpKernel μ m ω s).toReal) μ := by
   rw [condexpKernel]
-  exact integrable_toReal_condDistrib (aemeasurable_id'' μ hm) hs
+  exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs
 #align probability_theory.integrable_to_real_condexp_kernel ProbabilityTheory.integrable_toReal_condexpKernel
 
 end Integrability
 
+lemma condexpKernel_ae_eq_condexp' [IsFiniteMeasure μ] {s : Set Ω} (hs : MeasurableSet s) :
+    (fun ω ↦ (condexpKernel μ m ω s).toReal) =ᵐ[μ] μ⟦s | m ⊓ mΩ⟧ := by
+  have h := condDistrib_ae_eq_condexp (μ := μ)
+    (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
+  simp only [id_eq, ge_iff_le, MeasurableSpace.comap_id, preimage_id_eq] at h
+  simp_rw [condexpKernel_apply_eq_condDistrib]
+  exact h
+
+lemma condexpKernel_ae_eq_condexp [IsFiniteMeasure μ]
+    (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
+    (fun ω ↦ (condexpKernel μ m ω s).toReal) =ᵐ[μ] μ⟦s | m⟧ :=
+  (condexpKernel_ae_eq_condexp' hs).trans (by rw [inf_of_le_left hm])
+
+lemma condexpKernel_ae_eq_trim_condexp [IsFiniteMeasure μ]
+    (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
+    (fun ω ↦ (condexpKernel μ m ω s).toReal) =ᵐ[μ.trim hm] μ⟦s | m⟧ := by
+  rw [ae_eq_trim_iff hm _ stronglyMeasurable_condexp]
+  · exact condexpKernel_ae_eq_condexp hm hs
+  · refine Measurable.stronglyMeasurable ?_
+    exact @Measurable.ennreal_toReal _ m _ (measurable_condexpKernel hs)
+
+theorem condexp_ae_eq_integral_condexpKernel' [NormedAddCommGroup F] {f : Ω → F}
+    [NormedSpace ℝ F] [CompleteSpace F] (hf_int : Integrable f μ) :
+    μ[f|m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ y, f y ∂condexpKernel μ m ω := by
+  have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
+  simp_rw [condexpKernel_apply_eq_condDistrib]
+  have h := condexp_ae_eq_integral_condDistrib_id hX hf_int
+  simpa only [MeasurableSpace.comap_id, id_eq] using h
+
 /-- The conditional expectation of `f` with respect to a σ-algebra `m` is almost everywhere equal to
 the integral `∫ y, f y ∂(condexpKernel μ m ω)`. -/
-theorem condexp_ae_eq_integral_condexpKernel [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ)
-    (hf_int : Integrable f μ) : μ[f|m] =ᵐ[μ] fun ω => ∫ y, f y ∂condexpKernel μ m ω := by
-  have hX : @Measurable Ω Ω mΩ m id := measurable_id.mono le_rfl hm
-  rw [condexpKernel]
-  refine' EventuallyEq.trans _ (condexp_ae_eq_integral_condDistrib_id hX hf_int)
-  simp only [MeasurableSpace.comap_id, id.def]; rfl
+theorem condexp_ae_eq_integral_condexpKernel [NormedAddCommGroup F] {f : Ω → F}
+    [NormedSpace ℝ F] [CompleteSpace F] (hm : m ≤ mΩ) (hf_int : Integrable f μ) :
+    μ[f|m] =ᵐ[μ] fun ω => ∫ y, f y ∂condexpKernel μ m ω :=
+  ((condexp_ae_eq_integral_condexpKernel' hf_int).symm.trans (by rw [inf_of_le_left hm])).symm
 #align probability_theory.condexp_ae_eq_integral_condexp_kernel ProbabilityTheory.condexp_ae_eq_integral_condexpKernel
 
 end ProbabilityTheory