--- 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.
--- 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
--- 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)
--- 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)"
--- 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
--- 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)"
--- 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)
--- 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)
--- 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])
--- 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)