# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1707924825 0
# Node ID 2c18ac57e92e59002b2e5a314b8f028a6edec109
# Parent  66cbd1ef0db19ef4a3b383373d05f8acec99273c
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses

diff -r 66cbd1ef0db1 -r 2c18ac57e92e NEWS
--- a/NEWS	Tue Feb 13 17:18:57 2024 +0000
+++ b/NEWS	Wed Feb 14 15:33:45 2024 +0000
@@ -25,6 +25,9 @@
   by Sledgehammer and should be used instead. For more information, see
   Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY.
 
+* HOL-Analysis: the syntax of Lebesgue integrals (LINT, LBINT, \<integral>, etc.) now
+  requires parentheses in most cases. INCOMPATIBILITY.
+
 * HOL-Analysis: corrected the definition of convex function (convex_on)
   to require the underlying set to be convex. INCOMPATIBILITY.
 
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -1503,7 +1503,7 @@
     proof (intro nn_integral_mono_AE, eventually_elim)
       fix x assume "\<forall>i. norm (s i x) \<le> w x" "(\<lambda>i. s i x) \<longlonglongrightarrow> f x" "0 \<le> w x"
       then show "ennreal (norm (f x)) \<le> ennreal (w x)"
-        by (intro LIMSEQ_le_const2[where X="\<lambda>i. ennreal (norm (s i x))"]) (auto intro: tendsto_intros)
+        by (metis LIMSEQ_le_const2 ennreal_leI tendsto_norm)
     qed
     with w show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by auto
   qed fact
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -927,10 +927,10 @@
 lemma set_borel_integral_eq_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "set_integrable lborel S f"
-  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
+  shows "f integrable_on S" "(LINT x : S | lborel. f x) = integral S f"
 proof -
   let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
-  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
+  have "(?f has_integral (LINT x : S | lborel. f x)) UNIV"
     using assms has_integral_integral_lborel
     unfolding set_integrable_def set_lebesgue_integral_def by blast
   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
@@ -939,7 +939,7 @@
     by (auto simp add: integrable_on_def)
   with 1 have "(f has_integral (integral S f)) S"
     by (intro integrable_integral, auto simp add: integrable_on_def)
-  thus "LINT x : S | lborel. f x = integral S f"
+  thus "(LINT x : S | lborel. f x) = integral S f"
     by (intro has_integral_unique [OF 1])
 qed
 
@@ -954,7 +954,7 @@
 lemma set_lebesgue_integral_eq_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "set_integrable lebesgue S f"
-  shows "f integrable_on S" "LINT x:S | lebesgue. f x = integral S f"
+  shows "f integrable_on S" "(LINT x:S | lebesgue. f x) = integral S f"
   using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)
 
 lemma lmeasurable_iff_has_integral:
@@ -2184,7 +2184,7 @@
 
 lemma set_integral_norm_bound:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
+  shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> (LINT x:k|M. norm (f x))"
   using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by (simp add: set_lebesgue_integral_def)
 
 lemma set_integral_finite_UN_AE:
@@ -2193,7 +2193,7 @@
     and ae: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> AE x in M. (x \<in> A i \<and> x \<in> A j) \<longrightarrow> i = j"
     and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
     and f: "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f"
-  shows "LINT x:(\<Union>i\<in>I. A i)|M. f x = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
+  shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   using \<open>finite I\<close> order_refl[of I]
 proof (induction I rule: finite_subset_induct')
   case (insert i I')
@@ -4000,7 +4000,7 @@
             =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
 proof-
   have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) 
-      = LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x"
+      = (LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x)"
     by (meson vector_space_over_itself.scale_left_distrib)
   also have "... = (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
   proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros)
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Analysis/Interval_Integral.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -290,7 +290,7 @@
              split: if_split_asm)
 next
   case (le a b) 
-  have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
+  have "(LBINT x:{x. - x \<in> einterval a b}. f (- x)) = (LBINT x:einterval (- b) (- a). f (- x))"
     unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def einterval_def
     by (metis (lifting) ereal_less_uminus_reorder ereal_uminus_less_reorder indicator_simps mem_Collect_eq uminus_ereal.simps(1))
   then show ?case
@@ -315,13 +315,13 @@
 
 lemma interval_integral_zero [simp]:
   fixes a b :: ereal
