src/HOL/Probability/Levy.thy

--- a/src/HOL/Probability/Levy.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Probability/Levy.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -375,10 +375,10 @@
     have 3: "\<And>u v. integrable lborel (\<lambda>x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))"
       by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
                 continuous_intros ballI M'.isCont_char continuous_intros)
-    have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
+    have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> (LBINT t:{-d/2..d/2}. cmod (1 - char M' t))"
       unfolding set_lebesgue_integral_def
       using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
-    also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+    also have 4: "\<dots> \<le> (LBINT t:{-d/2..d/2}. \<epsilon> / 4)"
       unfolding set_lebesgue_integral_def
     proof (rule integral_mono [OF 3])