--- a/src/HOL/Probability/Conditional_Expectation.thy Tue Feb 06 15:29:10 2024 +0000
+++ b/src/HOL/Probability/Conditional_Expectation.thy Wed Feb 07 11:52:34 2024 +0000
@@ -1145,9 +1145,9 @@
unfolding phi_def proof (rule cInf_greatest, auto)
fix t assume "t \<in> I" "y < t"
have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)"
- apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
+ apply (rule convex_on_slope_le[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
also have "... \<le> (q y - q t) / (y - t)"
- apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
+ apply (rule convex_on_slope_le[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp
next
obtain e where "0 < e" "ball y e \<subseteq> I" using \<open>open I\<close> \<open>y \<in> I\<close> openE by blast