-  shows "LBINT x=a..b. 0 = 0"
+  shows "(LBINT x=a..b. 0) = 0"
 unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq
 by simp
 
 lemma interval_integral_const [intro, simp]:
   fixes a b c :: real
-  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
+  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "(LBINT x=a..b. c) = c * (b - a)"
   unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
   by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
 
@@ -780,7 +780,7 @@
   and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
   and contf : "continuous_on (g ` {a..b}) f"
   and contg': "continuous_on {a..b} g'"
-  shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
+  shows "(LBINT x=a..b. g' x *\<^sub>R f (g x)) = (LBINT y=g a..g b. f y)"
 proof-
   have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
     using derivg unfolding has_real_derivative_iff_has_vector_derivative .
@@ -798,7 +798,7 @@
     by (blast intro: continuous_on_compose2 contf contg)
   have "continuous_on {a..b} (\<lambda>x. g' x *\<^sub>R f (g x))"
     by (auto intro!: continuous_on_scaleR contg' contfg)
-  then have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+  then have "(LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x)) = F (g b) - F (g a)"
     using integral_FTC_atLeastAtMost [OF \<open>a \<le> b\<close> vector_diff_chain_within[OF v_derivg derivF]]
     by force
   then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -78,12 +78,12 @@
             using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
             by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
         hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) =
