--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Aug 24 20:26:02 2025 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Aug 25 12:44:36 2025 +0100
@@ -512,7 +512,7 @@
subsection\<^marker>\<open>tag unimportant\<close>\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
lemma vec_cbox_1_eq [simp]:
- shows "vec ` cbox u v = cbox (vec u) (vec v ::real^1)"
+ shows "vec ` {u..v} = cbox (vec u) (vec v ::real^1)"
by (force simp: Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
lemma vec_nth_cbox_1_eq [simp]:
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Aug 24 20:26:02 2025 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Aug 25 12:44:36 2025 +0100
@@ -2487,7 +2487,7 @@
also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> snd ` p. norm (integral (i\<inter>l) f))"
by (simp add: sum.cartesian_product)
also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod (\<inter>) x) f))"
- by (force simp: split_def intro!: sum.cong)
+ by (simp add: split_def)
also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
proof -
have eq0: " (integral (l1 \<inter> k1) f) = 0"
@@ -2606,7 +2606,7 @@
unfolding sum_distrib_right[symmetric] using uv by auto
qed
show ?thesis
- by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
+ by (auto simp add: sumeq p' d' simp flip: sum_Sigma_product intro!: sum.cong)
qed
finally show ?thesis .
qed
@@ -2714,10 +2714,9 @@
show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
using d1[OF p(1,2)] by (simp only: real_norm_def)
show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
- by (auto simp: split_paired_all sum.cong [OF refl])
+ by simp
have "(\<Sum>(x,k) \<in> p. norm (integral k f)) = (\<Sum>k\<in>snd ` p. norm (integral k f))"
- apply (rule sum.over_tagged_division_lemma[OF p(1)])
- by (metis Henstock_Kurzweil_Integration.integral_empty integral_open_interval norm_zero)
+ by (simp add: sum_content.box_empty_imp sum.over_tagged_division_lemma[OF p(1)])
also have "... \<le> SDF"
using partial_division_of_tagged_division[of p "cbox a b"] p(1)
by (auto simp: SDF_def tagged_partial_division_of_def intro!: cSUP_upper2 D_1 D_2)
@@ -2850,8 +2849,11 @@
using t by auto
finally have eq1: "?\<mu> (\<Union>\<F>) = (\<Sum>x\<in>\<F>. content x * indicator S (t x))" .
have eq2: "(\<Sum>K\<in>\<F>. ?\<mu> (K \<inter> S)) = (\<Sum>K\<in>\<F>. integral K (indicator S))"
- apply (rule sum.cong [OF refl])
- by (metis integral_indicator \<F>div \<open>S \<in> lmeasurable\<close> division_ofD(4) fmeasurable.Int inf.commute lmeasurable_cbox)
+ proof (rule sum.cong [OF refl])
+ show "\<And>x. x \<in> \<F> \<Longrightarrow> measure lebesgue (x \<inter> S) = integral x (indicat_real S)"
+ by (metis integral_indicator \<F>div \<open>S \<in> lmeasurable\<close> division_ofD(4) fmeasurable.Int
+ inf.commute lmeasurable_cbox)
+ qed
have "\<bar>\<Sum>(x,K)\<in>(\<lambda>K. (t K, K)) ` \<F>. content K * indicator S x - integral K (indicator S)\<bar> \<le> e"
using Henstock_lemma_part1 [of "indicator S::'a\<Rightarrow>real", OF _ \<open>e > 0\<close> \<open>gauge \<gamma>\<close> _ tagged fine]
indS_int norme by auto
@@ -3482,15 +3484,15 @@
fix x
have "(\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. ((f x \<bullet> i + g x \<bullet> i + \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) / 2) *\<^sub>R i)"
by (force intro: sum.cong)
- also have "... = (1 / 2) *\<^sub>R (\<Sum>i\<in>Basis. (f x \<bullet> i + g x \<bullet> i + \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) *\<^sub>R i)"
+ also have "... = (1/2) *\<^sub>R (\<Sum>i\<in>Basis. (f x \<bullet> i + g x \<bullet> i + \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) *\<^sub>R i)"
by (simp add: scaleR_right.sum)
- also have "... = (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))"
+ also have "... = (1/2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))"
by (simp add: sum.distrib algebra_simps euclidean_representation)
finally
show "(\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
- (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
+ (1/2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
qed
- moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
+ moreover have "(\<lambda>x. (1/2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
absolutely_integrable_on S"
using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
by (intro set_integral_add absolutely_integrable_scaleR_left assms) (simp add: algebra_simps)
@@ -3506,8 +3508,7 @@
lemma absolutely_integrable_min:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
- shows "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
- absolutely_integrable_on S"
+ shows "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) absolutely_integrable_on S"
proof -
have "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
(\<lambda>x. (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
@@ -3515,15 +3516,15 @@
fix x
have "(\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. ((f x \<bullet> i + g x \<bullet> i - \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) / 2) *\<^sub>R i)"
by (force intro: sum.cong)
- also have "... = (1 / 2) *\<^sub>R (\<Sum>i\<in>Basis. (f x \<bullet> i + g x \<bullet> i - \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) *\<^sub>R i)"
+ also have "... = (1/2) *\<^sub>R (\<Sum>i\<in>Basis. (f x \<bullet> i + g x \<bullet> i - \<bar>f x \<bullet> i - g x \<bullet> i\<bar>) *\<^sub>R i)"
by (simp add: scaleR_right.sum)
- also have "... = (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))"
+ also have "... = (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))"
by (simp add: sum.distrib sum_subtractf algebra_simps euclidean_representation)
finally
show "(\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
- (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
+ (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
qed
- moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
+ moreover have "(\<lambda>x. (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
absolutely_integrable_on S"
using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
by (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
@@ -3626,7 +3627,6 @@
proof (rule has_integral_twiddle)
show "\<exists>w z::real^1. vec ` cbox u v = cbox w z"
"content (vec ` cbox u v :: (real^1) set) = 1 * content (cbox u v)" for u v
- unfolding vec_cbox_1_eq
by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
show "\<exists>w z. (\<lambda>x. x $ 1) ` cbox u v = cbox w z" for u v :: "real^1"
using vec_nth_cbox_1_eq by blast
@@ -3673,12 +3673,10 @@
proof (rule has_integral_twiddle)
show "\<exists>w z::real. (\<lambda>x. x $ 1) ` cbox u v = cbox w z"
"content ((\<lambda>x. x $ 1) ` cbox u v) = 1 * content (cbox u v)" for u v::"real^1"
- unfolding vec_cbox_1_eq by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
- show "\<exists>w z::real^1. vec ` cbox u v = cbox w z" for u v :: "real"
- using vec_cbox_1_eq by auto
+ by (auto simp: content_cbox_if_cart interval_eq_empty_cart)
qed (auto simp: continuous_vec assms)
then show ?thesis
- using vec_cbox_1_eq by auto
+ by auto
qed
lemma has_integral_vec1_D_cbox:
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 24 20:26:02 2025 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Aug 25 12:44:36 2025 +0100
@@ -140,7 +140,8 @@
using ab by (intro emeasure_mono) auto
then show ?thesis
using \<open>content (box a b) > 0\<close>
- by (smt (verit, best) Sigma_Algebra.measure_def emeasure_lborel_ball_finite enn2real_mono infinity_ennreal_def)
+ by (metis Sigma_Algebra.measure_def emeasure_lborel_ball_finite enn2real_positive_iff
+ infinity_ennreal_def le_zero_eq not_gr_zero)
qed
lemma content_cball_pos:
@@ -286,7 +287,7 @@
"(f has_integral y) (cbox a b) \<longleftrightarrow>
(\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
(\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
- norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
+ norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - y) < e))"
by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)
lemma has_integral_real:
@@ -1369,11 +1370,12 @@
using mem_interior by metis
have x: "x\<bullet>k = c"
using x interior_subset by fastforce
- have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon>/2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
- using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon>/2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
(\<Sum>i\<in>Basis. (if i = k then \<epsilon>/2 else 0))"
- using "*" by (blast intro: sum.cong)
+ proof (rule sum.cong [OF refl])
+ show "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon>/2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
+ using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_not_same_Basis)
+ qed
also have "\<dots> < \<epsilon>"
by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
finally have "x + (\<epsilon>/2) *\<^sub>R k \<in> ball x \<epsilon>"
@@ -1957,9 +1959,8 @@
have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)"
by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
- using k *
- by (intro prod_zero bexI[OF _ k])
- (auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong)
+ using k * unfolding b'_def a'_def
+ by (auto simp: inner_diff intro!: prod_zero sum.cong)
also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
proof (intro tendsto_cong eventually_at_rightI)
@@ -2055,7 +2056,7 @@
by (metis inf.orderE)
qed
then have *: "(\<Sum>(x,K)\<in>\<D>. content K * ?i x) = (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
- by (force simp add: split_paired_all intro!: sum.cong [OF refl])
+ by (force simp: split_paired_all intro!: sum.cong [OF refl])
note p'= tagged_division_ofD[OF p(1)] and p''=division_of_tagged_division[OF p(1)]
have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
proof -
--- a/src/HOL/Filter.thy Sun Aug 24 20:26:02 2025 +0200
+++ b/src/HOL/Filter.thy Mon Aug 25 12:44:36 2025 +0100
@@ -1911,7 +1911,8 @@
lemma eventually_parametric [transfer_rule]:
"((A ===> (=)) ===> rel_filter A ===> (=)) eventually eventually"
-by(auto 4 4 intro!: rel_funI elim!: rel_filter.cases simp add: eventually_map_filter_on dest: rel_funD intro: always_eventually elim!: eventually_rev_mp)
+ unfolding rel_fun_def
+ by(force elim!: rel_filter.cases eventually_rev_mp simp add: eventually_map_filter_on intro: always_eventually)
lemma frequently_parametric [transfer_rule]: "((A ===> (=)) ===> rel_filter A ===> (=)) frequently frequently"
unfolding frequently_def[abs_def] by transfer_prover