feat: port Probability.Kernel.Disintegration (#5289)

leanprover-community · Jun 20, 2023 · 88b496d · 88b496d
1 parent 9a53f9f
commit 88b496d
Show file tree

Hide file tree

Showing 3 changed files with 542 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2450,6 +2450,7 @@ import Mathlib.Probability.Integration
 import Mathlib.Probability.Kernel.Basic
 import Mathlib.Probability.Kernel.Composition
 import Mathlib.Probability.Kernel.CondCdf
+import Mathlib.Probability.Kernel.Disintegration
 import Mathlib.Probability.Kernel.IntegralCompProd
 import Mathlib.Probability.Kernel.Invariance
 import Mathlib.Probability.Kernel.MeasurableIntegral

diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean
@@ -991,7 +991,8 @@ theorem measure_condCdf_univ (ρ : Measure (α × ℝ)) (a : α) : (condCdf ρ a
   exact StieltjesFunction.measure_univ _ (tendsto_condCdf_atBot ρ a) (tendsto_condCdf_atTop ρ a)
 #align probability_theory.measure_cond_cdf_univ ProbabilityTheory.measure_condCdf_univ
 
-instance (ρ : Measure (α × ℝ)) (a : α) : IsProbabilityMeasure (condCdf ρ a).measure :=
+instance instIsProbabilityMeasure (ρ : Measure (α × ℝ)) (a : α) :
+    IsProbabilityMeasure (condCdf ρ a).measure :=
   ⟨measure_condCdf_univ ρ a⟩
 
 /-- The function `a ↦ (condCdf ρ a).measure` is measurable. -/