-                   LBINT x:{a..b} \<inter> g-`{u..v}. g' x"
+                   (LBINT x:{a..b} \<inter> g-`{u..v}. g' x)"
           unfolding set_lebesgue_integral_def
           by (subst nn_integral_eq_integral[symmetric])
              (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
         also from interval_integral_FTC_finite[OF A B]
-            have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
+            have "(LBINT x:{a..b} \<inter> g-`{u..v}. g' x) = v - u"
                 by (simp add: u'v' interval_integral_Icc \<open>u \<le> v\<close>)
         finally have "(\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
                            ennreal (v - u)" .
@@ -130,12 +130,12 @@
           (simp split: split_indicator)
       also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
         by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
-      also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
+      also have "g b - g a = (LBINT x:{a..b}. g' x)" using derivg'
         unfolding set_lebesgue_integral_def
         by (intro integral_FTC_atLeastAtMost[symmetric])
            (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
                  has_vector_derivative_at_within)
-      also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
+      also have "ennreal ... = (\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel)"
         using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
         by (subst nn_integral_eq_integral)
            (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
@@ -341,7 +341,7 @@
   from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
     by (force simp: mult.commute set_integrable_def)
 
-  have "LBINT x. (f x :: real) * indicator {g a..g b} x =
+  have "(LBINT x. (f x :: real) * indicator {g a..g b} x) =
           enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
           enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
     unfolding set_integrable_def
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Analysis/Set_Integral.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -23,7 +23,7 @@
 
 syntax
   "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
+  ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 10)
 
 translations
   "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
@@ -39,11 +39,11 @@
 
 syntax
   "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-  ("(2LBINT _./ _)" [0,60] 60)
+  ("(2LBINT _./ _)" [0,60] 10)
 
 syntax
   "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-  ("(3LBINT _:_./ _)" [0,60,61] 60)
+  ("(3LBINT _:_./ _)" [0,60,61] 10)
 
 (*
     Basic properties
@@ -105,7 +105,7 @@
 lemma set_lebesgue_integral_cong_AE:
   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assumes "AE x \<in> A in M. f x = g x"
-  shows "LINT x:A|M. f x = LINT x:A|M. g x"
+  shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
 proof-
   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
     using assms by auto
@@ -149,25 +149,25 @@
 (* TODO: integral_cmul_indicator should be named set_integral_const *)
 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
 
-lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
+lemma set_integral_scaleR_right [simp]: "(LINT t:A|M. a *\<^sub>R f t) = a *\<^sub>R (LINT t:A|M. f t)"
   unfolding set_lebesgue_integral_def
   by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
 
 lemma set_integral_mult_right [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
-  shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
+  shows "(LINT t:A|M. a * f t) = a * (LINT t:A|M. f t)"
   unfolding set_lebesgue_integral_def
   by (subst integral_mult_right_zero[symmetric]) auto
 
 lemma set_integral_mult_left [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
-  shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
+  shows "(LINT t:A|M. f t * a) = (LINT t:A|M. f t) * a"
   unfolding set_lebesgue_integral_def
   by (subst integral_mult_left_zero[symmetric]) auto
 
 lemma set_integral_divide_zero [simp]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
-  shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
+  shows "(LINT t:A|M. f t / a) = (LINT t:A|M. f t) / a"
   unfolding set_lebesgue_integral_def
   by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
      (auto split: split_indicator)
@@ -236,21 +236,20 @@
   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "set_integrable M A f" "set_integrable M A g"
   shows "set_integrable M A (\<lambda>x. f x + g x)"
-    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
+    and "(LINT x:A|M. f x + g x) = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
   using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
 
 lemma set_integral_diff [simp, intro]:
   assumes "set_integrable M A f" "set_integrable M A g"
-  shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
-    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
+  shows "set_integrable M A (\<lambda>x. f x - g x)" and "(LINT x:A|M. f x - g x) = (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
 
-lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
+lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> (LINT x:A|M. - f x) = - (LINT x:A|M. f x)"
   unfolding set_integrable_def set_lebesgue_integral_def
   by (subst integral_minus[symmetric]) simp_all
 
 lemma set_integral_complex_of_real:
-  "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
+  "(LINT x:A|M. complex_of_real (f x)) = of_real (LINT x:A|M. f x)"
   unfolding set_lebesgue_integral_def
   by (subst integral_complex_of_real[symmetric])
      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
@@ -341,7 +340,7 @@
   assumes "A \<inter> B = {}"
   and "set_integrable M A f"
   and "set_integrable M B f"
-shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+shows "(LINT x:A\<union>B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   using assms
   unfolding set_integrable_def set_lebesgue_integral_def
   by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
@@ -350,7 +349,7 @@
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
-  shows "LINT x:B|M. f x = LINT x:A|M. f x"
+  shows "(LINT x:B|M. f x) = (LINT x:A|M. f x)"
   unfolding set_lebesgue_integral_def
 proof (rule integral_cong_AE)
   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
@@ -376,13 +375,13 @@
   assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
   and "set_integrable M A f"
   and "set_integrable M B f"
-  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+  shows "(LINT x:A\<union>B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
 proof -
   have f: "set_integrable M (A \<union> B) f"
     by (intro set_integrable_Un assms)
   then have f': "set_borel_measurable M (A \<union> B) f"
     using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
-  have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
+  have "(LINT x:A\<union>B|M. f x) = (LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x)"
   proof (rule set_integral_cong_set)
     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
       using ae by auto
@@ -420,11 +419,11 @@
   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
 shows "set_integrable M (\<Union>i. A i) f"
-    unfolding set_integrable_def
+  unfolding set_integrable_def
   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
-  apply (rule intgbl [unfolded set_integrable_def])
-  prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
-  apply (rule AE_I2)
+      apply (rule intgbl [unfolded set_integrable_def])
+     prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
+    apply (rule AE_I2)
   using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
 proof (rule AE_I2)
   { fix x assume "x \<in> space M"
@@ -432,18 +431,16 @@
     proof cases
       assume "\<exists>i. x \<in> A i"
       then obtain i where "x \<in> A i" ..
-      then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
+      then have "\<forall>\<^sub>F i in sequentially. x \<in> A i"
         using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
-      show ?thesis
-        apply (intro tendsto_eventually)
-        using *
-        apply eventually_elim
-        apply (auto split: split_indicator)
-        done
+      with eventually_mono have "\<forall>\<^sub>F i in sequentially. indicat_real (A i) x *\<^sub>R f x = indicat_real (\<Union> (range A)) x *\<^sub>R f x"
+        by fastforce
+      then show ?thesis
+        by (intro tendsto_eventually)
     qed auto }
   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
     apply (rule borel_measurable_LIMSEQ_real)
-    apply assumption
+     apply assumption
     using intgbl set_integrable_def by blast
 qed
 
@@ -453,7 +450,7 @@
   assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
     and intgbl: "set_integrable M (\<Union>i. A i) f"
-  shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
+  shows "(LINT x:(\<Union>i. A i)|M. f x) = (\<Sum>i. (LINT x:(A i)|M. f x))"
     unfolding set_lebesgue_integral_def
 proof (subst integral_suminf[symmetric])
   show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
@@ -503,7 +500,7 @@
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
   and intgbl: "set_integrable M (\<Union>i. A i) f"
-shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> (LINT x:(\<Union>i. A i)|M. f x)"
   unfolding set_lebesgue_integral_def
 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
   have int_A: "\<And>i. set_integrable M (A i) f"
@@ -528,7 +525,7 @@
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
   and int0: "set_integrable M (A 0) f"
-  shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
+  shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> (LINT x:(\<Inter>i. A i)|M. f x)"
   unfolding set_lebesgue_integral_def
 proof (rule integral_dominated_convergence)
   have int_A: "\<And>i. set_integrable M (A i) f"
@@ -580,7 +577,7 @@
 
 syntax
   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-  ("(3CLINT _|_. _)" [0,110,60] 60)
+  ("(3CLINT _|_. _)" [0,110,60] 10)
 
 translations
   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
@@ -614,7 +611,7 @@
 
 syntax
 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4CLINT _:_|_. _)" [0,60,110,61] 60)
+("(4CLINT _:_|_. _)" [0,60,110,61] 10)
 
 translations
 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
@@ -633,10 +630,10 @@
 
 syntax
 "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
+("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 10)
 
 "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
+("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 10)
 
 translations
 "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -56,8 +56,7 @@
 
 definition
   char :: "real measure \<Rightarrow> real \<Rightarrow> complex"
-where
-  "char M t = CLINT x|M. iexp (t * x)"
+  where "char M t \<equiv> CLINT x|M. iexp (t * x)"
 
 lemma (in real_distribution) char_zero: "char M 0 = 1"
   unfolding char_def by (simp del: space_eq_univ add: prob_space)
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Probability/Conditional_Expectation.thy
--- a/src/HOL/Probability/Conditional_Expectation.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -355,13 +355,13 @@
 
   fix A assume "A \<in> sets F"
   then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
-  have "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M"
+  have "(\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M) = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M"
     by (simp add: mult.commute mult.left_commute)
   also have "... = \<integral>\<^sup>+x. (f x * indicator A x) * nn_cond_exp M F g x \<partial>M"
     by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
-  also have "... = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M"
+  also have "... = (\<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M)"
     by (simp add: mult.commute mult.left_commute)
-  finally show "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M" by simp
+  finally show "(\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M) = (\<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M)" by simp
 qed (auto simp add: assms)
 
 lemma nn_cond_exp_sum:
@@ -370,7 +370,7 @@
 proof (rule nn_cond_exp_charact)
   fix A assume [measurable]: "A \<in> sets F"
   then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
-  have "\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)"
+  have "(\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M) = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)"
     by (rule nn_set_integral_add) (auto simp add: assms \<open>A \<in> sets M\<close>)
   also have "... = (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F g x \<partial>M)"
     by (metis (no_types, lifting) mult.commute nn_integral_cong)
@@ -378,9 +378,9 @@
     by (simp add: nn_cond_exp_intg)
   also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)"
     by (metis (no_types, lifting) mult.commute nn_integral_cong)
-  also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M"
+  also have "... = (\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M)"
     by (rule nn_set_integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close>)
-  finally show "\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M = \<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M"
+  finally show "(\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M) = (\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M)"
     by simp
 qed (auto simp add: assms)
 
@@ -390,12 +390,12 @@
   shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x"
 proof (rule nn_cond_exp_charact)
   fix A assume [measurable]: "A \<in> sets F"
-  have "\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M = \<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M"
+  have "(\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) = \<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M"
     by (simp add: mult.commute)
   also have "... = \<integral>\<^sup>+x. indicator A x * f x \<partial>M" by (simp add: nn_cond_exp_intg assms)
-  also have "... = \<integral>\<^sup>+x\<in>A. f x \<partial>M" by (simp add: mult.commute)
-  also have "... = \<integral>\<^sup>+x\<in>A. g x \<partial>M" by (rule nn_set_integral_cong[OF assms(1)])
-  finally show "\<integral>\<^sup>+x\<in>A. g x \<partial>M = \<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M" by simp
+  also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M)" by (simp add: mult.commute)
+  also have "... = (\<integral>\<^sup>+x\<in>A. g x \<partial>M)" by (rule nn_set_integral_cong[OF assms(1)])
+  finally show "(\<integral>\<^sup>+x\<in>A. g x \<partial>M) = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M)" by simp
 qed (auto simp add: assms)
 
 lemma nn_cond_exp_mono:
@@ -791,14 +791,14 @@
   fix A assume "A \<in> sets F"
   then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
   have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
-  have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
+  have "(\<integral>x\<in>A. (f x * g x) \<partial>M) = \<integral>x. (f x * indicator A x) * g x \<partial>M"
     by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
   also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
     apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
-  also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
+  also have "... = (\<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M)"
     by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
-  finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
+  finally show "(\<integral>x\<in>A. (f x * g x) \<partial>M) = (\<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M)" by simp
 qed (auto simp add: real_cond_exp_intg(1) assms)
 
 lemma real_cond_exp_add [intro]:
@@ -817,7 +817,7 @@
   have intAg: "integrable M (\<lambda>x. indicator A x * g x)"
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
 
-  have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
+  have "(\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
     apply (rule set_integral_add, auto simp add: assms set_integrable_def)
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
           integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
@@ -827,9 +827,9 @@
     using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
   also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
     unfolding set_lebesgue_integral_def by auto
-  also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
+  also have "... = (\<integral>x\<in>A. (f x + g x)\<partial>M)"
     by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def \<open>A \<in> sets M\<close> intAf intAg)
-  finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
+  finally show "(\<integral>x\<in>A. (f x + g x)\<partial>M) = (\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M)"
     by simp
 qed (auto simp add: assms)
 
diff -r 66cbd1ef0db1 -r 2c18ac57e92e 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])
 
