feat(probability/kernel/disintegration): disintegration of finite mea…

…sures on product spaces (#18834)

Disintegration of finite measures on `α × Ω`, where `Ω` is a standard Borel space.



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

src/measure_theory/constructions/prod/basic.lean

@@ -189,6 +189,35 @@ begin
   exact measurable_measure_prod_mk_right hs
 end
 
+lemma measurable_embedding.prod_mk {α β γ δ : Type*} {mα : measurable_space α}
+  {mβ : measurable_space β} {mγ : measurable_space γ} {mδ : measurable_space δ}
+  {f : α → β} {g : γ → δ} (hg : measurable_embedding g) (hf : measurable_embedding f) :
+  measurable_embedding (λ x : γ × α, (g x.1, f x.2)) :=
+begin
+  have h_inj : function.injective (λ x : γ × α, (g x.fst, f x.snd)),
+  { intros x y hxy,
+    rw [← @prod.mk.eta _ _ x, ← @prod.mk.eta _ _ y],
+    simp only [prod.mk.inj_iff] at hxy ⊢,
+    exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩, },
+  refine ⟨h_inj, _, _⟩,
+  { exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd), },
+  { -- Induction using the π-system of rectangles
+    refine λ s hs, @measurable_space.induction_on_inter _
+      (λ s, measurable_set ((λ (x : γ × α), (g x.fst, f x.snd)) '' s)) _ _ generate_from_prod.symm
+      is_pi_system_prod _ _ _ _ _ hs,
+    { simp only [set.image_empty, measurable_set.empty], },
+    { rintros t ⟨t₁, t₂, ht₁, ht₂, rfl⟩,
+      rw ← set.prod_image_image_eq,
+      exact (hg.measurable_set_image.mpr ht₁).prod (hf.measurable_set_image.mpr ht₂), },
+    { intros t ht ht_m,
+      rw [← set.range_diff_image h_inj, ← set.prod_range_range_eq],
+      exact measurable_set.diff
+        (measurable_set.prod hg.measurable_set_range hf.measurable_set_range) ht_m, },
+    { intros g hg_disj hg_meas hg,
+      simp_rw set.image_Union,
+      exact measurable_set.Union hg, }, },
+end
+
 /-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
   Tonelli's theorem is measurable. -/
 lemma measurable.lintegral_prod_right' [sigma_finite ν] :

src/probability/kernel/cond_cdf.lean

@@ -966,4 +966,49 @@ lemma integral_cond_cdf (ρ : measure (α × ℝ)) [is_finite_measure ρ] (x : 
   ∫ a, cond_cdf ρ a x ∂ρ.fst = (ρ (univ ×ˢ Iic x)).to_real :=
 by rw [← set_integral_cond_cdf ρ _ measurable_set.univ, measure.restrict_univ]
 
+section measure
+
+lemma measure_cond_cdf_Iic (ρ : measure (α × ℝ)) (a : α) (x : ℝ) :
+  (cond_cdf ρ a).measure (Iic x) = ennreal.of_real (cond_cdf ρ a x) :=
+begin
+  rw [← sub_zero (cond_cdf ρ a x)],
+  exact (cond_cdf ρ a).measure_Iic (tendsto_cond_cdf_at_bot ρ a) _,
+end
+
+lemma measure_cond_cdf_univ (ρ : measure (α × ℝ)) (a : α) :
+  (cond_cdf ρ a).measure univ = 1 :=
+begin
+  rw [← ennreal.of_real_one, ← sub_zero (1 : ℝ)],
+  exact stieltjes_function.measure_univ _ (tendsto_cond_cdf_at_bot ρ a)
+    (tendsto_cond_cdf_at_top ρ a),
+end
+
+instance (ρ : measure (α × ℝ)) (a : α) : is_probability_measure ((cond_cdf ρ a).measure) :=
+⟨measure_cond_cdf_univ ρ a⟩
+
+/-- The function `a ↦ (cond_cdf ρ a).measure` is measurable. -/
+lemma measurable_measure_cond_cdf (ρ : measure (α × ℝ)) :
+  measurable (λ a, (cond_cdf ρ a).measure) :=
+begin
+  rw measure.measurable_measure,
+  refine λ s hs, measurable_space.induction_on_inter
+    (borel_eq_generate_from_Iic ℝ) is_pi_system_Iic _ _ _ _ hs,
+  { simp only [measure_empty, measurable_const], },
+  { rintros S ⟨u, rfl⟩,
+    simp_rw measure_cond_cdf_Iic ρ _ u,
+    exact (measurable_cond_cdf ρ u).ennreal_of_real, },
+  { intros t ht ht_cd_meas,
+    have : (λ a, (cond_cdf ρ a).measure tᶜ)
+      = (λ a, (cond_cdf ρ a).measure univ) - (λ a, (cond_cdf ρ a).measure t),
+    { ext1 a,
+      rw [measure_compl ht (measure_ne_top (cond_cdf ρ a).measure _), pi.sub_apply], },
+    simp_rw [this, measure_cond_cdf_univ ρ],
+    exact measurable.sub measurable_const ht_cd_meas, },
+  { intros f hf_disj hf_meas hf_cd_meas,
+    simp_rw measure_Union hf_disj hf_meas,
+    exact measurable.ennreal_tsum hf_cd_meas, },
+end
+
+end measure
+
 end probability_theory