diff -r 66cbd1ef0db1 -r 2c18ac57e92e src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Probability/Sinc_Integral.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -216,7 +216,7 @@
     using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
     by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
 
-  have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
+  have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> (LBINT x::real:{0<..}. 0)) at_top"
     unfolding set_lebesgue_integral_def
   proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]], 
          simp_all del: abs_divide split: split_indicator)
@@ -278,23 +278,23 @@
     have "Si t = LBINT x=0..t. sin x * (LBINT u=0..\<infinity>. exp (-(u * x)))"
       unfolding Si_def using \<open>0 \<le> t\<close>
       by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
-    also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
+    also have "\<dots> = (LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x))))"
       using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def)
-    also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
+    also have "\<dots> = (LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x)))))"
       apply (subst interval_integral_Ioi)
       unfolding set_lebesgue_integral_def  by(simp_all add: indicator_times ac_simps )
-    also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
+    also have "\<dots> = (LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x)))))"
     proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
       show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
           \<in> borel_measurable (lborel \<Otimes>\<^sub>M lborel)" (is "?f \<in> borel_measurable _")
         by measurable
 
-      have "AE x in lborel. indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
+      have "AE x in lborel. indicator {0..t} x *\<^sub>R abs (sinc x) = (LBINT y. norm (?f (x, y)))"
         using AE_lborel_singleton[of 0] AE_lborel_singleton[of t]
       proof eventually_elim
         fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
-        have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> =
-            LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
+        have "(LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar>) =
+              (LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x)"
           by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
         also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
           by (cases "x > 0")
@@ -303,7 +303,7 @@
           by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
         also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
           using x by (simp add: field_simps split: split_indicator)
-        finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
+        finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = (LBINT y. norm (?f (x, y)))"
           by simp
       qed
       moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)"
@@ -316,11 +316,11 @@
       then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
         by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator)
     qed
-    also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
+    also have "... = (LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x))"
       using \<open>0\<le>t\<close>
       by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps
                split: split_indicator intro!: Bochner_Integration.integral_cong)
-    also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
+    also have "\<dots> = (LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t)))"
       by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
     also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"
       using Si_at_top_integrable[OF \<open>0\<le>t\<close>] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square)
@@ -371,8 +371,7 @@
       by (rule interval_integral_discrete_difference[of "{0}"]) auto
     finally have "(LBINT t=ereal 0..T. sin (t * \<theta>) / t) = (LBINT t=ereal 0..T * \<theta>. sin t / t)"
       by simp
-    hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
-        LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
+    hence "(LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x) = (LBINT x. indicator {0<..<T * \<theta>} x * sin x / x)"
       using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
         by (auto simp: ac_simps set_lebesgue_integral_def)
   } note aux1 = this
@@ -390,7 +389,7 @@
       by (rule interval_integral_discrete_difference[of "{0}"]) auto
     finally have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T * -\<theta>. sin t / t)"
       by simp
-    hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
+    hence "(LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x) =
        - (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
       using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
         by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm)