--- a/src/HOL/Analysis/Affine.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Affine.thy Sat Aug 12 10:09:29 2023 +0100
@@ -5,7 +5,7 @@
begin
lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)"
- by (fact if_distrib)
+ by simp
lemma sum_delta_notmem:
assumes "x \<notin> s"
@@ -13,12 +13,7 @@
and "sum (\<lambda>y. if (x = y) then P x else Q y) s = sum Q s"
and "sum (\<lambda>y. if (y = x) then P y else Q y) s = sum Q s"
and "sum (\<lambda>y. if (x = y) then P y else Q y) s = sum Q s"
- apply (rule_tac [!] sum.cong)
- using assms
- apply auto
- done
-
-lemmas independent_finite = independent_imp_finite
+ by (smt (verit, best) assms sum.cong)+
lemma span_substd_basis:
assumes d: "d \<subseteq> Basis"
@@ -32,13 +27,11 @@
ultimately have "span d \<subseteq> ?B"
using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast
moreover have *: "card d \<le> dim (span d)"
- using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms]
- span_superset[of d]
- by auto
+ by (simp add: d dim_eq_card_independent independent_substdbasis)
moreover from * have "dim ?B \<le> dim (span d)"
using dim_substandard[OF assms] by auto
ultimately show ?thesis
- using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto
+ by (simp add: s subspace_dim_equal)
qed
lemma basis_to_substdbasis_subspace_isomorphism:
@@ -51,7 +44,8 @@
using dim_unique[of B B "card B"] assms span_superset[of B] by auto
have "dim B \<le> card (Basis :: 'a set)"
using dim_subset_UNIV[of B] by simp
- from obtain_subset_with_card_n[OF this] obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
+ from obtain_subset_with_card_n[OF this]
+ obtain d :: "'a set" where d: "d \<subseteq> Basis" and t: "card d = dim B"
by auto
let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
@@ -65,9 +59,9 @@
subsection \<open>Affine set and affine hull\<close>
definition\<^marker>\<open>tag important\<close> affine :: "'a::real_vector set \<Rightarrow> bool"
- where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
+ where "affine S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> S)"
-lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
+lemma affine_alt: "affine S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S)"
unfolding affine_def by (metis eq_diff_eq')
lemma affine_empty [iff]: "affine {}"
@@ -79,21 +73,21 @@
lemma affine_UNIV [iff]: "affine UNIV"
unfolding affine_def by auto
-lemma affine_Inter [intro]: "(\<And>s. s\<in>f \<Longrightarrow> affine s) \<Longrightarrow> affine (\<Inter>f)"
+lemma affine_Inter [intro]: "(\<And>S. S\<in>\<F> \<Longrightarrow> affine S) \<Longrightarrow> affine (\<Inter>\<F>)"
unfolding affine_def by auto
-lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
+lemma affine_Int[intro]: "affine S \<Longrightarrow> affine T \<Longrightarrow> affine (S \<inter> T)"
unfolding affine_def by auto
-lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
- apply (clarsimp simp add: affine_def)
+lemma affine_scaling: "affine S \<Longrightarrow> affine ((*\<^sub>R) c ` S)"
+ apply (clarsimp simp: affine_def)
apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
apply (auto simp: algebra_simps)
done
-lemma affine_affine_hull [simp]: "affine(affine hull s)"
+lemma affine_affine_hull [simp]: "affine(affine hull S)"
unfolding hull_def
- using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
+ using affine_Inter[of "{T. affine T \<and> S \<subseteq> T}"] by auto
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
by (metis affine_affine_hull hull_same)
@@ -198,6 +192,8 @@
"affine hull p = {y. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
(is "_ = ?rhs")
proof (rule hull_unique)
+ have "\<And>x. sum (\<lambda>z. 1) {x} = 1"
+ by auto
show "p \<subseteq> ?rhs"
proof (intro subsetI CollectI exI conjI)
show "\<And>x. sum (\<lambda>z. 1) {x} = 1"
@@ -452,31 +448,16 @@
unfolding affine_parallel_def
using image_add_0 by blast
-lemma affine_parallel_commut:
+lemma affine_parallel_commute:
assumes "affine_parallel A B"
shows "affine_parallel B A"
-proof -
- from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
- unfolding affine_parallel_def by auto
- have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
- from B show ?thesis
- using translation_galois [of B a A]
- unfolding affine_parallel_def by blast
-qed
+ by (metis affine_parallel_def assms translation_galois)
lemma affine_parallel_assoc:
assumes "affine_parallel A B"
and "affine_parallel B C"
shows "affine_parallel A C"
-proof -
- from assms obtain ab where "B = (\<lambda>x. ab + x) ` A"
- unfolding affine_parallel_def by auto
- moreover
- from assms obtain bc where "C = (\<lambda>x. bc + x) ` B"
- unfolding affine_parallel_def by auto
- ultimately show ?thesis
- using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
-qed
+ by (metis affine_parallel_def assms translation_assoc)
lemma affine_translation_aux:
fixes a :: "'a::real_vector"
@@ -503,24 +484,13 @@
lemma affine_translation:
"affine S \<longleftrightarrow> affine ((+) a ` S)" for a :: "'a::real_vector"
-proof
- show "affine ((+) a ` S)" if "affine S"
- using that translation_assoc [of "- a" a S]
- by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"])
- show "affine S" if "affine ((+) a ` S)"
- using that by (rule affine_translation_aux)
-qed
+ by (metis affine_translation_aux translation_galois)
lemma parallel_is_affine:
fixes S T :: "'a::real_vector set"
assumes "affine S" "affine_parallel S T"
shows "affine T"
-proof -
- from assms obtain a where "T = (\<lambda>x. a + x) ` S"
- unfolding affine_parallel_def by auto
- then show ?thesis
- using affine_translation assms by auto
-qed
+ by (metis affine_parallel_def affine_translation assms)
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
unfolding subspace_def affine_def by auto
@@ -532,64 +502,12 @@
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Subspace parallel to an affine set\<close>
lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
-proof -
- have h0: "subspace S \<Longrightarrow> affine S \<and> 0 \<in> S"
- using subspace_imp_affine[of S] subspace_0 by auto
- {
- assume assm: "affine S \<and> 0 \<in> S"
- {
- fix c :: real
- fix x
- assume x: "x \<in> S"
- have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
- moreover
- have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
- using affine_alt[of S] assm x by auto
- ultimately have "c *\<^sub>R x \<in> S" by auto
- }
- then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto
-
- {
- fix x y
- assume xy: "x \<in> S" "y \<in> S"
- define u where "u = (1 :: real)/2"
- have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)"
- by auto
- moreover
- have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y"
- by (simp add: algebra_simps)
- moreover
- have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S"
- using affine_alt[of S] assm xy by auto
- ultimately
- have "(1/2) *\<^sub>R (x+y) \<in> S"
- using u_def by auto
- moreover
- have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
- by auto
- ultimately
- have "x + y \<in> S"
- using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
- }
- then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S"
- by auto
- then have "subspace S"
- using h1 assm unfolding subspace_def by auto
- }
- then show ?thesis using h0 by metis
-qed
+ by (metis add_cancel_right_left affine_alt diff_add_cancel mem_affine_3 scaleR_eq_0_iff subspace_def vector_space_assms(4))
lemma affine_diffs_subspace:
assumes "affine S" "a \<in> S"
shows "subspace ((\<lambda>x. (-a)+x) ` S)"
-proof -
- have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
- have "affine ((\<lambda>x. (-a)+x) ` S)"
- using affine_translation assms by blast
- moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
- using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
- ultimately show ?thesis using subspace_affine by auto
-qed
+ by (metis ab_left_minus affine_translation assms image_eqI subspace_affine)
lemma affine_diffs_subspace_subtract:
"subspace ((\<lambda>x. x - a) ` S)" if "affine S" "a \<in> S"
@@ -600,61 +518,26 @@
and "a \<in> S"
assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}"
shows "subspace L \<and> affine_parallel S L"
-proof -
- from assms have "L = plus (- a) ` S" by auto
- then have par: "affine_parallel S L"
- unfolding affine_parallel_def ..
- then have "affine L" using assms parallel_is_affine by auto
- moreover have "0 \<in> L"
- using assms by auto
- ultimately show ?thesis
- using subspace_affine par by auto
-qed
+ by (smt (verit) Collect_cong ab_left_minus affine_parallel_def assms image_def mem_Collect_eq parallel_is_affine subspace_affine)
lemma parallel_subspace_aux:
assumes "subspace A"
and "subspace B"
and "affine_parallel A B"
shows "A \<supseteq> B"
-proof -
- from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
- using affine_parallel_expl[of A B] by auto
- then have "-a \<in> A"
- using assms subspace_0[of B] by auto
- then have "a \<in> A"
- using assms subspace_neg[of A "-a"] by auto
- then show ?thesis
- using assms a unfolding subspace_def by auto
-qed
+ by (metis add.right_neutral affine_parallel_expl assms subsetI subspace_def)
lemma parallel_subspace:
assumes "subspace A"
and "subspace B"
and "affine_parallel A B"
shows "A = B"
-proof
- show "A \<supseteq> B"
- using assms parallel_subspace_aux by auto
- show "A \<subseteq> B"
- using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
-qed
+ by (simp add: affine_parallel_commute assms parallel_subspace_aux subset_antisym)
lemma affine_parallel_subspace:
assumes "affine S" "S \<noteq> {}"
shows "\<exists>!L. subspace L \<and> affine_parallel S L"
-proof -
- have ex: "\<exists>L. subspace L \<and> affine_parallel S L"
- using assms parallel_subspace_explicit by auto
- {
- fix L1 L2
- assume ass: "subspace L1 \<and> affine_parallel S L1" "subspace L2 \<and> affine_parallel S L2"
- then have "affine_parallel L1 L2"
- using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
- then have "L1 = L2"
- using ass parallel_subspace by auto
- }
- then show ?thesis using ex by auto
-qed
+ by (meson affine_parallel_assoc affine_parallel_commute assms equals0I parallel_subspace parallel_subspace_explicit)
subsection \<open>Affine Dependence\<close>
@@ -662,50 +545,49 @@
text "Formalized by Lars Schewe."
definition\<^marker>\<open>tag important\<close> affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
- where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
+ where "affine_dependent S \<longleftrightarrow> (\<exists>x\<in>S. x \<in> affine hull (S - {x}))"
-lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
+lemma affine_dependent_imp_dependent: "affine_dependent S \<Longrightarrow> dependent S"
unfolding affine_dependent_def dependent_def
using affine_hull_subset_span by auto
lemma affine_dependent_subset:
- "\<lbrakk>affine_dependent s; s \<subseteq> t\<rbrakk> \<Longrightarrow> affine_dependent t"
-apply (simp add: affine_dependent_def Bex_def)
-apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
-done
+ "\<lbrakk>affine_dependent S; S \<subseteq> T\<rbrakk> \<Longrightarrow> affine_dependent T"
+ using hull_mono [OF Diff_mono [OF _ subset_refl]]
+ by (smt (verit) affine_dependent_def subsetD)
lemma affine_independent_subset:
- shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
-by (metis affine_dependent_subset)
+ shows "\<lbrakk>\<not> affine_dependent T; S \<subseteq> T\<rbrakk> \<Longrightarrow> \<not> affine_dependent S"
+ by (metis affine_dependent_subset)
lemma affine_independent_Diff:
- "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
+ "\<not> affine_dependent S \<Longrightarrow> \<not> affine_dependent(S - T)"
by (meson Diff_subset affine_dependent_subset)
proposition affine_dependent_explicit:
"affine_dependent p \<longleftrightarrow>
- (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
+ (\<exists>S U. finite S \<and> S \<subseteq> p \<and> sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> sum (\<lambda>v. U v *\<^sub>R v) S = 0)"
proof -
- have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> (\<Sum>w\<in>S. u w *\<^sub>R w) = 0"
- if "(\<Sum>w\<in>S. u w *\<^sub>R w) = x" "x \<in> p" "finite S" "S \<noteq> {}" "S \<subseteq> p - {x}" "sum u S = 1" for x S u
+ have "\<exists>S U. finite S \<and> S \<subseteq> p \<and> sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> (\<Sum>w\<in>S. U w *\<^sub>R w) = 0"
+ if "(\<Sum>w\<in>S. U w *\<^sub>R w) = x" "x \<in> p" "finite S" "S \<noteq> {}" "S \<subseteq> p - {x}" "sum U S = 1" for x S U
proof (intro exI conjI)
have "x \<notin> S"
using that by auto
- then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else u v) = 0"
+ then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else U v) = 0"
using that by (simp add: sum_delta_notmem)
- show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0"
+ show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else U w) *\<^sub>R w) = 0"
using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong)
qed (use that in auto)
- moreover have "\<exists>x\<in>p. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p - {x} \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
- if "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" "finite S" "S \<subseteq> p" "sum u S = 0" "v \<in> S" "u v \<noteq> 0" for S u v
+ moreover have "\<exists>x\<in>p. \<exists>S U. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p - {x} \<and> sum U S = 1 \<and> (\<Sum>v\<in>S. U v *\<^sub>R v) = x"
+ if "(\<Sum>v\<in>S. U v *\<^sub>R v) = 0" "finite S" "S \<subseteq> p" "sum U S = 0" "v \<in> S" "U v \<noteq> 0" for S U v
proof (intro bexI exI conjI)
have "S \<noteq> {v}"
using that by auto
then show "S - {v} \<noteq> {}"
using that by auto
- show "(\<Sum>x \<in> S - {v}. - (1 / u v) * u x) = 1"
+ show "(\<Sum>x \<in> S - {v}. - (1 / U v) * U x) = 1"
unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that)
- show "(\<Sum>x\<in>S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v"
+ show "(\<Sum>x\<in>S - {v}. (- (1 / U v) * U x) *\<^sub>R x) = v"
unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric]
scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>]
using that by auto
@@ -720,90 +602,82 @@
fixes S :: "'a::real_vector set"
assumes "finite S"
shows "affine_dependent S \<longleftrightarrow>
- (\<exists>u. sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
+ (\<exists>U. sum U S = 0 \<and> (\<exists>v\<in>S. U v \<noteq> 0) \<and> sum (\<lambda>v. U v *\<^sub>R v) S = 0)"
(is "?lhs = ?rhs")
proof
- have *: "\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else 0::'a)"
+ have *: "\<And>vt U v. (if vt then U v else 0) *\<^sub>R v = (if vt then (U v) *\<^sub>R v else 0::'a)"
by auto
assume ?lhs
- then obtain t u v where
- "finite t" "t \<subseteq> S" "sum u t = 0" "v\<in>t" "u v \<noteq> 0" "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
+ then obtain T U v where
+ "finite T" "T \<subseteq> S" "sum U T = 0" "v\<in>T" "U v \<noteq> 0" "(\<Sum>v\<in>T. U v *\<^sub>R v) = 0"
unfolding affine_dependent_explicit by auto
then show ?rhs
- apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
- apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>t\<subseteq>S\<close>])
+ apply (rule_tac x="\<lambda>x. if x\<in>T then U x else 0" in exI)
+ apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>T\<subseteq>S\<close>])
done
next
assume ?rhs
- then obtain u v where "sum u S = 0" "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
+ then obtain U v where "sum U S = 0" "v\<in>S" "U v \<noteq> 0" "(\<Sum>v\<in>S. U v *\<^sub>R v) = 0"
by auto
then show ?lhs unfolding affine_dependent_explicit
using assms by auto
qed
lemma dependent_imp_affine_dependent:
- assumes "dependent {x - a| x . x \<in> s}"
- and "a \<notin> s"
- shows "affine_dependent (insert a s)"
+ assumes "dependent {x - a| x . x \<in> S}"
+ and "a \<notin> S"
+ shows "affine_dependent (insert a S)"
proof -
- from assms(1)[unfolded dependent_explicit] obtain S u v
- where obt: "finite S" "S \<subseteq> {x - a |x. x \<in> s}" "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
+ from assms(1)[unfolded dependent_explicit] obtain S' U v
+ where S: "finite S'" "S' \<subseteq> {x - a |x. x \<in> S}" "v\<in>S'" "U v \<noteq> 0" "(\<Sum>v\<in>S'. U v *\<^sub>R v) = 0"
by auto
- define t where "t = (\<lambda>x. x + a) ` S"
-
- have inj: "inj_on (\<lambda>x. x + a) S"
+ define T where "T = (\<lambda>x. x + a) ` S'"
+ have inj: "inj_on (\<lambda>x. x + a) S'"
unfolding inj_on_def by auto
- have "0 \<notin> S"
- using obt(2) assms(2) unfolding subset_eq by auto
- have fin: "finite t" and "t \<subseteq> s"
- unfolding t_def using obt(1,2) by auto
- then have "finite (insert a t)" and "insert a t \<subseteq> insert a s"
+ have "0 \<notin> S'"
+ using S(2) assms(2) unfolding subset_eq by auto
+ have fin: "finite T" and "T \<subseteq> S"
+ unfolding T_def using S(1,2) by auto
+ then have "finite (insert a T)" and "insert a T \<subseteq> insert a S"
by auto
- moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x)) = (\<Sum>x\<in>t. Q x)"
- apply (rule sum.cong)
- using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
- apply auto
- done
- have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
- unfolding sum_clauses(2)[OF fin] * using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by auto
- moreover have "\<exists>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) \<noteq> 0"
- using obt(3,4) \<open>0\<notin>S\<close>
- by (rule_tac x="v + a" in bexI) (auto simp: t_def)
- moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"
- using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by (auto intro!: sum.cong)
- have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)"
+ moreover have *: "\<And>P Q. (\<Sum>x\<in>T. (if x = a then P x else Q x)) = (\<Sum>x\<in>T. Q x)"
+ by (smt (verit, best) \<open>T \<subseteq> S\<close> assms(2) subsetD sum.cong)
+ have "(\<Sum>x\<in>insert a T. if x = a then - (\<Sum>x\<in>T. U (x - a)) else U (x - a)) = 0"
+ by (smt (verit) \<open>T \<subseteq> S\<close> assms(2) fin insert_absorb insert_subset sum.insert sum_mono)
+ moreover have "\<exists>v\<in>insert a T. (if v = a then - (\<Sum>x\<in>T. U (x - a)) else U (v - a)) \<noteq> 0"
+ using S(3,4) \<open>0\<notin>S'\<close>
+ by (rule_tac x="v + a" in bexI) (auto simp: T_def)
+ moreover have *: "\<And>P Q. (\<Sum>x\<in>T. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>T. Q x *\<^sub>R x)"
+ using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto intro!: sum.cong)
+ have "(\<Sum>x\<in>T. U (x - a)) *\<^sub>R a = (\<Sum>v\<in>T. U (v - a) *\<^sub>R v)"
unfolding scaleR_left.sum
- unfolding t_def and sum.reindex[OF inj] and o_def
- using obt(5)
+ unfolding T_def and sum.reindex[OF inj] and o_def
+ using S(5)
by (auto simp: sum.distrib scaleR_right_distrib)
- then have "(\<Sum>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) *\<^sub>R v) = 0"
- unfolding sum_clauses(2)[OF fin]
- using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
- by (auto simp: *)
+ then have "(\<Sum>v\<in>insert a T. (if v = a then - (\<Sum>x\<in>T. U (x - a)) else U (v - a)) *\<^sub>R v) = 0"
+ unfolding sum_clauses(2)[OF fin] using \<open>a\<notin>S\<close> \<open>T\<subseteq>S\<close> by (auto simp: *)
ultimately show ?thesis
unfolding affine_dependent_explicit
- apply (rule_tac x="insert a t" in exI, auto)
- done
+ by (force intro!: exI[where x="insert a T"])
qed
lemma affine_dependent_biggerset:
- fixes s :: "'a::euclidean_space set"
- assumes "finite s" "card s \<ge> DIM('a) + 2"
- shows "affine_dependent s"
+ fixes S :: "'a::euclidean_space set"
+ assumes "finite S" "card S \<ge> DIM('a) + 2"
+ shows "affine_dependent S"
proof -
- have "s \<noteq> {}" using assms by auto
- then obtain a where "a\<in>s" by auto
- have *: "{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})"
+ have "S \<noteq> {}" using assms by auto
+ then obtain a where "a\<in>S" by auto
+ have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})"
by auto
- have "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
+ have "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
unfolding * by (simp add: card_image inj_on_def)
also have "\<dots> > DIM('a)" using assms(2)
- unfolding card_Diff_singleton[OF \<open>a\<in>s\<close>] by auto
- finally show ?thesis
- apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
- apply (rule dependent_imp_affine_dependent)
- apply (rule dependent_biggerset, auto)
- done
+ unfolding card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
+ finally have "affine_dependent (insert a (S - {a}))"
+ using dependent_biggerset dependent_imp_affine_dependent by blast
+ then show ?thesis
+ by (simp add: \<open>a \<in> S\<close> insert_absorb)
qed
lemma affine_dependent_biggerset_general:
@@ -822,13 +696,10 @@
also have "\<dots> < dim S + 1" by auto
also have "\<dots> \<le> card (S - {a})"
using assms card_Diff_singleton[OF \<open>a\<in>S\<close>] by auto
- finally show ?thesis
- apply (subst insert_Diff[OF \<open>a\<in>S\<close>, symmetric])
- apply (rule dependent_imp_affine_dependent)
- apply (rule dependent_biggerset_general)
- unfolding **
- apply auto
- done
+ finally have "affine_dependent (insert a (S - {a}))"
+ by (smt (verit) Collect_cong dependent_imp_affine_dependent dependent_biggerset_general ** Diff_iff insertCI)
+ then show ?thesis
+ by (simp add: \<open>a \<in> S\<close> insert_absorb)
qed
@@ -882,16 +753,7 @@
lemma affine_dependent_translation_eq:
"affine_dependent S \<longleftrightarrow> affine_dependent ((\<lambda>x. a + x) ` S)"
-proof -
- {
- assume "affine_dependent ((\<lambda>x. a + x) ` S)"
- then have "affine_dependent S"
- using affine_dependent_translation[of "((\<lambda>x. a + x) ` S)" "-a"] translation_assoc[of "-a" a]
- by auto
- }
- then show ?thesis
- using affine_dependent_translation by auto
-qed
+ by (metis affine_dependent_translation translation_galois)
lemma affine_hull_0_dependent:
assumes "0 \<in> affine hull S"
@@ -919,14 +781,8 @@
ultimately have "x \<in> span (S - {x})" by auto
then have "x \<noteq> 0 \<Longrightarrow> dependent S"
using x dependent_def by auto
- moreover
- {
- assume "x = 0"
- then have "0 \<in> affine hull S"
- using x hull_mono[of "S - {0}" S] by auto
- then have "dependent S"
- using affine_hull_0_dependent by auto
- }
+ moreover have "dependent S" if "x = 0"
+ by (metis that affine_hull_0_dependent Diff_insert_absorb dependent_zero x)
ultimately show ?thesis by auto
qed
@@ -945,60 +801,45 @@
lemma affine_dependent_iff_dependent2:
assumes "a \<in> S"
shows "affine_dependent S \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` (S-{a}))"
-proof -
- have "insert a (S - {a}) = S"
- using assms by auto
- then show ?thesis
- using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
-qed
+ by (metis Diff_iff affine_dependent_iff_dependent assms insert_Diff singletonI)
lemma affine_hull_insert_span_gen:
- "affine hull (insert a s) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` s)"
+ "affine hull (insert a S) = (\<lambda>x. a + x) ` span ((\<lambda>x. - a + x) ` S)"
proof -
- have h1: "{x - a |x. x \<in> s} = ((\<lambda>x. -a+x) ` s)"
+ have h1: "{x - a |x. x \<in> S} = ((\<lambda>x. -a+x) ` S)"
by auto
{
- assume "a \<notin> s"
+ assume "a \<notin> S"
then have ?thesis
- using affine_hull_insert_span[of a s] h1 by auto
+ using affine_hull_insert_span[of a S] h1 by auto
}
moreover
{
- assume a1: "a \<in> s"
- have "\<exists>x. x \<in> s \<and> -a+x=0"
- apply (rule exI[of _ a])
- using a1
- apply auto
- done
- then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
+ assume a1: "a \<in> S"
+ then have "insert 0 ((\<lambda>x. -a+x) ` (S - {a})) = (\<lambda>x. -a+x) ` S"
by auto
- then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
- using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
- moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
+ then have "span ((\<lambda>x. -a+x) ` (S - {a})) = span ((\<lambda>x. -a+x) ` S)"
+ using span_insert_0[of "(+) (- a) ` (S - {a})"]
+ by presburger
+ moreover have "{x - a |x. x \<in> (S - {a})} = ((\<lambda>x. -a+x) ` (S - {a}))"
by auto
- moreover have "insert a (s - {a}) = insert a s"
+ moreover have "insert a (S - {a}) = insert a S"
by auto
ultimately have ?thesis
- using affine_hull_insert_span[of "a" "s-{a}"] by auto
+ using affine_hull_insert_span[of "a" "S-{a}"] by auto
}
ultimately show ?thesis by auto
qed
lemma affine_hull_span2:
- assumes "a \<in> s"
- shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` (s-{a}))"
- using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]]
- by auto
+ assumes "a \<in> S"
+ shows "affine hull S = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` (S-{a}))"
+ by (metis affine_hull_insert_span_gen assms insert_Diff)
lemma affine_hull_span_gen:
- assumes "a \<in> affine hull s"
- shows "affine hull s = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` s)"
-proof -
- have "affine hull (insert a s) = affine hull s"
- using hull_redundant[of a affine s] assms by auto
- then show ?thesis
- using affine_hull_insert_span_gen[of a "s"] by auto
-qed
+ assumes "a \<in> affine hull S"
+ shows "affine hull S = (\<lambda>x. a+x) ` span ((\<lambda>x. -a+x) ` S)"
+ by (metis affine_hull_insert_span_gen assms hull_redundant)
lemma affine_hull_span_0:
assumes "0 \<in> affine hull S"
@@ -1044,29 +885,13 @@
lemma affine_basis_exists:
fixes V :: "'n::real_vector set"
shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
-proof (cases "V = {}")
- case True
- then show ?thesis
- using affine_independent_0 by auto
-next
- case False
- then obtain x where "x \<in> V" by auto
- then show ?thesis
- using affine_dependent_def[of "{x}"] extend_to_affine_basis_nonempty[of "{x}" V]
- by auto
-qed
+ by (metis affine_dependent_def affine_independent_1 empty_subsetI extend_to_affine_basis_nonempty insert_subset order_refl)
proposition extend_to_affine_basis:
fixes S V :: "'n::real_vector set"
assumes "\<not> affine_dependent S" "S \<subseteq> V"
obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
-proof (cases "S = {}")
- case True then show ?thesis
- using affine_basis_exists by (metis empty_subsetI that)
-next
- case False
- then show ?thesis by (metis assms extend_to_affine_basis_nonempty that)
-qed
+ by (metis affine_basis_exists assms(1) assms(2) bot.extremum extend_to_affine_basis_nonempty)
subsection \<open>Affine Dimension of a Set\<close>
@@ -1095,7 +920,7 @@
by (metis affine_empty subset_empty subset_hull)
lemma empty_eq_affine_hull[simp]: "{} = affine hull S \<longleftrightarrow> S = {}"
-by (metis affine_hull_eq_empty)
+ by (metis affine_hull_eq_empty)
lemma aff_dim_parallel_subspace_aux:
fixes B :: "'n::euclidean_space set"
@@ -1146,7 +971,7 @@
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
moreover have "affine_parallel (affine hull B) Lb"
using Lb_def B assms affine_hull_span2[of a B] a
- affine_parallel_commut[of "Lb" "(affine hull B)"]
+ affine_parallel_commute[of "Lb" "(affine hull B)"]
unfolding affine_parallel_def
by auto
moreover have "subspace Lb"
@@ -1168,15 +993,7 @@
fixes B :: "'n::euclidean_space set"
assumes "\<not> affine_dependent B"
shows "finite B"
-proof -
- {
- assume "B \<noteq> {}"
- then obtain a where "a \<in> B" by auto
- then have ?thesis
- using aff_dim_parallel_subspace_aux assms by auto
- }
- then show ?thesis by auto
-qed
+ using aff_dim_parallel_subspace_aux assms finite.simps by fastforce
lemma aff_dim_empty:
@@ -1195,7 +1012,7 @@
qed
lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1"
- by (simp add: aff_dim_empty [symmetric])
+ using aff_dim_empty by blast
lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S"
unfolding aff_dim_def using hull_hull[of _ S] by auto
@@ -1224,7 +1041,7 @@
define Lb where "Lb = span ((\<lambda>x. -a+x) ` (B-{a}))"
have "affine_parallel (affine hull B) Lb"
using Lb_def affine_hull_span2[of a B] a
- affine_parallel_commut[of "Lb" "(affine hull B)"]
+ affine_parallel_commute[of "Lb" "(affine hull B)"]
unfolding affine_parallel_def by auto
moreover have "subspace Lb"
using Lb_def subspace_span by auto
@@ -1245,11 +1062,14 @@
using aff_dim_unique[of B B] assms by auto
lemma affine_independent_iff_card:
- fixes s :: "'a::euclidean_space set"
- shows "\<not> affine_dependent s \<longleftrightarrow> finite s \<and> aff_dim s = int(card s) - 1"
- apply (rule iffI)
- apply (simp add: aff_dim_affine_independent aff_independent_finite)
- by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff)
+ fixes S :: "'a::euclidean_space set"
+ shows "\<not> affine_dependent S \<longleftrightarrow> finite S \<and> aff_dim S = int(card S) - 1" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (simp add: aff_dim_affine_independent aff_independent_finite)
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (metis of_nat_eq_iff affine_basis_exists aff_dim_unique card_subset_eq diff_add_cancel)
+qed
lemma aff_dim_sing [simp]:
fixes a :: "'n::euclidean_space"
@@ -1272,78 +1092,39 @@
fixes V :: "('n::euclidean_space) set"
shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and>
\<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
-proof -
- obtain B where B: "\<not> affine_dependent B" "B \<subseteq> V" "affine hull B = affine hull V"
- using affine_basis_exists[of V] by auto
- then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
- with B show ?thesis by auto
-qed
+ by (metis aff_dim_unique affine_basis_exists)
lemma aff_dim_le_card:
fixes V :: "'n::euclidean_space set"
assumes "finite V"
shows "aff_dim V \<le> of_nat (card V) - 1"
-proof -
- obtain B where B: "B \<subseteq> V" "of_nat (card B) = aff_dim V + 1"
- using aff_dim_inner_basis_exists[of V] by auto
- then have "card B \<le> card V"
- using assms card_mono by auto
- with B show ?thesis by auto
+ by (metis aff_dim_inner_basis_exists assms card_mono le_diff_eq of_nat_le_iff)
+
+lemma aff_dim_parallel_le:
+ fixes S T :: "'n::euclidean_space set"
+ assumes "affine_parallel (affine hull S) (affine hull T)"
+ shows "aff_dim S \<le> aff_dim T"
+proof (cases "S={} \<or> T={}")
+ case True
+ then show ?thesis
+ by (smt (verit, best) aff_dim_affine_hull2 affine_hull_empty affine_parallel_def assms empty_is_image)
+next
+ case False
+ then obtain L where L: "subspace L" "affine_parallel (affine hull T) L"
+ by (metis affine_affine_hull affine_hull_eq_empty affine_parallel_subspace)
+ with False show ?thesis
+ by (metis aff_dim_parallel_subspace affine_parallel_assoc assms dual_order.refl)
qed
lemma aff_dim_parallel_eq:
fixes S T :: "'n::euclidean_space set"
assumes "affine_parallel (affine hull S) (affine hull T)"
shows "aff_dim S = aff_dim T"
-proof -
- {
- assume "T \<noteq> {}" "S \<noteq> {}"
- then obtain L where L: "subspace L \<and> affine_parallel (affine hull T) L"
- using affine_parallel_subspace[of "affine hull T"]
- affine_affine_hull[of T]
- by auto
- then have "aff_dim T = int (dim L)"
- using aff_dim_parallel_subspace \<open>T \<noteq> {}\<close> by auto
- moreover have *: "subspace L \<and> affine_parallel (affine hull S) L"
- using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
- moreover from * have "aff_dim S = int (dim L)"
- using aff_dim_parallel_subspace \<open>S \<noteq> {}\<close> by auto
- ultimately have ?thesis by auto
- }
- moreover
- {
- assume "S = {}"
- then have "S = {}" and "T = {}"
- using assms
- unfolding affine_parallel_def
- by auto
- then have ?thesis using aff_dim_empty by auto
- }
- moreover
- {
- assume "T = {}"
- then have "S = {}" and "T = {}"
- using assms
- unfolding affine_parallel_def
- by auto
- then have ?thesis
- using aff_dim_empty by auto
- }
- ultimately show ?thesis by blast
-qed
+ by (smt (verit, del_insts) aff_dim_parallel_le affine_parallel_commute assms)
lemma aff_dim_translation_eq:
"aff_dim ((+) a ` S) = aff_dim S" for a :: "'n::euclidean_space"
-proof -
- have "affine_parallel (affine hull S) (affine hull ((\<lambda>x. a + x) ` S))"
- unfolding affine_parallel_def
- apply (rule exI[of _ "a"])
- using affine_hull_translation[of a S]
- apply auto
- done
- then show ?thesis
- using aff_dim_parallel_eq[of S "(\<lambda>x. a + x) ` S"] by auto
-qed
+ by (metis aff_dim_parallel_eq affine_hull_translation affine_parallel_def)
lemma aff_dim_translation_eq_subtract:
"aff_dim ((\<lambda>x. x - a) ` S) = aff_dim S" for a :: "'n::euclidean_space"
@@ -1351,97 +1132,51 @@
lemma aff_dim_affine:
fixes S L :: "'n::euclidean_space set"
- assumes "S \<noteq> {}"
- and "affine S"
- and "subspace L"
- and "affine_parallel S L"
+ assumes "affine S" "subspace L" "affine_parallel S L" "S \<noteq> {}"
shows "aff_dim S = int (dim L)"
-proof -
- have *: "affine hull S = S"
- using assms affine_hull_eq[of S] by auto
- then have "affine_parallel (affine hull S) L"
- using assms by (simp add: *)
- then show ?thesis
- using assms aff_dim_parallel_subspace[of S L] by blast
-qed
+ by (simp add: aff_dim_parallel_subspace assms hull_same)
-lemma dim_affine_hull:
+lemma dim_affine_hull [simp]:
fixes S :: "'n::euclidean_space set"
shows "dim (affine hull S) = dim S"
-proof -
- have "dim (affine hull S) \<ge> dim S"
- using dim_subset by auto
- moreover have "dim (span S) \<ge> dim (affine hull S)"
- using dim_subset affine_hull_subset_span by blast
- moreover have "dim (span S) = dim S"
- using dim_span by auto
- ultimately show ?thesis by auto
-qed
+ by (metis affine_hull_subset_span dim_eq_span dim_mono hull_subset span_eq_dim)
lemma aff_dim_subspace:
fixes S :: "'n::euclidean_space set"
assumes "subspace S"
shows "aff_dim S = int (dim S)"
-proof (cases "S={}")
- case True with assms show ?thesis
- by (simp add: subspace_affine)
-next
- case False
- with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine
- show ?thesis by auto
-qed
+ by (metis aff_dim_affine affine_parallel_subspace assms empty_iff parallel_subspace subspace_affine)
lemma aff_dim_zero:
fixes S :: "'n::euclidean_space set"
assumes "0 \<in> affine hull S"
shows "aff_dim S = int (dim S)"
-proof -
- have "subspace (affine hull S)"
- using subspace_affine[of "affine hull S"] affine_affine_hull assms
- by auto
- then have "aff_dim (affine hull S) = int (dim (affine hull S))"
- using assms aff_dim_subspace[of "affine hull S"] by auto
- then show ?thesis
- using aff_dim_affine_hull[of S] dim_affine_hull[of S]
- by auto
-qed
+ by (metis aff_dim_affine_hull aff_dim_subspace affine_hull_span_0 assms dim_span subspace_span)
lemma aff_dim_eq_dim:
- "aff_dim S = int (dim ((+) (- a) ` S))" if "a \<in> affine hull S"
- for S :: "'n::euclidean_space set"
-proof -
- have "0 \<in> affine hull (+) (- a) ` S"
- unfolding affine_hull_translation
- using that by (simp add: ac_simps)
- with aff_dim_zero show ?thesis
- by (metis aff_dim_translation_eq)
-qed
+ fixes S :: "'n::euclidean_space set"
+ assumes "a \<in> affine hull S"
+ shows "aff_dim S = int (dim ((+) (- a) ` S))"
+ by (metis ab_left_minus aff_dim_translation_eq aff_dim_zero affine_hull_translation image_eqI assms)
lemma aff_dim_eq_dim_subtract:
- "aff_dim S = int (dim ((\<lambda>x. x - a) ` S))" if "a \<in> affine hull S"
- for S :: "'n::euclidean_space set"
- using aff_dim_eq_dim [of a] that by (simp cong: image_cong_simp)
+ fixes S :: "'n::euclidean_space set"
+ assumes "a \<in> affine hull S"
+ shows "aff_dim S = int (dim ((\<lambda>x. x - a) ` S))"
+ using aff_dim_eq_dim assms by auto
lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
- using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"]
- dim_UNIV[where 'a="'n::euclidean_space"]
- by auto
+ by (simp add: aff_dim_subspace)
lemma aff_dim_geq:
fixes V :: "'n::euclidean_space set"
shows "aff_dim V \<ge> -1"
-proof -
- obtain B where "affine hull B = affine hull V"
- and "\<not> affine_dependent B"
- and "int (card B) = aff_dim V + 1"
- using aff_dim_basis_exists by auto
- then show ?thesis by auto
-qed
+ by (metis add_le_cancel_right aff_dim_basis_exists diff_self of_nat_0_le_iff uminus_add_conv_diff)
lemma aff_dim_negative_iff [simp]:
fixes S :: "'n::euclidean_space set"
- shows "aff_dim S < 0 \<longleftrightarrow>S = {}"
-by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
+ shows "aff_dim S < 0 \<longleftrightarrow> S = {}"
+ by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
lemma aff_lowdim_subset_hyperplane:
fixes S :: "'a::euclidean_space set"
@@ -1482,83 +1217,48 @@
fixes S :: "'a :: euclidean_space set"
assumes "\<not> affine_dependent S" "a \<in> S"
shows "card S = dim ((\<lambda>x. x - a) ` S) + 1"
-proof -
- have non: "\<not> affine_dependent (insert a S)"
- by (simp add: assms insert_absorb)
- have "finite S"
- by (meson assms aff_independent_finite)
- with \<open>a \<in> S\<close> have "card S \<noteq> 0" by auto
- moreover have "dim ((\<lambda>x. x - a) ` S) = card S - 1"
- using aff_dim_eq_dim_subtract aff_dim_unique \<open>a \<in> S\<close> hull_inc insert_absorb non by fastforce
- ultimately show ?thesis
- by auto
-qed
+ using aff_dim_affine_independent aff_dim_eq_dim_subtract assms hull_subset by fastforce
lemma independent_card_le_aff_dim:
fixes B :: "'n::euclidean_space set"
assumes "B \<subseteq> V"
assumes "\<not> affine_dependent B"
shows "int (card B) \<le> aff_dim V + 1"
-proof -
- obtain T where T: "\<not> affine_dependent T \<and> B \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
- by (metis assms extend_to_affine_basis[of B V])
- then have "of_nat (card T) = aff_dim V + 1"
- using aff_dim_unique by auto
- then show ?thesis
- using T card_mono[of T B] aff_independent_finite[of T] by auto
-qed
+ by (metis aff_dim_unique aff_independent_finite assms card_mono extend_to_affine_basis of_nat_mono)
lemma aff_dim_subset:
fixes S T :: "'n::euclidean_space set"
assumes "S \<subseteq> T"
shows "aff_dim S \<le> aff_dim T"
-proof -
- obtain B where B: "\<not> affine_dependent B" "B \<subseteq> S" "affine hull B = affine hull S"
- "of_nat (card B) = aff_dim S + 1"
- using aff_dim_inner_basis_exists[of S] by auto
- then have "int (card B) \<le> aff_dim T + 1"
- using assms independent_card_le_aff_dim[of B T] by auto
- with B show ?thesis by auto
-qed
+ by (metis add_le_cancel_right aff_dim_inner_basis_exists assms dual_order.trans independent_card_le_aff_dim)
lemma aff_dim_le_DIM:
fixes S :: "'n::euclidean_space set"
shows "aff_dim S \<le> int (DIM('n))"
-proof -
- have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
- using aff_dim_UNIV by auto
- then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
- using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
-qed
+ by (metis aff_dim_UNIV aff_dim_subset top_greatest)
lemma affine_dim_equal:
fixes S :: "'n::euclidean_space set"
assumes "affine S" "affine T" "S \<noteq> {}" "S \<subseteq> T" "aff_dim S = aff_dim T"
shows "S = T"
proof -
- obtain a where "a \<in> S" using assms by auto
- then have "a \<in> T" using assms by auto
+ obtain a where "a \<in> S" "a \<in> T" "T \<noteq> {}" using assms by auto
define LS where "LS = {y. \<exists>x \<in> S. (-a) + x = y}"
then have ls: "subspace LS" "affine_parallel S LS"
using assms parallel_subspace_explicit[of S a LS] \<open>a \<in> S\<close> by auto
then have h1: "int(dim LS) = aff_dim S"
using assms aff_dim_affine[of S LS] by auto
- have "T \<noteq> {}" using assms by auto
define LT where "LT = {y. \<exists>x \<in> T. (-a) + x = y}"
then have lt: "subspace LT \<and> affine_parallel T LT"
using assms parallel_subspace_explicit[of T a LT] \<open>a \<in> T\<close> by auto
- then have "int(dim LT) = aff_dim T"
- using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close> by auto
then have "dim LS = dim LT"
- using h1 assms by auto
+ using assms aff_dim_affine[of T LT] \<open>T \<noteq> {}\<close> h1 by auto
moreover have "LS \<le> LT"
using LS_def LT_def assms by auto
ultimately have "LS = LT"
using subspace_dim_equal[of LS LT] ls lt by auto
- moreover have "S = {x. \<exists>y \<in> LS. a+y=x}"
- using LS_def by auto
- moreover have "T = {x. \<exists>y \<in> LT. a+y=x}"
- using LT_def by auto
+ moreover have "S = {x. \<exists>y \<in> LS. a+y=x}" "T = {x. \<exists>y \<in> LT. a+y=x}"
+ using LS_def LT_def by auto
ultimately show ?thesis by auto
qed
@@ -1566,10 +1266,6 @@
fixes S :: "'a::euclidean_space set"
shows "aff_dim S = 0 \<longleftrightarrow> (\<exists>a. S = {a})"
proof (cases "S = {}")
- case True
- then show ?thesis
- by auto
-next
case False
then obtain a where "a \<in> S" by auto
show ?thesis
@@ -1580,58 +1276,39 @@
then show "\<exists>a. S = {a}"
using \<open>a \<in> S\<close> by blast
qed auto
-qed
+qed auto
lemma affine_hull_UNIV:
fixes S :: "'n::euclidean_space set"
assumes "aff_dim S = int(DIM('n))"
shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
-proof -
- have "S \<noteq> {}"
- using assms aff_dim_empty[of S] by auto
- have h0: "S \<subseteq> affine hull S"
- using hull_subset[of S _] by auto
- have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S"
- using aff_dim_UNIV assms by auto
- then have h2: "aff_dim (affine hull S) \<le> aff_dim (UNIV :: ('n::euclidean_space) set)"
- using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto
- have h3: "aff_dim S \<le> aff_dim (affine hull S)"
- using h0 aff_dim_subset[of S "affine hull S"] assms by auto
- then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)"
- using h0 h1 h2 by auto
- then show ?thesis
- using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"]
- affine_affine_hull[of S] affine_UNIV assms h4 h0 \<open>S \<noteq> {}\<close>
- by auto
-qed
+ by (simp add: aff_dim_empty affine_dim_equal assms)
lemma disjoint_affine_hull:
- fixes s :: "'n::euclidean_space set"
- assumes "\<not> affine_dependent s" "t \<subseteq> s" "u \<subseteq> s" "t \<inter> u = {}"
- shows "(affine hull t) \<inter> (affine hull u) = {}"
+ fixes S :: "'n::euclidean_space set"
+ assumes "\<not> affine_dependent S" "T \<subseteq> S" "U \<subseteq> S" "T \<inter> U = {}"
+ shows "(affine hull T) \<inter> (affine hull U) = {}"
proof -
- from assms(1) have "finite s"
- by (simp add: aff_independent_finite)
- with assms(2,3) have "finite t" "finite u"
- by (blast intro: finite_subset)+
- have False if "y \<in> affine hull t" and "y \<in> affine hull u" for y
+ obtain "finite S" "finite T" "finite U"
+ using assms by (simp add: aff_independent_finite finite_subset)
+ have False if "y \<in> affine hull T" and "y \<in> affine hull U" for y
proof -
from that obtain a b
- where a1 [simp]: "sum a t = 1"
- and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) t = y"
- and [simp]: "sum b u = 1" "sum (\<lambda>v. b v *\<^sub>R v) u = y"
- by (auto simp: affine_hull_finite \<open>finite t\<close> \<open>finite u\<close>)
- define c where "c x = (if x \<in> t then a x else if x \<in> u then -(b x) else 0)" for x
- from assms(2,3,4) have [simp]: "s \<inter> t = t" "s \<inter> - t \<inter> u = u"
- by auto
- have "sum c s = 0"
- by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite s\<close> sum_negf)
- moreover have "\<not> (\<forall>v\<in>s. c v = 0)"
- by (metis (no_types) IntD1 \<open>s \<inter> t = t\<close> a1 c_def sum.neutral zero_neq_one)
- moreover have "(\<Sum>v\<in>s. c v *\<^sub>R v) = 0"
- by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite s\<close>)
+ where a1 [simp]: "sum a T = 1"
+ and [simp]: "sum (\<lambda>v. a v *\<^sub>R v) T = y"
+ and [simp]: "sum b U = 1" "sum (\<lambda>v. b v *\<^sub>R v) U = y"
+ by (auto simp: affine_hull_finite \<open>finite T\<close> \<open>finite U\<close>)
+ define c where "c x = (if x \<in> T then a x else if x \<in> U then -(b x) else 0)" for x
+ have [simp]: "S \<inter> T = T" "S \<inter> - T \<inter> U = U"
+ using assms by auto
+ have "sum c S = 0"
+ by (simp add: c_def comm_monoid_add_class.sum.If_cases \<open>finite S\<close> sum_negf)
+ moreover have "\<not> (\<forall>v\<in>S. c v = 0)"
+ by (metis (no_types) IntD1 \<open>S \<inter> T = T\<close> a1 c_def sum.neutral zero_neq_one)
+ moreover have "(\<Sum>v\<in>S. c v *\<^sub>R v) = 0"
+ by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases \<open>finite S\<close>)
ultimately show ?thesis
- using assms(1) \<open>finite s\<close> by (auto simp: affine_dependent_explicit)
+ using assms(1) \<open>finite S\<close> by (auto simp: affine_dependent_explicit)
qed
then show ?thesis by blast
qed
--- a/src/HOL/Analysis/Borel_Space.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Sat Aug 12 10:09:29 2023 +0100
@@ -77,13 +77,7 @@
using of_rat_dense by blast
assume * [rule_format]: "\<forall>d>0. \<exists>x\<in>A. x \<noteq> a \<and> dist x a < d \<and> \<not> l < f x"
from q2 have "real_of_rat q2 < f a \<and> (\<forall>x\<in>A. x < a \<longrightarrow> f x < real_of_rat q2)"
- proof auto
- fix x assume "x \<in> A" "x < a"
- with q2 *[of "a - x"] show "f x < real_of_rat q2"
- apply (auto simp add: dist_real_def not_less)
- apply (subgoal_tac "f x \<le> f xa")
- by (auto intro: mono)
- qed
+ using q2 *[of "a - _"] dist_real_def mono by fastforce
thus ?thesis by auto
next
fix u assume "u > f a"
@@ -91,13 +85,7 @@
using of_rat_dense by blast
assume *[rule_format]: "\<forall>d>0. \<exists>x\<in>A. x \<noteq> a \<and> dist x a < d \<and> \<not> u > f x"
from q2 have "real_of_rat q2 > f a \<and> (\<forall>x\<in>A. x > a \<longrightarrow> f x > real_of_rat q2)"
- proof auto
- fix x assume "x \<in> A" "x > a"
- with q2 *[of "x - a"] show "f x > real_of_rat q2"
- apply (auto simp add: dist_real_def)
- apply (subgoal_tac "f x \<ge> f xa")
- by (auto intro: mono)
- qed
+ using q2 *[of "_ - a"] dist_real_def mono by fastforce
thus ?thesis by auto
qed
qed
@@ -127,13 +115,8 @@
fixes A :: "real set"
assumes "open A" "mono_on A f"
shows "countable {a\<in>A. \<not>isCont f a}"
-proof -
- have "{a\<in>A. \<not>isCont f a} = {a\<in>A. \<not>(continuous (at a within A) f)}"
- by (auto simp add: continuous_within_open [OF _ \<open>open A\<close>])
- thus ?thesis
- apply (elim ssubst)
- by (rule mono_on_ctble_discont, rule assms)
-qed
+ using continuous_within_open [OF _ \<open>open A\<close>] \<open>mono_on A f\<close>
+ by (smt (verit, ccfv_threshold) Collect_cong mono_on_ctble_discont)
lemma mono_ctble_discont:
fixes f :: "real \<Rightarrow> real"
@@ -144,8 +127,7 @@
lemma has_real_derivative_imp_continuous_on:
assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
shows "continuous_on A f"
- apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
- using assms differentiable_at_withinI real_differentiable_def by blast
+ by (meson DERIV_isCont assms continuous_at_imp_continuous_on)
lemma continuous_interval_vimage_Int:
assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
@@ -173,14 +155,11 @@
intro!: mono)
moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
moreover have "g c' \<le> c" "g d' \<ge> d"
- apply (insert c'' d'' c'd'_in_set)
- apply (subst c''(2)[symmetric])
- apply (auto simp: c'_def intro!: mono cInf_lower c'') []
- apply (subst d''(2)[symmetric])
- apply (auto simp: d'_def intro!: mono cSup_upper d'') []
- done
- with c'd'_in_set have "g c' = c" "g d' = d" by auto
- ultimately show ?thesis using that by blast
+ using c'' d'' calculation by (metis IntE atLeastAtMost_iff mono order_class.order_eq_iff)+
+ with c'd'_in_set have "g c' = c" "g d' = d"
+ by auto
+ ultimately show ?thesis
+ using that by blast
qed
subsection \<open>Generic Borel spaces\<close>
@@ -196,9 +175,7 @@
by (auto simp add: measurable_def borel_def)
lemma in_borel_measurable_borel:
- "f \<in> borel_measurable M \<longleftrightarrow>
- (\<forall>S \<in> sets borel.
- f -` S \<inter> space M \<in> sets M)"
+ "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>S \<in> sets borel. f -` S \<inter> space M \<in> sets M)"
by (auto simp add: measurable_def borel_def)
lemma space_borel[simp]: "space borel = UNIV"
@@ -219,10 +196,7 @@
lemma borel_open[measurable (raw generic)]:
assumes "open A" shows "A \<in> sets borel"
-proof -
- have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
- thus ?thesis unfolding borel_def by auto
-qed
+ by (simp add: assms sets_borel)
lemma borel_closed[measurable (raw generic)]:
assumes "closed A" shows "A \<in> sets borel"
@@ -237,12 +211,7 @@
unfolding insert_def by (rule sets.Un) auto
lemma sets_borel_eq_count_space: "sets (borel :: 'a::{countable, t2_space} measure) = count_space UNIV"
-proof -
- have "(\<Union>a\<in>A. {a}) \<in> sets borel" for A :: "'a set"
- by (intro sets.countable_UN') auto
- then show ?thesis
- by auto
-qed
+ by (simp add: set_eq_iff sets.countable)
lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
unfolding Compl_eq_Diff_UNIV by simp
@@ -312,7 +281,7 @@
shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
(\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
- (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
+ (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong: if_cong)
lemma borel_measurable_restrict_space_iff_ennreal:
fixes f :: "'a \<Rightarrow> ennreal"
@@ -320,7 +289,7 @@
shows "f \<in> borel_measurable (restrict_space M \<Omega>) \<longleftrightarrow>
(\<lambda>x. f x * indicator \<Omega> x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
- (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong del: if_weak_cong)
+ (auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a] cong: if_cong)
lemma borel_measurable_restrict_space_iff:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -329,7 +298,7 @@
(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> borel_measurable M"
by (subst measurable_restrict_space_iff)
(auto simp: indicator_def of_bool_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a] ac_simps
- cong del: if_weak_cong)
+ cong: if_cong)
lemma cbox_borel[measurable]: "cbox a b \<in> sets borel"
by (auto intro: borel_closed)
@@ -338,7 +307,7 @@
by (auto intro: borel_open)
lemma borel_compact: "compact (A::'a::t2_space set) \<Longrightarrow> A \<in> sets borel"
- by (auto intro: borel_closed dest!: compact_imp_closed)
+ by (simp add: borel_closed compact_imp_closed)
lemma borel_sigma_sets_subset:
"A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
@@ -360,7 +329,7 @@
using X by (intro sigma_algebra.sigma_sets_subset[OF sigma_algebra_sigma_sets]) auto
finally show "sigma_sets UNIV {S. open S} \<subseteq> sigma_sets UNIV (F`A)" .
show "sigma_sets UNIV (F`A) \<subseteq> sigma_sets UNIV {S. open S}"
- unfolding borel_rev_eq using F by (intro borel_sigma_sets_subset) auto
+ by (metis F image_subset_iff sets_borel sigma_sets_mono)
qed auto
lemma borel_eq_sigmaI2:
@@ -371,7 +340,7 @@
assumes F: "\<And>i j. (i, j) \<in> A \<Longrightarrow> F i j \<in> sets borel"
shows "borel = sigma UNIV ((\<lambda>(i, j). F i j) ` A)"
using assms
- by (intro borel_eq_sigmaI1[where X="(\<lambda>(i, j). G i j) ` B" and F="(\<lambda>(i, j). F i j)"]) auto
+ by (smt (verit, del_insts) borel_eq_sigmaI1 image_iff prod.collapse split_beta)
lemma borel_eq_sigmaI3:
fixes F :: "'i \<Rightarrow> 'j \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
@@ -443,20 +412,15 @@
qed (auto simp: eq intro: generate_topology.Basis)
lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
- unfolding borel_def
-proof (intro sigma_eqI sigma_sets_eqI, safe)
- fix x :: "'a set" assume "open x"
- hence "x = UNIV - (UNIV - x)" by auto
- also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
- by (force intro: sigma_sets.Compl simp: \<open>open x\<close>)
- finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
-next
- fix x :: "'a set" assume "closed x"
- hence "x = UNIV - (UNIV - x)" by auto
- also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
- by (force intro: sigma_sets.Compl simp: \<open>closed x\<close>)
- finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
-qed simp_all
+proof -
+ have "x \<in> sigma_sets UNIV (Collect closed)"
+ if "open x" for x :: "'a set"
+ by (metis that Compl_eq_Diff_UNIV closed_Compl double_complement mem_Collect_eq
+ sigma_sets.Basic sigma_sets.Compl)
+ then show ?thesis
+ unfolding borel_def
+ by (metis Pow_UNIV borel_closed mem_Collect_eq sets_borel sigma_eqI sigma_sets_eqI top_greatest)
+qed
proposition borel_eq_countable_basis:
fixes B::"'a::topological_space set set"
@@ -517,8 +481,7 @@
lemma borel_measurable_continuous_on_indicator:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "A \<in> sets borel \<Longrightarrow> continuous_on A f \<Longrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable borel"
- by (subst borel_measurable_restrict_space_iff[symmetric])
- (auto intro: borel_measurable_continuous_on_restrict)
+ using borel_measurable_continuous_on_restrict borel_measurable_restrict_space_iff inf_top.right_neutral by blast
lemma borel_measurable_Pair[measurable (raw)]:
fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
@@ -720,7 +683,7 @@
shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> borel_measurable M"
proof cases
assume "I = {}" then show ?thesis
- unfolding \<open>I = {}\<close> image_empty by simp
+ by (simp add: borel_measurable_const)
next
assume "I \<noteq> {}"
show ?thesis
@@ -742,7 +705,7 @@
shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
proof cases
assume "I = {}" then show ?thesis
- unfolding \<open>I = {}\<close> image_empty by simp
+ by (simp add: borel_measurable_const)
next
assume "I \<noteq> {}"
show ?thesis
@@ -1045,25 +1008,23 @@
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have i: "i \<in> Basis" by auto
- have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
- also have *: "{x::'a. a < x\<bullet>i} =
- (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
- proof (safe, simp_all add: eucl_less_def split: if_split_asm)
- fix x :: 'a
+ have **: "\<exists>y. \<forall>j\<in>Basis. j \<noteq> i \<longrightarrow> - real y < x \<bullet> j" if "a < x \<bullet> i" for x
+ proof -
obtain k where k: "Max ((\<bullet>) (- x) ` Basis) < real k"
using reals_Archimedean2 by blast
{ fix i :: 'a assume "i \<in> Basis"
then have "-x\<bullet>i < real k"
using k by (subst (asm) Max_less_iff) auto
then have "- real k < x\<bullet>i" by simp }
- then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> -real k < x \<bullet> ia"
+ then show ?thesis
by (auto intro!: exI[of _ k])
qed
- finally show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
- apply (simp only:)
- apply (intro sets.countable_UN sets.Diff)
- apply (auto intro: sigma_sets_top)
- done
+ have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
+ also have *: "{x::'a. a < x\<bullet>i} = (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -k) *\<^sub>R n) <e x})"
+ using i ** by (force simp add: eucl_less_def split: if_split_asm)
+ finally have eq: "{x. x \<bullet> i \<le> a} = UNIV - (\<Union>x. {xa. (\<Sum>n\<in>Basis. (if n = i then a else - real x) *\<^sub>R n) <e xa})" .
+ show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
+ unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
qed auto
lemma borel_eq_lessThan:
@@ -1072,24 +1033,26 @@
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have i: "i \<in> Basis" by auto
- have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
- also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
- proof (safe, simp_all add: eucl_less_def split: if_split_asm)
- fix x :: 'a
+ have **: "\<exists>y. \<forall>j\<in>Basis. j \<noteq> i \<longrightarrow> real y > x \<bullet> j" if "a > x \<bullet> i" for x
+ proof -
obtain k where k: "Max ((\<bullet>) x ` Basis) < real k"
using reals_Archimedean2 by blast
{ fix i :: 'a assume "i \<in> Basis"
then have "x\<bullet>i < real k"
using k by (subst (asm) Max_less_iff) auto
then have "x\<bullet>i < real k" by simp }
- then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia < real k"
+ then show ?thesis
by (auto intro!: exI[of _ k])
qed
- finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
- apply (simp only:)
- apply (intro sets.countable_UN sets.Diff)
- apply (auto intro: sigma_sets_top )
- done
+ have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
+ also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
+ using i ** by (force simp add: eucl_less_def split: if_split_asm)
+ finally
+ have eq: "{x. a \<le> x \<bullet> i} =
+ UNIV - (\<Union>k. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" .
+
+ show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
+ unfolding eq by (fastforce intro!: sigma_sets_top sets.Diff)
qed auto
lemma borel_eq_atLeastAtMost:
@@ -1276,9 +1239,7 @@
lemma borel_measurable_uminus_eq [simp]:
fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
shows "(\<lambda>x. - f x) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
-proof
- assume ?l from borel_measurable_uminus[OF this] show ?r by simp
-qed auto
+ by (smt (verit, ccfv_SIG) borel_measurable_uminus equation_minus_iff measurable_cong)
lemma affine_borel_measurable_vector:
fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
@@ -1294,8 +1255,10 @@
by (auto simp: algebra_simps)
hence "?S \<in> sets borel" by auto
moreover
- from \<open>b \<noteq> 0\<close> have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
- apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)
+ have "\<And>x. \<lbrakk>a + b *\<^sub>R f x \<in> S\<rbrakk> \<Longrightarrow> f x \<in> (\<lambda>x. (x - a) /\<^sub>R b) ` S"
+ using \<open>b \<noteq> 0\<close> image_iff by fastforce
+ with \<open>b \<noteq> 0\<close> have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
+ by auto
ultimately show ?thesis using assms unfolding in_borel_measurable_borel
by auto
qed simp
@@ -1313,10 +1276,12 @@
fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
assumes f: "f \<in> borel_measurable M"
shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
- apply (rule measurable_compose[OF f])
- apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
- apply (auto intro!: continuous_on_inverse continuous_on_id)
- done
+proof -
+ have "countable {0::'b}" "continuous_on (- {0::'b}) inverse"
+ by (auto intro!: continuous_on_inverse continuous_on_id)
+ then show ?thesis
+ by (metis borel_measurable_continuous_countable_exceptions f measurable_compose)
+qed
lemma borel_measurable_divide[measurable (raw)]:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
@@ -1341,10 +1306,8 @@
lemma borel_measurable_ln[measurable (raw)]:
assumes f: "f \<in> borel_measurable M"
shows "(\<lambda>x. ln (f x :: real)) \<in> borel_measurable M"
- apply (rule measurable_compose[OF f])
- apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
- apply (auto intro!: continuous_on_ln continuous_on_id)
- done
+ using borel_measurable_continuous_countable_exceptions[of "{0}"] measurable_compose[OF f]
+ by (auto intro!: continuous_on_ln continuous_on_id)
lemma borel_measurable_log[measurable (raw)]:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
@@ -1402,12 +1365,16 @@
lemma\<^marker>\<open>tag important\<close> borel_measurable_complex_iff:
"f \<in> borel_measurable M \<longleftrightarrow>
- (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M"
- apply auto
- apply (subst fun_complex_eq)
- apply (intro borel_measurable_add)
- apply auto
- done
+ (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ using borel_measurable_Im borel_measurable_Re measurable_compose by blast
+ assume R: ?rhs
+ then have "(\<lambda>x. complex_of_real (Re (f x)) + \<i> * complex_of_real (Im (f x))) \<in> borel_measurable M"
+ by (intro borel_measurable_add) auto
+ then show ?lhs
+ using complex_eq by force
+qed
lemma powr_real_measurable [measurable]:
assumes "f \<in> measurable M borel" "g \<in> measurable M borel"
@@ -1427,10 +1394,8 @@
fixes f :: "'a \<Rightarrow> ereal"
assumes f: "f \<in> borel_measurable M"
shows "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M"
- apply (rule measurable_compose[OF f])
- apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"])
- apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
- done
+ using measurable_compose[OF f] borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"]
+ by (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
lemma borel_measurable_ereal_cases:
fixes f :: "'a \<Rightarrow> ereal"
@@ -1451,10 +1416,8 @@
by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
lemma borel_measurable_uminus_eq_ereal[simp]:
- "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
-proof
- assume ?l from borel_measurable_uminus_ereal[OF this] show ?r by simp
-qed auto
+ "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
+ by (smt (verit, ccfv_SIG) borel_measurable_uminus_ereal ereal_uminus_uminus measurable_cong)
lemma set_Collect_ereal2:
fixes f g :: "'a \<Rightarrow> ereal"
@@ -1511,13 +1474,7 @@
lemma vimage_sets_compl_iff:
"f -` A \<inter> space M \<in> sets M \<longleftrightarrow> f -` (- A) \<inter> space M \<in> sets M"
-proof -
- { fix A assume "f -` A \<inter> space M \<in> sets M"
- moreover have "f -` (- A) \<inter> space M = space M - f -` A \<inter> space M" by auto
- ultimately have "f -` (- A) \<inter> space M \<in> sets M" by auto }
- from this[of A] this[of "-A"] show ?thesis
- by (metis double_complement)
-qed
+ by (metis Diff_Compl Diff_Diff_Int diff_eq inf_aci(1) sets.Diff sets.top vimage_Compl)
lemma borel_measurable_iff_Iic_ereal:
"(f::'a\<Rightarrow>ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
@@ -1741,7 +1698,7 @@
lemma Collect_closed_imp_pred_borel: "closed {x. P x} \<Longrightarrow> Measurable.pred borel P"
by (simp add: pred_def)
-(* Proof by Jeremy Avigad and Luke Serafin *)
+text \<open>Proof by Jeremy Avigad and Luke Serafin\<close>
lemma isCont_borel_pred[measurable]:
fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
shows "Measurable.pred borel (isCont f)"
@@ -1821,12 +1778,19 @@
fixes f :: "real \<Rightarrow> real" and A :: "real set"
assumes "mono_on A f"
shows "f \<in> borel_measurable (restrict_space borel A)"
- apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]])
- apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space)
- apply (auto simp add: sets_restrict_restrict_space continuous_on_eq_continuous_within
- cong: measurable_cong_sets
- intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
- done
+proof -
+ have "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets (restrict_space borel A)"
+ using sets_restrict_space by fastforce
+ moreover
+ have "continuous_on (A \<inter> - {a \<in> A. \<not> continuous (at a within A) f}) f"
+ by (force simp: continuous_on_eq_continuous_within intro: continuous_within_subset)
+ then have "f \<in> borel_measurable (restrict_space (restrict_space borel A)
+ (- {a \<in> A. \<not> continuous (at a within A) f}))"
+ by (smt (verit, best) borel_measurable_continuous_on_restrict measurable_cong_sets sets_restrict_restrict_space)
+ ultimately show ?thesis
+ using measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]]
+ by (smt (verit, del_insts) UNIV_I mem_Collect_eq space_borel)
+qed
lemma borel_measurable_piecewise_mono:
fixes f::"real \<Rightarrow> real" and C::"real set set"
@@ -1920,7 +1884,6 @@
fixes f g::"_\<Rightarrow> 'a::{second_countable_topology, t2_space}"
assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
shows "{x \<in> space M. f x = g x} \<in> sets M"
-
proof -
define A where "A = {x \<in> space M. f x = g x}"
define B where "B = {y. \<exists>x::'a. y = (x,x)}"
@@ -1931,33 +1894,8 @@
then show ?thesis unfolding A_def by simp
qed
-lemma measurable_inequality_set [measurable]:
- fixes f g::"_ \<Rightarrow> 'a::{second_countable_topology, linorder_topology}"
- assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
- shows "{x \<in> space M. f x \<le> g x} \<in> sets M"
- "{x \<in> space M. f x < g x} \<in> sets M"
- "{x \<in> space M. f x \<ge> g x} \<in> sets M"
- "{x \<in> space M. f x > g x} \<in> sets M"
-proof -
- define F where "F = (\<lambda>x. (f x, g x))"
- have * [measurable]: "F \<in> borel_measurable M" unfolding F_def by simp
-
- have "{x \<in> space M. f x \<le> g x} = F-`{(x, y) | x y. x \<le> y} \<inter> space M" unfolding F_def by auto
- moreover have "{(x, y) | x y. x \<le> (y::'a)} \<in> sets borel" using closed_subdiagonal borel_closed by blast
- ultimately show "{x \<in> space M. f x \<le> g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-
- have "{x \<in> space M. f x < g x} = F-`{(x, y) | x y. x < y} \<inter> space M" unfolding F_def by auto
- moreover have "{(x, y) | x y. x < (y::'a)} \<in> sets borel" using open_subdiagonal borel_open by blast
- ultimately show "{x \<in> space M. f x < g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-
- have "{x \<in> space M. f x \<ge> g x} = F-`{(x, y) | x y. x \<ge> y} \<inter> space M" unfolding F_def by auto
- moreover have "{(x, y) | x y. x \<ge> (y::'a)} \<in> sets borel" using closed_superdiagonal borel_closed by blast
- ultimately show "{x \<in> space M. f x \<ge> g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-
- have "{x \<in> space M. f x > g x} = F-`{(x, y) | x y. x > y} \<inter> space M" unfolding F_def by auto
- moreover have "{(x, y) | x y. x > (y::'a)} \<in> sets borel" using open_superdiagonal borel_open by blast
- ultimately show "{x \<in> space M. f x > g x} \<in> sets M" using * by (metis (mono_tags, lifting) measurable_sets)
-qed
+lemmas measurable_inequality_set [measurable] =
+ borel_measurable_le borel_measurable_less borel_measurable_le borel_measurable_less
proposition measurable_limit [measurable]:
fixes f::"nat \<Rightarrow> 'a \<Rightarrow> 'b::first_countable_topology"
@@ -2051,8 +1989,8 @@
lemma measurable_restrict_mono:
assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
-by (rule measurable_compose[OF measurable_restrict_space3 f])
- (insert \<open>B \<subseteq> A\<close>, auto)
+ by (rule measurable_compose[OF measurable_restrict_space3 f]) (use \<open>B \<subseteq> A\<close> in auto)
+
text \<open>The next one is a variation around \<open>measurable_piecewise_restrict\<close>.\<close>
@@ -2065,22 +2003,27 @@
fix B assume [measurable]: "B \<in> sets N"
{
fix n::nat
- obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
+ obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x"
+ using assms(3) by blast
then have *: "f-`B \<inter> A n = h-`B \<inter> A n" by auto
- have "h-`B \<inter> A n = h-`B \<inter> space M \<inter> A n" using assms(2) sets.sets_into_space by auto
- then have "h-`B \<inter> A n \<in> sets M" by simp
- then have "f-`B \<inter> A n \<in> sets M" using * by simp
+ have "h-`B \<inter> A n = h-`B \<inter> space M \<inter> A n"
+ using assms(2) sets.sets_into_space by auto
+ then have "f-`B \<inter> A n \<in> sets M"
+ by (simp add: "*")
}
- then have "(\<Union>n. f-`B \<inter> A n) \<in> sets M" by measurable
- moreover have "f-`B \<inter> space M = (\<Union>n. f-`B \<inter> A n)" using assms(2) by blast
+ then have "(\<Union>n. f-`B \<inter> A n) \<in> sets M"
+ by measurable
+ moreover have "f-`B \<inter> space M = (\<Union>n. f-`B \<inter> A n)"
+ using assms(2) by blast
ultimately show "f-`B \<inter> space M \<in> sets M" by simp
next
fix x assume "x \<in> space M"
- then obtain n where "x \<in> A n" using assms(2) by blast
- obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
- then have "f x = h x" using \<open>x \<in> A n\<close> by blast
- moreover have "h x \<in> space N" by (metis measurable_space \<open>x \<in> space M\<close> \<open>h \<in> measurable M N\<close>)
- ultimately show "f x \<in> space N" by simp
+ then obtain n where "x \<in> A n"
+ using assms(2) by blast
+ obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x"
+ using assms(3) by blast
+ then show "f x \<in> space N"
+ by (metis \<open>x \<in> A n\<close> \<open>x \<in> space M\<close> measurable_space)
qed
end
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Sat Aug 12 10:09:29 2023 +0100
@@ -138,25 +138,23 @@
fixes l::complex
assumes "(f \<longlongrightarrow> l) F" and "\<not> trivial_limit F" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
shows "l \<in> \<real>"
-proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
- show "eventually (\<lambda>x. f x \<in> \<real>) F"
- using assms(3, 4) by (auto intro: eventually_mono)
-qed
+ using Lim_in_closed_set[OF closed_complex_Reals] assms
+ by (smt (verit) eventually_mono)
lemma real_lim_sequentially:
fixes l::complex
shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
-by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
+ by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
lemma real_series:
fixes l::complex
shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
-unfolding sums_def
-by (metis real_lim_sequentially sum_in_Reals)
+ unfolding sums_def
+ by (metis real_lim_sequentially sum_in_Reals)
lemma Lim_null_comparison_Re:
assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
- by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
+ using Lim_null_comparison assms tendsto_Re by fastforce
subsection\<open>Holomorphic functions\<close>
@@ -191,25 +189,11 @@
lemma holomorphic_on_UN_open:
assumes "\<And>n. n \<in> I \<Longrightarrow> f holomorphic_on A n" "\<And>n. n \<in> I \<Longrightarrow> open (A n)"
shows "f holomorphic_on (\<Union>n\<in>I. A n)"
-proof -
- have "f field_differentiable at z within (\<Union>n\<in>I. A n)" if "z \<in> (\<Union>n\<in>I. A n)" for z
- proof -
- from that obtain n where "n \<in> I" "z \<in> A n"
- by blast
- hence "f holomorphic_on A n" "open (A n)"
- by (simp add: assms)+
- with \<open>z \<in> A n\<close> have "f field_differentiable at z"
- by (auto simp: holomorphic_on_open field_differentiable_def)
- thus ?thesis
- by (meson field_differentiable_at_within)
- qed
- thus ?thesis
- by (auto simp: holomorphic_on_def)
-qed
+ by (metis UN_E assms holomorphic_on_open open_UN)
lemma holomorphic_on_imp_continuous_on:
"f holomorphic_on s \<Longrightarrow> continuous_on s f"
- by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
+ using differentiable_imp_continuous_on holomorphic_on_imp_differentiable_on by blast
lemma holomorphic_closedin_preimage_constant:
assumes "f holomorphic_on D"
@@ -247,22 +231,15 @@
lemma constant_on_imp_holomorphic_on:
assumes "f constant_on A"
shows "f holomorphic_on A"
-proof -
- from assms obtain c where c: "\<forall>x\<in>A. f x = c"
- unfolding constant_on_def by blast
- have "f holomorphic_on A \<longleftrightarrow> (\<lambda>_. c) holomorphic_on A"
- by (intro holomorphic_cong) (use c in auto)
- thus ?thesis
- by simp
-qed
+ by (metis assms constant_on_def holomorphic_on_const holomorphic_transform)
lemma holomorphic_on_compose:
- "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
+ "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g \<circ> f) holomorphic_on s"
using field_differentiable_compose_within[of f _ s g]
by (auto simp: holomorphic_on_def)
lemma holomorphic_on_compose_gen:
- "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
+ "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g \<circ> f) holomorphic_on s"
by (metis holomorphic_on_compose holomorphic_on_subset)
lemma holomorphic_on_balls_imp_entire:
@@ -284,15 +261,10 @@
lemma holomorphic_on_balls_imp_entire':
assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
shows "f holomorphic_on B"
-proof (rule holomorphic_on_balls_imp_entire)
- {
- fix M :: real
- have "\<exists>x. x > max M 0" by (intro gt_ex)
- hence "\<exists>x>0. x > M" by auto
- }
- thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
- by (auto simp: not_le)
-qed (insert assms, auto)
+proof (rule holomorphic_on_balls_imp_entire)
+ show "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
+ by (meson greaterThan_iff gt_ex less_le_not_le order_le_less_trans)
+qed (use assms in auto)
lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on A \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on A"
by (metis field_differentiable_minus holomorphic_on_def)
@@ -357,8 +329,7 @@
lemma holomorphic_on_Un [holomorphic_intros]:
assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
shows "f holomorphic_on (A \<union> B)"
- using assms by (auto simp: holomorphic_on_def at_within_open[of _ A]
- at_within_open[of _ B] at_within_open[of _ "A \<union> B"] open_Un)
+ by (metis Un_iff assms holomorphic_on_open open_Un)
lemma holomorphic_on_If_Un [holomorphic_intros]:
assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B"
@@ -374,19 +345,16 @@
also have "g holomorphic_on B \<longleftrightarrow> ?h holomorphic_on B"
using assms by (intro holomorphic_cong) auto
finally show \<dots> .
-qed (insert assms, auto)
+qed (use assms in auto)
lemma holomorphic_derivI:
- "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
- \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
-by (metis DERIV_deriv_iff_field_differentiable at_within_open holomorphic_on_def has_field_derivative_at_within)
+ "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk> \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
+ by (metis DERIV_deriv_iff_field_differentiable at_within_open holomorphic_on_def has_field_derivative_at_within)
lemma complex_derivative_transform_within_open:
"\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
\<Longrightarrow> deriv f z = deriv g z"
- unfolding holomorphic_on_def
- by (rule DERIV_imp_deriv)
- (metis DERIV_deriv_iff_field_differentiable has_field_derivative_transform_within_open at_within_open)
+ by (smt (verit) DERIV_imp_deriv has_field_derivative_transform_within_open holomorphic_on_open)
lemma holomorphic_on_compose_cnj_cnj:
assumes "f holomorphic_on cnj ` A" "open A"
@@ -408,13 +376,13 @@
subsection\<open>Analyticity on a set\<close>
definition\<^marker>\<open>tag important\<close> analytic_on (infixl "(analytic'_on)" 50)
- where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
+ where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>\<epsilon>. 0 < \<epsilon> \<and> f holomorphic_on (ball x \<epsilon>)"
named_theorems\<^marker>\<open>tag important\<close> analytic_intros "introduction rules for proving analyticity"
lemma analytic_imp_holomorphic: "f analytic_on S \<Longrightarrow> f holomorphic_on S"
- by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
- (metis centre_in_ball field_differentiable_at_within)
+ unfolding analytic_on_def holomorphic_on_def
+ using centre_in_ball field_differentiable_at_within field_differentiable_within_open by blast
lemma analytic_on_open: "open S \<Longrightarrow> f analytic_on S \<longleftrightarrow> f holomorphic_on S"
by (meson analytic_imp_holomorphic analytic_on_def holomorphic_on_subset openE)
@@ -426,15 +394,12 @@
lemma analytic_at_imp_isCont:
assumes "f analytic_on {z}"
shows "isCont f z"
- using assms by (meson analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at insertI1)
+ by (meson analytic_on_imp_differentiable_at assms field_differentiable_imp_continuous_at insertCI)
lemma analytic_at_neq_imp_eventually_neq:
assumes "f analytic_on {x}" "f x \<noteq> c"
shows "eventually (\<lambda>y. f y \<noteq> c) (at x)"
-proof (intro tendsto_imp_eventually_ne)
- show "f \<midarrow>x\<rightarrow> f x"
- using assms by (simp add: analytic_at_imp_isCont isContD)
-qed (use assms in auto)
+ using analytic_at_imp_isCont assms isContD tendsto_imp_eventually_ne by blast
lemma analytic_on_subset: "f analytic_on S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> f analytic_on T"
by (auto simp: analytic_on_def)
@@ -455,18 +420,21 @@
have "?lhs \<longleftrightarrow> (\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T)"
proof safe
assume "f analytic_on S"
- then show "\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T"
- apply (simp add: analytic_on_def)
- apply (rule exI [where x="\<Union>{U. open U \<and> f analytic_on U}"], auto)
- apply (metis open_ball analytic_on_open centre_in_ball)
- by (metis analytic_on_def)
+ then have "\<forall>x \<in> \<Union>{U. open U \<and> f analytic_on U}. \<exists>\<epsilon>>0. f holomorphic_on ball x \<epsilon>"
+ using analytic_on_def by force
+ moreover have "S \<subseteq> \<Union>{U. open U \<and> f analytic_on U}"
+ using \<open>f analytic_on S\<close>
+ by (smt (verit, best) open_ball Union_iff analytic_on_def analytic_on_open centre_in_ball mem_Collect_eq subsetI)
+ ultimately show "\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T"
+ unfolding analytic_on_def
+ by (metis (mono_tags, lifting) mem_Collect_eq open_Union)
next
fix T
assume "open T" "S \<subseteq> T" "f analytic_on T"
then show "f analytic_on S"
by (metis analytic_on_subset)
qed
- also have "... \<longleftrightarrow> ?rhs"
+ also have "\<dots> \<longleftrightarrow> ?rhs"
by (auto simp: analytic_on_open)
finally show ?thesis .
qed
@@ -486,7 +454,7 @@
lemma analytic_on_compose:
assumes f: "f analytic_on S"
and g: "g analytic_on (f ` S)"
- shows "(g o f) analytic_on S"
+ shows "(g \<circ> f) analytic_on S"
unfolding analytic_on_def
proof (intro ballI)
fix x
@@ -500,21 +468,19 @@
with e' obtain d where d: "0 < d" and fd: "f ` ball x d \<subseteq> ball (f x) e'"
by (auto simp: continuous_at_ball)
have "g \<circ> f holomorphic_on ball x (min d e)"
- apply (rule holomorphic_on_compose)
- apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
- by (metis fd gh holomorphic_on_subset image_mono min.cobounded1 subset_ball)
+ by (meson fd fh gh holomorphic_on_compose_gen holomorphic_on_subset image_mono min.cobounded1 min.cobounded2 subset_ball)
then show "\<exists>e>0. g \<circ> f holomorphic_on ball x e"
by (metis d e min_less_iff_conj)
qed
lemma analytic_on_compose_gen:
"f analytic_on S \<Longrightarrow> g analytic_on T \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<in> T)
- \<Longrightarrow> g o f analytic_on S"
-by (metis analytic_on_compose analytic_on_subset image_subset_iff)
+ \<Longrightarrow> g \<circ> f analytic_on S"
+ by (metis analytic_on_compose analytic_on_subset image_subset_iff)
lemma analytic_on_neg [analytic_intros]:
"f analytic_on S \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on S"
-by (metis analytic_on_holomorphic holomorphic_on_minus)
+ by (metis analytic_on_holomorphic holomorphic_on_minus)
lemma analytic_on_add [analytic_intros]:
assumes f: "f analytic_on S"
@@ -529,33 +495,11 @@
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
by (metis analytic_on_def g z)
have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_add)
- apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
- by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
+ by (metis fh gh holomorphic_on_add holomorphic_on_subset linorder_linear min_def subset_ball)
then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e"
by (metis e e' min_less_iff_conj)
qed
-lemma analytic_on_diff [analytic_intros]:
- assumes f: "f analytic_on S"
- and g: "g analytic_on S"
- shows "(\<lambda>z. f z - g z) analytic_on S"
-unfolding analytic_on_def
-proof (intro ballI)
- fix z
- assume z: "z \<in> S"
- then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
- by (metis analytic_on_def)
- obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
- by (metis analytic_on_def g z)
- have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_diff)
- apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
- by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
- then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e"
- by (metis e e' min_less_iff_conj)
-qed
-
lemma analytic_on_mult [analytic_intros]:
assumes f: "f analytic_on S"
and g: "g analytic_on S"
@@ -569,13 +513,23 @@
obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
by (metis analytic_on_def g z)
have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_mult)
- apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
- by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
+ by (metis fh gh holomorphic_on_mult holomorphic_on_subset min.absorb_iff2 min_def subset_ball)
then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e"
by (metis e e' min_less_iff_conj)
qed
+lemma analytic_on_diff [analytic_intros]:
+ assumes f: "f analytic_on S" and g: "g analytic_on S"
+ shows "(\<lambda>z. f z - g z) analytic_on S"
+proof -
+ have "(\<lambda>z. - g z) analytic_on S"
+ by (simp add: analytic_on_neg g)
+ then have "(\<lambda>z. f z + - g z) analytic_on S"
+ using analytic_on_add f by blast
+ then show ?thesis
+ by fastforce
+qed
+
lemma analytic_on_inverse [analytic_intros]:
assumes f: "f analytic_on S"
and nz: "(\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0)"
@@ -591,24 +545,20 @@
then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
by (metis open_ball centre_in_ball continuous_on_open_avoid e z nz)
have "(\<lambda>z. inverse (f z)) holomorphic_on ball z (min e e')"
- apply (rule holomorphic_on_inverse)
- apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball)
- by (metis nz' mem_ball min_less_iff_conj)
+ using fh holomorphic_on_inverse holomorphic_on_open nz' by fastforce
then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e"
by (metis e e' min_less_iff_conj)
qed
lemma analytic_on_divide [analytic_intros]:
- assumes f: "f analytic_on S"
- and g: "g analytic_on S"
- and nz: "(\<And>z. z \<in> S \<Longrightarrow> g z \<noteq> 0)"
- shows "(\<lambda>z. f z / g z) analytic_on S"
-unfolding divide_inverse
-by (metis analytic_on_inverse analytic_on_mult f g nz)
+ assumes f: "f analytic_on S" and g: "g analytic_on S"
+ and nz: "(\<And>z. z \<in> S \<Longrightarrow> g z \<noteq> 0)"
+ shows "(\<lambda>z. f z / g z) analytic_on S"
+ unfolding divide_inverse by (metis analytic_on_inverse analytic_on_mult f g nz)
lemma analytic_on_power [analytic_intros]:
"f analytic_on S \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on S"
-by (induct n) (auto simp: analytic_on_mult)
+ by (induct n) (auto simp: analytic_on_mult)
lemma analytic_on_power_int [analytic_intros]:
assumes nz: "n \<ge> 0 \<or> (\<forall>x\<in>A. f x \<noteq> 0)" and f: "f analytic_on A"
@@ -645,15 +595,15 @@
proof -
have "deriv f w * deriv g (f w) = deriv g (f w) * deriv f w"
by (simp add: algebra_simps)
- also have "... = deriv (g o f) w"
+ also have "\<dots> = deriv (g \<circ> f) w"
using assms
by (metis analytic_on_imp_differentiable_at analytic_on_open deriv_chain image_subset_iff)
- also have "... = deriv id w"
+ also have "\<dots> = deriv id w"
proof (rule complex_derivative_transform_within_open [where s=S])
show "g \<circ> f holomorphic_on S"
by (rule assms holomorphic_on_compose_gen holomorphic_intros)+
qed (use assms in auto)
- also have "... = 1"
+ also have "\<dots> = 1"
by simp
finally show ?thesis .
qed
@@ -679,19 +629,16 @@
lemma analytic_at_two:
"f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
- (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s \<and> g holomorphic_on s)"
+ (\<exists>S. open S \<and> z \<in> S \<and> f holomorphic_on S \<and> g holomorphic_on S)"
(is "?lhs = ?rhs")
proof
assume ?lhs
- then obtain s t
- where st: "open s" "z \<in> s" "f holomorphic_on s"
- "open t" "z \<in> t" "g holomorphic_on t"
+ then obtain S T
+ where st: "open S" "z \<in> S" "f holomorphic_on S"
+ "open T" "z \<in> T" "g holomorphic_on T"
by (auto simp: analytic_at)
- show ?rhs
- apply (rule_tac x="s \<inter> t" in exI)
- using st
- apply (auto simp: holomorphic_on_subset)
- done
+ then show ?rhs
+ by (metis Int_iff holomorphic_on_subset inf_le1 inf_le2 open_Int)
next
assume ?rhs
then show ?lhs
@@ -707,32 +654,23 @@
and complex_derivative_mult_at: "deriv (\<lambda>w. f w * g w) z =
f z * deriv g z + deriv f z * g z"
proof -
- obtain s where s: "open s" "z \<in> s" "f holomorphic_on s" "g holomorphic_on s"
- using assms by (metis analytic_at_two)
show "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
- apply (rule DERIV_imp_deriv [OF DERIV_add])
- using s
- apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
- done
+ using analytic_on_imp_differentiable_at assms by auto
show "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
- apply (rule DERIV_imp_deriv [OF DERIV_diff])
- using s
- apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
- done
- show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
- apply (rule DERIV_imp_deriv [OF DERIV_mult'])
- using s
- apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
- done
+ using analytic_on_imp_differentiable_at assms by force
+ obtain S where "open S" "z \<in> S" "f holomorphic_on S" "g holomorphic_on S"
+ using assms by (metis analytic_at_two)
+ then show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
+ by (simp add: DERIV_imp_deriv [OF DERIV_mult'] holomorphic_derivI)
qed
lemma deriv_cmult_at:
"f analytic_on {z} \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
-by (auto simp: complex_derivative_mult_at)
+ by (auto simp: complex_derivative_mult_at)
lemma deriv_cmult_right_at:
"f analytic_on {z} \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
-by (auto simp: complex_derivative_mult_at)
+ by (auto simp: complex_derivative_mult_at)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Complex differentiation of sequences and series\<close>
@@ -748,27 +686,16 @@
proof -
from assms obtain x l where x: "x \<in> S" and tf: "((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially"
by blast
- { fix e::real assume e: "e > 0"
- then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> S \<longrightarrow> cmod (f' n x - g' x) \<le> e"
- by (metis conv)
- have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
- proof (rule exI [of _ N], clarify)
- fix n y h
- assume "N \<le> n" "y \<in> S"
- then have "cmod (f' n y - g' y) \<le> e"
- by (metis N)
- then have "cmod h * cmod (f' n y - g' y) \<le> cmod h * e"
- by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
- then show "cmod (f' n y * h - g' y * h) \<le> e * cmod h"
- by (simp add: norm_mult [symmetric] field_simps)
- qed
- } note ** = this
show ?thesis
unfolding has_field_derivative_def
proof (rule has_derivative_sequence [OF cvs _ _ x])
show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
by (rule tf)
- next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
+ next
+ have **: "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> \<epsilon> * cmod h"
+ if "\<epsilon> > 0" for \<epsilon>::real
+ by (metis that left_diff_distrib mult_right_mono norm_ge_zero norm_mult conv)
+ show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
unfolding eventually_sequentially by (blast intro: **)
qed (metis has_field_derivative_def df)
qed
@@ -784,19 +711,17 @@
proof -
from assms obtain x l where x: "x \<in> S" and sf: "((\<lambda>n. f n x) sums l)"
by blast
- { fix e::real assume e: "e > 0"
+ { fix \<epsilon>::real assume e: "\<epsilon> > 0"
then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> S
- \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
+ \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> \<epsilon>"
by (metis conv)
- have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
+ have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> \<epsilon> * cmod h"
proof (rule exI [of _ N], clarify)
fix n y h
assume "N \<le> n" "y \<in> S"
- then have "cmod ((\<Sum>i<n. f' i y) - g' y) \<le> e"
- by (metis N)
- then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e"
- by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
- then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
+ have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * \<epsilon>"
+ by (simp add: N \<open>N \<le> n\<close> \<open>y \<in> S\<close> mult_le_cancel_left)
+ then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> \<epsilon> * cmod h"
by (simp add: norm_mult [symmetric] field_simps sum_distrib_left)
qed
} note ** = this
@@ -818,8 +743,8 @@
lemma sum_Suc_reindex:
fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
- shows "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
-by (induct n) auto
+ shows "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
+ by (induct n) auto
lemma field_Taylor:
assumes S: "convex S"
@@ -836,7 +761,7 @@
assume "u \<in> closed_segment w z"
then have "u \<in> S"
by (metis wzs subsetD)
- have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
+ have *: "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
f (Suc i) u * (z-u)^i / (fact i)) =
f (Suc n) u * (z-u) ^ n / (fact n)"
proof (induction n)
@@ -849,7 +774,7 @@
f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) -
f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))"
using Suc by simp
- also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
+ also have "\<dots> = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
proof -
have "(fact(Suc n)) *
(f(Suc n) u *(z-u) ^ n / (fact n) +
@@ -859,29 +784,26 @@
((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
by (simp add: algebra_simps del: fact_Suc)
- also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
+ also have "\<dots> = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
(f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
(f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
by (simp del: fact_Suc)
- also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
+ also have "\<dots> = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
(f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
(f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
by (simp only: fact_Suc of_nat_mult ac_simps) simp
- also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
+ also have "\<dots> = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
by (simp add: algebra_simps)
finally show ?thesis
by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact_Suc)
qed
finally show ?case .
qed
- then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
+ have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
(at u within S)"
- apply (intro derivative_eq_intros)
- apply (blast intro: assms \<open>u \<in> S\<close>)
- apply (rule refl)+
- apply (auto simp: field_simps)
- done
+ unfolding * [symmetric]
+ by (rule derivative_eq_intros assms \<open>u \<in> S\<close> refl | auto simp: field_simps)+
} note sum_deriv = this
{ fix u
assume u: "u \<in> closed_segment w z"
@@ -889,9 +811,9 @@
by (metis wzs subsetD)
have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> norm (f (Suc n) u) * norm (u - z) ^ n"
by (metis norm_minus_commute order_refl)
- also have "... \<le> norm (f (Suc n) u) * norm (z - w) ^ n"
+ also have "\<dots> \<le> norm (f (Suc n) u) * norm (z - w) ^ n"
by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u])
- also have "... \<le> B * norm (z - w) ^ n"
+ also have "\<dots> \<le> B * norm (z - w) ^ n"
by (metis norm_ge_zero zero_le_power mult_right_mono B [OF us])
finally have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> B * norm (z - w) ^ n" .
} note cmod_bound = this
@@ -903,14 +825,14 @@
\<le> norm ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
by (simp add: norm_minus_commute)
- also have "... \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)"
- apply (rule field_differentiable_bound
- [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
- and S = "closed_segment w z", OF convex_closed_segment])
- apply (auto simp: DERIV_subset [OF sum_deriv wzs]
- norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
- done
- also have "... \<le> B * norm (z - w) ^ Suc n / (fact n)"
+ also have "\<dots> \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)"
+ proof (rule field_differentiable_bound)
+ show "\<And>x. x \<in> closed_segment w z \<Longrightarrow>
+ ((\<lambda>\<xi>. \<Sum>i\<le>n. f i \<xi> * (z - \<xi>) ^ i / fact i) has_field_derivative f (Suc n) x * (z - x) ^ n / fact n)
+ (at x within closed_segment w z)"
+ using DERIV_subset sum_deriv wzs by blast
+ qed (auto simp: norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
+ also have "\<dots> \<le> B * norm (z - w) ^ Suc n / (fact n)"
by (simp add: algebra_simps norm_minus_commute)
finally show ?thesis .
qed
@@ -921,8 +843,7 @@
and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
and w: "w \<in> S"
and z: "z \<in> S"
- shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
- \<le> B * cmod(z - w)^(Suc n) / fact n"
+ shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i))) \<le> B * cmod(z - w)^(Suc n) / fact n"
using assms by (rule field_Taylor)
@@ -932,20 +853,22 @@
assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
shows "\<exists>u. u \<in> closed_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
proof -
- have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
- by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
+ define \<phi> where "\<phi> \<equiv> \<lambda>t. (1 - t) *\<^sub>R w + t *\<^sub>R z"
+ have twz: "\<And>t. \<phi> t = w + t *\<^sub>R (z - w)"
+ by (simp add: \<phi>_def real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
note assms[unfolded has_field_derivative_def, derivative_intros]
- show ?thesis
- apply (cut_tac mvt_simple
- [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w + t *\<^sub>R z)"
- "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
- apply auto
- apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
- apply (auto simp: closed_segment_def twz) []
- apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
- apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
- apply (force simp: twz closed_segment_def)
- done
+ have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk>
+ \<Longrightarrow> (Re \<circ> f \<circ> \<phi> has_derivative Re \<circ> (*) (f' (\<phi> x)) \<circ> (\<lambda>t. t *\<^sub>R (z - w)))
+ (at x within {0..1})"
+ unfolding \<phi>_def
+ by (intro derivative_eq_intros has_derivative_at_withinI)
+ (auto simp: in_segment scaleR_right_diff_distrib)
+ obtain x where "0<x" "x<1" "(Re \<circ> f \<circ> \<phi>) 1 -
+ (Re \<circ> f \<circ> \<phi>) 0 = (Re \<circ> (*) (f' (\<phi> x)) \<circ> (\<lambda>t. t *\<^sub>R (z - w))) (1 - 0)"
+ using mvt_simple [OF zero_less_one *] by force
+ then show ?thesis
+ unfolding \<phi>_def
+ by (smt (verit) comp_apply in_segment(1) scaleR_left_distrib scaleR_one scaleR_zero_left)
qed
lemma complex_Taylor_mvt:
@@ -967,30 +890,27 @@
(f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
(fact (Suc i)))"
by (subst sum_Suc_reindex) simp
- also have "... = f (Suc 0) u -
+ also have "\<dots> = f (Suc 0) u -
(f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
(fact (Suc n)) +
(\<Sum>i = 0..n.
f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i)) -
f (Suc i) u * (z-u) ^ i / (fact i))"
by (simp only: diff_divide_distrib fact_cancel ac_simps)
- also have "... = f (Suc 0) u -
+ also have "\<dots> = f (Suc 0) u -
(f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
(fact (Suc n)) +
f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
by (subst sum_Suc_diff) auto
- also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
+ also have "\<dots> = f (Suc n) u * (z-u) ^ n / (fact n)"
by (simp only: algebra_simps diff_divide_distrib fact_cancel)
- finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
+ finally have *: "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
- of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) =
f (Suc n) u * (z - u) ^ n / (fact n)" .
- then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
+ have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
f (Suc n) u * (z - u) ^ n / (fact n)) (at u)"
- apply (intro derivative_eq_intros)+
- apply (force intro: u assms)
- apply (rule refl)+
- apply (auto simp: ac_simps)
- done
+ unfolding * [symmetric]
+ by (rule derivative_eq_intros assms u refl | auto simp: field_simps)+
}
then show ?thesis
apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / (fact i)"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Sat Aug 12 10:09:29 2023 +0100
@@ -437,7 +437,7 @@
then obtain L where L: "subspace L" "affine_parallel S L"
using assms affine_parallel_subspace[of S] by auto
then obtain a where a: "S = ((+) a ` L)"
- using affine_parallel_def[of L S] affine_parallel_commut by auto
+ using affine_parallel_def[of L S] affine_parallel_commute by auto
from L have "closed L" using closed_subspace by auto
then have "closed S"
using closed_translation a by auto
--- a/src/HOL/Analysis/Elementary_Topology.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Sat Aug 12 10:09:29 2023 +0100
@@ -1692,20 +1692,15 @@
(\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
lemma seq_compactI:
- assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
shows "seq_compact S"
unfolding seq_compact_def using assms by fast
lemma seq_compactE:
assumes "seq_compact S" "\<forall>n. f n \<in> S"
- obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+ obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "(f \<circ> r) \<longlonglongrightarrow> l"
using assms unfolding seq_compact_def by fast
-lemma closed_sequentially: (* TODO: move upwards *)
- assumes "closed S" and "\<And>n. f n \<in> S" and "f \<longlonglongrightarrow> l"
- shows "l \<in> S"
- by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)
-
lemma seq_compact_Int_closed:
assumes "seq_compact S" and "closed T"
shows "seq_compact (S \<inter> T)"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Aug 12 10:09:29 2023 +0100
@@ -1373,7 +1373,7 @@
obtain a where "a \<in> interior (convex hull insert 0 B)"
proof (rule interior_simplex_nonempty [OF indB])
show "finite B"
- by (simp add: indB independent_finite)
+ by (simp add: indB independent_imp_finite)
show "card B = DIM('N)"
by (simp add: cardB 2)
qed
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Sat Aug 12 10:09:29 2023 +0100
@@ -8,9 +8,11 @@
imports Binary_Product_Measure Function_Topology
begin
-lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
- by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
- (force intro: exI[of _ "restrict f I" for f])
+lemma Pi_choice: "(\<forall>i\<in>I. \<exists>x\<in>F i. P i x) \<longleftrightarrow> (\<exists>f\<in>Pi I F. \<forall>i\<in>I. P i (f i))"
+ by (metis Pi_iff)
+
+lemma PiE_choice: "(\<forall>i\<in>I. \<exists>x\<in>F i. P i x) \<longleftrightarrow>(\<exists>f\<in>Pi\<^sub>E I F. \<forall>i\<in>I. P i (f i))"
+ unfolding Pi_choice by (metis Int_iff PiE_def restrict_PiE restrict_apply)
lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
by auto
@@ -97,7 +99,7 @@
then show "x \<in> A \<longleftrightarrow> x \<in> B"
using y x \<open>J \<subseteq> I\<close> PiE_cancel_merge[of "J" "I - J" x y S]
by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
- qed (insert sets, auto)
+ qed (use sets in auto)
qed
lemma restrict_vimage:
@@ -178,7 +180,7 @@
lemma Pi_cong_sets:
"\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
- unfolding Pi_def by auto
+ by auto
lemma PiM_cong:
assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
@@ -327,17 +329,11 @@
done
qed
proposition prod_algebra_cong:
- assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
+ assumes "I = J" and "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
shows "prod_algebra I M = prod_algebra J N"
-proof -
- have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
- using sets_eq_imp_space_eq[OF sets] by auto
- with sets show ?thesis unfolding \<open>I = J\<close>
- by (intro antisym prod_algebra_mono) auto
-qed
+ by (metis assms prod_algebra_mono sets_eq_imp_space_eq subsetI subset_antisym)
-lemma space_in_prod_algebra:
- "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
+lemma space_in_prod_algebra: "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
proof cases
assume "I = {}" then show ?thesis
by (auto simp add: prod_algebra_def image_iff prod_emb_def)
@@ -346,9 +342,8 @@
then obtain i where "i \<in> I" by auto
then have "(\<Pi>\<^sub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
by (auto simp: prod_emb_def)
- also have "\<dots> \<in> prod_algebra I M"
- using \<open>i \<in> I\<close> by (intro prod_algebraI) auto
- finally show ?thesis .
+ then show ?thesis
+ by (simp add: \<open>i \<in> I\<close> prod_algebraI)
qed
lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
@@ -383,8 +378,8 @@
show "A \<in> sigma_sets ?\<Omega> ?R"
proof cases
assume "I = {}"
- with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
- with \<open>I = {}\<close> show ?thesis by (auto intro!: sigma_sets_top)
+ with X show ?thesis
+ by (metis (no_types, lifting) PiE_cong R.top empty_iff prod_emb_PiE subset_eq)
next
assume "I \<noteq> {}"
with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^sub>E i\<in>I. space (M i)). f j \<in> X j})"
@@ -405,16 +400,25 @@
qed
lemma sets_PiM_eq_proj:
- "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
- apply (simp add: sets_PiM_single)
- apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
- apply auto []
- apply auto []
- apply simp
- apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
- apply (rule sets_vimage_algebra2)
- apply (auto intro!: arg_cong2[where f=sigma_sets])
- done
+ assumes "I \<noteq> {}"
+ shows "sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs =
+ sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
+ by (simp add: sets_PiM_single)
+ also have "\<dots> = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+ (\<Union>x\<in>I. sets (vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>xa. xa x) (M x)))"
+ apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
+ apply (rule sets_vimage_algebra2)
+ by (auto intro!: arg_cong2[where f=sigma_sets])
+ also have "... = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
+ (\<Union> (sets ` (\<lambda>i. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i)) ` I))"
+ by simp
+ also have "... = ?rhs"
+ by (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"]) (use assms in auto)
+ finally show ?thesis .
+qed
lemma
shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
@@ -616,7 +620,7 @@
by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm)
then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)"
using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I)
-qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM)
+qed (use \<open>i \<in> I\<close> in \<open>auto simp: space_PiM\<close>)
lemma measurable_component_singleton'[measurable_dest]:
assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
@@ -696,7 +700,10 @@
by auto
then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
using A X by (auto intro!: measurable_sets)
-qed (insert X, auto simp add: PiE_def dest: measurable_space)
+next
+ show "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
+ using X by (auto simp add: PiE_def dest: measurable_space)
+qed
lemma measurable_abs_UNIV:
"(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
@@ -708,13 +715,7 @@
lemma measurable_restrict_subset':
assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
-proof-
- from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
- by (rule measurable_restrict_subset)
- also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
- by (intro sets_PiM_cong measurable_cong_sets) simp_all
- finally show ?thesis .
-qed
+ by (metis (no_types) assms measurable_cong_sets measurable_restrict_subset sets_PiM_cong)
lemma measurable_prod_emb[intro, simp]:
"J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
@@ -754,11 +755,7 @@
lemma sets_in_extensional_aux:
"{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
-proof -
- have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
- by (auto simp add: extensional_def space_PiM)
- then show ?thesis by simp
-qed
+ by (smt (verit) PiE_iff mem_Collect_eq sets.top space_PiM subsetI subset_antisym)
lemma sets_in_extensional[measurable (raw)]:
"f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
@@ -772,7 +769,7 @@
then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))"
using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
also have "\<dots> \<in> sets (PiM I M)"
- using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
+ using I \<open>I \<noteq> {}\<close> by (simp add: E sets.countable_INT' sets_PiM_I subset_eq)
finally show ?thesis .
qed (simp add: sets_PiM_empty)
@@ -805,8 +802,9 @@
and K: "\<And>i. K i = prod_emb I M (J i) (X i)"
by (metis Union.IH)
show ?case
- proof (intro exI[of _ "\<Union>i. J i"] bexI[of _ "\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i)"] conjI)
- show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" using J by auto
+ proof (intro exI bexI conjI)
+ show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)"
+ using J by auto
with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))"
by (simp add: K[abs_def] SUP_upper)
qed(auto intro: X)
@@ -1010,7 +1008,7 @@
in_space: "\<And>j. space (M j) = \<Union>(F j)"
using sigma_finite_countable by (metis subset_eq)
moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
- using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
+ using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD1])
ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
by (intro exI[of _ "Pi\<^sub>E I ` Pi\<^sub>E I F"])
(auto intro!: countable_PiE sets_PiM_I_finite
@@ -1042,26 +1040,26 @@
(\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
by (subst emeasure_distr)
(auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
-qed (insert fin, simp_all)
+qed (use fin in simp_all)
proposition (in product_sigma_finite) product_nn_integral_fold:
assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
and f[measurable]: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
- shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
- (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
+shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
+ (is "?lhs = ?rhs")
proof -
interpret I: finite_product_sigma_finite M I by standard fact
interpret J: finite_product_sigma_finite M J by standard fact
interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
- show ?thesis
- apply (subst distr_merge[OF IJ, symmetric])
- apply (subst nn_integral_distr[OF measurable_merge])
- apply measurable []
- apply (subst J.nn_integral_fst[symmetric, OF P_borel])
- apply simp
- done
+ have "?lhs = integral\<^sup>N (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) f"
+ by (simp add: I.finite_index J.finite_index assms(1) distr_merge)
+ also have "... = \<integral>\<^sup>+ x. f (merge I J x) \<partial>(Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
+ by (simp add: nn_integral_distr)
+ also have "... = ?rhs"
+ using P.Fubini P.nn_integral_snd by force
+ finally show ?thesis .
qed
lemma (in product_sigma_finite) distr_singleton:
@@ -1082,10 +1080,7 @@
proof -
interpret I: finite_product_sigma_finite M "{i}" by standard simp
from f show ?thesis
- apply (subst distr_singleton[symmetric])
- apply (subst nn_integral_distr[OF measurable_component_singleton])
- apply simp_all
- done
+ by (metis distr_singleton insert_iff measurable_component_singleton nn_integral_distr)
qed
proposition (in product_sigma_finite) product_nn_integral_insert:
@@ -1118,8 +1113,7 @@
shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
apply (subst product_nn_integral_insert[OF assms])
apply (rule pair_sigma_finite.Fubini')
- apply intro_locales []
- apply (rule sigma_finite[OF I(1)])
+ apply (simp add: local.sigma_finite pair_sigma_finite.intro sigma_finite_measures)
apply measurable
done
@@ -1139,11 +1133,8 @@
measurable_comp[OF measurable_component_singleton, unfolded comp_def])
auto
then show ?case
- apply (simp add: product_nn_integral_insert[OF insert(1,2)])
- apply (simp add: insert(2-) * nn_integral_multc)
- apply (subst nn_integral_cmult)
- apply (auto simp add: insert(2-))
- done
+ using product_nn_integral_insert[OF insert(1,2)]
+ by (simp add: insert(2-) * nn_integral_multc nn_integral_cmult)
qed (simp add: space_PiM)
proposition (in product_sigma_finite) product_nn_integral_pair:
@@ -1176,7 +1167,8 @@
lemma (in product_sigma_finite)
assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
shows emeasure_fold_integral:
- "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)" (is ?I)
+ "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)"
+ (is "?lhs = ?rhs")
and emeasure_fold_measurable:
"(\<lambda>x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M))) \<in> borel_measurable (Pi\<^sub>M I M)" (is ?B)
proof -
@@ -1185,13 +1177,14 @@
interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
have merge: "merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) \<in> sets (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
by (intro measurable_sets[OF _ A] measurable_merge assms)
-
- show ?I
- apply (subst distr_merge[symmetric, OF IJ])
- apply (subst emeasure_distr[OF measurable_merge A])
+ have "?lhs = emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) A"
+ by (simp add: I.finite_index J.finite_index assms(1) distr_merge)
+ also have "... = emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M))"
+ by (meson A emeasure_distr measurable_merge)
+ also have "... = ?rhs"
apply (subst J.emeasure_pair_measure_alt[OF merge])
- apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
- done
+ by (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
+ finally show "?lhs = ?rhs" .
show ?B
using IJ.measurable_emeasure_Pair1[OF merge]
@@ -1201,7 +1194,6 @@
lemma sets_Collect_single:
"i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
by simp
-
lemma pair_measure_eq_distr_PiM:
fixes M1 :: "'a measure" and M2 :: "'a measure"
assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
@@ -1282,7 +1274,7 @@
{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
proof
have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
- proof (auto)
+ proof clarify
fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
then have *: "X i \<in> sets (M i)" for i by simp
define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
@@ -1315,9 +1307,7 @@
qed
show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
unfolding sets_PiM_single
- apply (rule sigma_sets_mono')
- apply (auto simp add: PiE_iff *)
- done
+ by (intro sigma_sets_mono') (auto simp add: PiE_iff *)
qed
lemma sets_PiM_subset_borel:
@@ -1361,7 +1351,7 @@
ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
qed
have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
- apply (rule sets.sigma_sets_subset') using ** by auto
+ by (metis "**" mem_Collect_eq open_UNIV sets.sigma_sets_subset' subsetI)
then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
unfolding borel_def by auto
qed (simp add: sets_PiM_subset_borel)
--- a/src/HOL/Analysis/Further_Topology.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Sat Aug 12 10:09:29 2023 +0100
@@ -30,9 +30,9 @@
proof
have "\<And>u. \<lbrakk>u \<in> S; norm u *\<^sub>R f (u /\<^sub>R norm u) \<notin> T\<rbrakk> \<Longrightarrow> u = 0"
by (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD)
- then have "g ` (S - {0}) \<subseteq> T"
+ then have "g \<in> (S - {0}) \<rightarrow> T"
using g_def by blast
- moreover have "g ` (S - {0}) \<subseteq> UNIV - {0}"
+ moreover have "g \<in> (S - {0}) \<rightarrow> UNIV - {0}"
proof (clarsimp simp: g_def)
fix y
assume "y \<in> S" and f0: "f (y /\<^sub>R norm y) = 0"
@@ -159,30 +159,24 @@
assumes ST: "subspace S" "subspace T" "dim S < dim T"
and "S \<subseteq> T"
and contf: "continuous_on (sphere 0 1 \<inter> S) f"
- and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
+ and fim: "f \<in> (sphere 0 1 \<inter> S) \<rightarrow> sphere 0 1 \<inter> T"
shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
proof -
have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
- using fim by (simp add: image_subset_iff)
+ using fim by auto
have "compact (sphere 0 1 \<inter> S)"
by (simp add: \<open>subspace S\<close> closed_subspace compact_Int_closed)
- then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 \<inter> S) \<subseteq> T"
+ then obtain g where pfg: "polynomial_function g" and gim: "g \<in> (sphere 0 1 \<inter> S) \<rightarrow> T"
and g12: "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> norm(f x - g x) < 1/2"
- using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"] fim by auto
+ using Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"] fim
+ by (auto simp: image_subset_iff_funcset)
have gnz: "g x \<noteq> 0" if "x \<in> sphere 0 1 \<inter> S" for x
- proof -
- have "norm (f x) = 1"
- using fim that by (simp add: image_subset_iff)
- then show ?thesis
- using g12 [OF that] by auto
- qed
+ using g12 that by fastforce
have diffg: "g differentiable_on sphere 0 1 \<inter> S"
by (metis pfg differentiable_on_polynomial_function)
define h where "h \<equiv> \<lambda>x. inverse(norm(g x)) *\<^sub>R g x"
have h: "x \<in> sphere 0 1 \<inter> S \<Longrightarrow> h x \<in> sphere 0 1 \<inter> T" for x
- unfolding h_def
- using gnz [of x]
- by (auto simp: subspace_mul [OF \<open>subspace T\<close>] subsetD [OF gim])
+ unfolding h_def using \<open>subspace T\<close> gim gnz subspace_mul by fastforce
have diffh: "h differentiable_on sphere 0 1 \<inter> S"
unfolding h_def using gnz
by (fastforce intro: derivative_intros diffg differentiable_on_compose [OF diffg])
@@ -205,7 +199,7 @@
have "convex T"
by (simp add: \<open>subspace T\<close> subspace_imp_convex)
then have "convex hull {f x, g x} \<subseteq> T"
- by (metis IntD2 closed_segment_subset fim gim image_subset_iff segment_convex_hull that)
+ by (metis IntD2 PiE closed_segment_subset fim gim segment_convex_hull that)
then show ?thesis
using that non0fg segment_convex_hull by fastforce
qed
@@ -279,14 +273,9 @@
then have affS_eq: "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
using \<open>aff_dim T = aff_dim S\<close> by simp
have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \<inter> T)"
- proof (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>])
- show "convex (ball 0 1 \<inter> T)"
- by (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex)
- show "bounded (ball 0 1 \<inter> T)"
- by (simp add: bounded_Int)
- show "aff_dim S = aff_dim (ball 0 1 \<inter> T)"
- by (rule affS_eq)
- qed
+ using homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>]
+ by (simp add: \<open>subspace T\<close> affS_eq assms bounded_Int convex_Int
+ homeomorphic_rel_frontiers_convex_bounded_sets subspace_imp_convex)
also have "... = frontier (ball 0 1) \<inter> T"
proof (rule convex_affine_rel_frontier_Int [OF convex_ball])
show "affine T"
@@ -318,10 +307,8 @@
then show ?thesis
proof (cases "T = {}")
case True
- then have "rel_frontier S = {}" "rel_frontier T = {}"
- using fim by fastforce+
then show ?thesis
- using that by (simp add: homotopic_on_emptyI)
+ by (smt (verit, best) False affST aff_dim_negative_iff)
next
case False
obtain T':: "'a set"
@@ -383,16 +370,16 @@
assumes fin: "finite \<F>"
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
- and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
- shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g \<in> S \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+ shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g \<in> (\<Union>\<F>) \<rightarrow> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
using assms
proof (induction \<F>)
case empty show ?case by simp
next
case (insert S \<F>)
- then obtain f where contf: "continuous_on (S) f" and fim: "f ` S \<subseteq> T" and feq: "\<forall>x \<in> S \<inter> K. f x = h x"
- by (meson insertI1)
- obtain g where contg: "continuous_on (\<Union>\<F>) g" and gim: "g ` \<Union>\<F> \<subseteq> T" and geq: "\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x"
+ then obtain f where contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> T" and feq: "\<forall>x \<in> S \<inter> K. f x = h x"
+ by (metis funcset_image insert_iff)
+ obtain g where contg: "continuous_on (\<Union>\<F>) g" and gim: "g \<in> (\<Union>\<F>) \<rightarrow> T" and geq: "\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x"
using insert by auto
have fg: "f x = g x" if "x \<in> T" "T \<in> \<F>" "x \<in> S" for x T
proof -
@@ -403,38 +390,38 @@
qed
moreover have "continuous_on (S \<union> \<Union> \<F>) (\<lambda>x. if x \<in> S then f x else g x)"
by (auto simp: insert closed_Union contf contg intro: fg continuous_on_cases)
+ moreover have "S \<union> \<Union> \<F> = \<Union> (insert S \<F>)"
+ by auto
ultimately show ?case
- by (smt (verit, del_insts) Int_iff UnE complete_lattice_class.Sup_insert feq fim geq gim image_subset_iff)
+ by (smt (verit) Int_iff Pi_iff UnE feq fim geq gim)
qed
lemma extending_maps_Union:
assumes fin: "finite \<F>"
- and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
- and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
- and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
- shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
-apply (simp flip: Union_maximal_sets [OF fin])
-apply (rule extending_maps_Union_aux)
-apply (simp_all add: Union_maximal_sets [OF fin] assms)
-by (metis K psubsetI)
-
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g \<in> S \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
+ and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
+ shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g \<in> (\<Union>\<F>) \<rightarrow> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)"
+proof -
+ have "\<And>S T. \<lbrakk>S \<in> \<F>; \<forall>U\<in>\<F>. \<not> S \<subset> U; T \<in> \<F>; \<forall>U\<in>\<F>. \<not> T \<subset> U; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
+ by (metis K psubsetI)
+ then show ?thesis
+ apply (simp flip: Union_maximal_sets [OF fin])
+ apply (rule extending_maps_Union_aux, simp_all add: Union_maximal_sets [OF fin] assms)
+ done
+qed
lemma extend_map_lemma:
assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S"
- and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
- obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
+ and contf: "continuous_on (\<Union>\<G>) f" and fim: "f \<in> (\<Union>\<G>) \<rightarrow> rel_frontier T"
+ obtains g where "continuous_on (\<Union>\<F>) g" "g \<in> (\<Union>\<F>) \<rightarrow> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
proof (cases "\<F> - \<G> = {}")
case True
show ?thesis
- proof
- show "continuous_on (\<Union> \<F>) f"
- using True \<open>\<G> \<subseteq> \<F>\<close> contf by auto
- show "f ` \<Union> \<F> \<subseteq> rel_frontier T"
- using True fim by auto
- qed auto
+ using True assms(2) contf fim that by force
next
case False
then have "0 \<le> aff_dim T"
@@ -467,14 +454,14 @@
using Suc.IH [OF ple] by auto
let ?Faces = "{D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D \<le> p}"
have extendh: "\<exists>g. continuous_on D g \<and>
- g ` D \<subseteq> rel_frontier T \<and>
+ g \<in> D \<rightarrow> rel_frontier T \<and>
(\<forall>x \<in> D \<inter> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}). g x = h x)"
if D: "D \<in> \<G> \<union> ?Faces" for D
proof (cases "D \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})")
case True
have "continuous_on D h"
using True conth continuous_on_subset by blast
- moreover have "h ` D \<subseteq> rel_frontier T"
+ moreover have "h \<in> D \<rightarrow> rel_frontier T"
using True him by blast
ultimately show ?thesis
by blast
@@ -574,7 +561,7 @@
show ?thesis
using that
apply clarsimp
- by (smt (verit, ccfv_SIG) IntI face_of_aff_dim_lt face_of_imp_convex [of X] face_of_imp_convex [of Y] face_of_trans ff)
+ by (smt (verit) IntI face_of_aff_dim_lt face_of_imp_convex face_of_trans ff inf_commute)
qed
obtain g where "continuous_on (\<Union>(\<G> \<union> ?Faces)) g"
"g ` \<Union>(\<G> \<union> ?Faces) \<subseteq> rel_frontier T"
@@ -589,23 +576,20 @@
show "\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}) \<subseteq> \<Union>\<F>"
using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset by fastforce
show "\<Union>\<F> \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < i})"
- proof (rule Union_mono)
- show "\<F> \<subseteq> \<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}"
- using face by (fastforce simp: aff i)
- qed
+ using face by (intro Union_mono) (fastforce simp: aff i)
qed
have "int i \<le> aff_dim T" by (simp add: i)
then show ?thesis
- using extendf [of i] unfolding eq by (metis that)
+ using extendf [of i] that unfolding eq by fastforce
qed
lemma extend_map_lemma_cofinite0:
assumes "finite \<F>"
and "pairwise (\<lambda>S T. S \<inter> T \<subseteq> K) \<F>"
- and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+ and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g \<in> (S - {a}) \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
shows "\<exists>C g. finite C \<and> disjnt C U \<and> card C \<le> card \<F> \<and>
- continuous_on (\<Union>\<F> - C) g \<and> g ` (\<Union>\<F> - C) \<subseteq> T
+ continuous_on (\<Union>\<F> - C) g \<and> g \<in> (\<Union>\<F> - C) \<rightarrow> T
\<and> (\<forall>x \<in> (\<Union>\<F> - C) \<inter> K. g x = h x)"
using assms
proof induction
@@ -614,18 +598,18 @@
next
case (insert X \<F>)
then have "closed X" and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
- and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
+ and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g \<in> (S - {a}) \<rightarrow> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
and pwX: "\<And>Y. Y \<in> \<F> \<and> Y \<noteq> X \<longrightarrow> X \<inter> Y \<subseteq> K \<and> Y \<inter> X \<subseteq> K"
and pwF: "pairwise (\<lambda> S T. S \<inter> T \<subseteq> K) \<F>"
by (simp_all add: pairwise_insert)
obtain C g where C: "finite C" "disjnt C U" "card C \<le> card \<F>"
and contg: "continuous_on (\<Union>\<F> - C) g"
- and gim: "g ` (\<Union>\<F> - C) \<subseteq> T"
+ and gim: "g \<in> (\<Union>\<F> - C) \<rightarrow> T"
and gh: "\<And>x. x \<in> (\<Union>\<F> - C) \<inter> K \<Longrightarrow> g x = h x"
using insert.IH [OF pwF \<F> clo] by auto
obtain a f where "a \<notin> U"
and contf: "continuous_on (X - {a}) f"
- and fim: "f ` (X - {a}) \<subseteq> T"
+ and fim: "f \<in> (X - {a}) \<rightarrow> T"
and fh: "(\<forall>x \<in> X \<inter> K. f x = h x)"
using insert.prems by (meson insertI1)
show ?case
@@ -652,19 +636,19 @@
by (blast intro: continuous_on_subset)
show "\<forall>x\<in>(\<Union>(insert X \<F>) - insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x"
using gh by (auto simp: fh)
- show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>(insert X \<F>) - insert a C) \<subseteq> T"
- using fim gim by auto force
+ show "(\<lambda>a. if a \<in> X then f a else g a) \<in> (\<Union>(insert X \<F>) - insert a C) \<rightarrow> T"
+ using fim gim Pi_iff by fastforce
qed
qed
lemma extend_map_lemma_cofinite1:
assumes "finite \<F>"
- and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g ` (X - {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
+ and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g \<in> (X - {a}) \<rightarrow> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; \<not> X \<subseteq> Y; \<not> Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K"
obtains C g where "finite C" "disjnt C U" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
- "g ` (\<Union>\<F> - C) \<subseteq> T"
+ "g \<in> (\<Union>\<F> - C) \<rightarrow> T"
"\<And>x. x \<in> (\<Union>\<F> - C) \<inter> K \<Longrightarrow> g x = h x"
proof -
let ?\<F> = "{X \<in> \<F>. \<forall>Y\<in>\<F>. \<not> X \<subset> Y}"
@@ -678,7 +662,7 @@
by (simp add: \<open>finite \<F>\<close> card_mono)
moreover
obtain C g where "finite C \<and> disjnt C U \<and> card C \<le> card ?\<F> \<and>
- continuous_on (\<Union>?\<F> - C) g \<and> g ` (\<Union>?\<F> - C) \<subseteq> T
+ continuous_on (\<Union>?\<F> - C) g \<and> g \<in> (\<Union>?\<F> - C) \<rightarrow> T
\<and> (\<forall>x \<in> (\<Union>?\<F> - C) \<inter> K. g x = h x)"
using extend_map_lemma_cofinite0 [OF fin pw, of U T h] by (fastforce intro!: clo \<F>)
ultimately show ?thesis
@@ -689,12 +673,12 @@
lemma extend_map_lemma_cofinite:
assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
- and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
+ and contf: "continuous_on (\<Union>\<G>) f" and fim: "f \<in> (\<Union>\<G>) \<rightarrow> rel_frontier T"
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T"
obtains C g where
"finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
- "g ` (\<Union> \<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
+ "g \<in> (\<Union> \<F> - C) \<rightarrow> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
proof -
define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
have "finite \<G>"
@@ -707,7 +691,7 @@
by (metis face inf_commute)
have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X"
by (simp add: \<H>_def) (smt (verit) \<open>\<G> \<subseteq> \<F>\<close> DiffE face' face_of_Int_subface in_mono inf.idem)
- obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h ` (\<Union>\<H>) \<subseteq> rel_frontier T"
+ obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h \<in> (\<Union>\<H>) \<rightarrow> rel_frontier T"
and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x"
proof (rule extend_map_lemma [OF \<open>finite \<H>\<close> [unfolded \<H>_def] Un_upper1 T])
show "\<And>X. \<lbrakk>X \<in> \<G> \<union> {D. \<exists>C\<in>\<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}\<rbrakk> \<Longrightarrow> polytope X"
@@ -720,11 +704,11 @@
then obtain a where a: "a \<notin> \<Union>\<G>"
by blast
have \<F>: "\<exists>a g. a \<notin> \<Union>\<G> \<and> continuous_on (D - {a}) g \<and>
- g ` (D - {a}) \<subseteq> rel_frontier T \<and> (\<forall>x \<in> D \<inter> \<Union>\<H>. g x = h x)"
+ g \<in> (D - {a}) \<rightarrow> rel_frontier T \<and> (\<forall>x \<in> D \<inter> \<Union>\<H>. g x = h x)"
if "D \<in> \<F>" for D
proof (cases "D \<subseteq> \<Union>\<H>")
case True
- then have "h ` (D - {a}) \<subseteq> rel_frontier T" "continuous_on (D - {a}) h"
+ then have "h \<in> (D - {a}) \<rightarrow> rel_frontier T" "continuous_on (D - {a}) h"
using him by (blast intro!: \<open>a \<notin> \<Union>\<G>\<close> continuous_on_subset [OF conth])+
then show ?thesis
using a by blast
@@ -755,7 +739,7 @@
by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD)
then obtain r where relfD: "rel_frontier D \<subseteq> affine hull D - {b}"
and contr: "continuous_on (affine hull D - {b}) r"
- and rim: "r ` (affine hull D - {b}) \<subseteq> rel_frontier D"
+ and rim: "r \<in> (affine hull D - {b}) \<rightarrow> rel_frontier D"
and rid: "\<And>x. x \<in> rel_frontier D \<Longrightarrow> r x = x"
by (auto simp: retract_of_def retraction_def)
show ?thesis
@@ -774,7 +758,7 @@
have "r ` (D - {b}) \<subseteq> r ` (affine hull D - {b})"
by (simp add: Diff_mono hull_subset image_mono)
also have "... \<subseteq> rel_frontier D"
- by (rule rim)
+ using rim by auto
also have "... \<subseteq> \<Union>{E. E face_of D \<and> aff_dim E < aff_dim T}"
using affD
by (force simp: rel_frontier_of_polyhedron [OF \<open>polyhedron D\<close>] facet_of_def)
@@ -788,7 +772,7 @@
show "continuous_on (r ` (D - {b})) h"
by (simp add: Diff_mono hull_subset continuous_on_subset [OF conth rsub])
qed
- show "(h \<circ> r) ` (D - {b}) \<subseteq> rel_frontier T"
+ show "(h \<circ> r) \<in> (D - {b}) \<rightarrow> rel_frontier T"
using brelD him rsub by fastforce
show "(h \<circ> r) x = h x" if x: "x \<in> D \<inter> \<Union>\<H>" for x
proof -
@@ -825,7 +809,7 @@
have clo: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
by (simp add: poly polytope_imp_closed)
obtain C g where "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
- "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T"
+ "g \<in> (\<Union>\<F> - C) \<rightarrow> rel_frontier T"
and gh: "\<And>x. x \<in> (\<Union>\<F> - C) \<inter> \<Union>\<H> \<Longrightarrow> g x = h x"
proof (rule extend_map_lemma_cofinite1 [OF \<open>finite \<F>\<close> \<F> clo])
show "X \<inter> Y \<subseteq> \<Union>\<H>" if XY: "X \<in> \<F>" "Y \<in> \<F>" and "\<not> X \<subseteq> Y" "\<not> Y \<subseteq> X" for X Y
@@ -856,7 +840,7 @@
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> rel_frontier T"
obtains g where "continuous_on (\<Union>\<F>) g"
- "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ "g \<in> (\<Union>\<F>) \<rightarrow> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g \<in> V \<rightarrow> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
@@ -877,12 +861,12 @@
proof (rule extend_map_lemma [of \<G> "\<G> \<inter> Pow V" T g])
show "continuous_on (\<Union>(\<G> \<inter> Pow V)) g"
by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff)
- qed (use \<open>finite \<G>\<close> T polyG affG faceG gim in fastforce)+
+ qed (use \<open>finite \<G>\<close> T polyG affG faceG gim image_subset_iff_funcset in auto)
show ?thesis
proof
show "continuous_on (\<Union>\<F>) h"
using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto
- show "h ` \<Union>\<F> \<subseteq> rel_frontier T"
+ show "h \<in> \<Union>\<F> \<rightarrow> rel_frontier T"
using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto
show "h x = f x" if "x \<in> S" for x
proof -
@@ -910,7 +894,7 @@
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X"
and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> rel_frontier T"
obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
- "g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+ "g \<in> (\<Union>\<F> - C) \<rightarrow> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof -
obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g \<in> V \<rightarrow> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
@@ -926,15 +910,15 @@
by (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly aff face]) auto
obtain C h where "finite C" and dis: "disjnt C (\<Union>(\<G> \<inter> Pow V))"
and card: "card C \<le> card \<G>" and conth: "continuous_on (\<Union>\<G> - C) h"
- and him: "h ` (\<Union>\<G> - C) \<subseteq> rel_frontier T"
+ and him: "h \<in> (\<Union>\<G> - C) \<rightarrow> rel_frontier T"
and hg: "\<And>x. x \<in> \<Union>(\<G> \<inter> Pow V) \<Longrightarrow> h x = g x"
proof (rule extend_map_lemma_cofinite [of \<G> "\<G> \<inter> Pow V" T g])
show "continuous_on (\<Union>(\<G> \<inter> Pow V)) g"
by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff)
- show "g ` \<Union>(\<G> \<inter> Pow V) \<subseteq> rel_frontier T"
+ show "g \<in> \<Union>(\<G> \<inter> Pow V) \<rightarrow> rel_frontier T"
using gim by force
qed (auto intro: \<open>finite \<G>\<close> T polyG affG dest: faceG)
- have Ssub: "S \<subseteq> \<Union>(\<G> \<inter> Pow V)"
+ have "S \<subseteq> \<Union>(\<G> \<inter> Pow V)"
proof
fix x
assume "x \<in> S"
@@ -948,23 +932,8 @@
then show "x \<in> \<Union>(\<G> \<inter> Pow V)"
using \<open>X \<in> \<G>\<close> \<open>x \<in> X\<close> by blast
qed
- show ?thesis
- proof
- show "continuous_on (\<Union>\<F>-C) h"
- using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto
- show "h ` (\<Union>\<F> - C) \<subseteq> rel_frontier T"
- using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto
- show "h x = f x" if "x \<in> S" for x
- proof -
- have "h x = g x"
- using Ssub hg that by blast
- also have "... = f x"
- by (simp add: gf that)
- finally show "h x = f x" .
- qed
- show "disjnt C S"
- using dis Ssub by (meson disjnt_iff subset_eq)
- qed (intro \<open>finite C\<close>)
+ then show ?thesis
+ by (metis PowI Union_Pow_eq \<open>\<Union> \<G> = \<Union> \<F>\<close> \<open>finite C\<close> conth dis disjnt_Union2 gf hg him subsetD that)
qed
@@ -1021,7 +990,7 @@
by (metis aff aff_dim_subset inf_commute inf_le1 order_trans)
obtain K g where K: "finite K" "disjnt K S"
and contg: "continuous_on (\<Union>{bbox \<inter> T} - K) g"
- and gim: "g ` (\<Union>{bbox \<inter> T} - K) \<subseteq> rel_frontier U"
+ and gim: "g \<in> (\<Union>{bbox \<inter> T} - K) \<rightarrow> rel_frontier U"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (rule extend_map_cell_complex_to_sphere_cofinite
[OF _ Ssub _ \<open>convex U\<close> \<open>bounded U\<close> _ _ _ contf fim])
@@ -1090,7 +1059,7 @@
have "(g \<circ> closest_point (cbox (- c) c \<inter> T)) ` (T - K) \<subseteq> g ` (\<Union>{bbox \<inter> T} - K)"
by (metis image_comp image_mono cpt_subset)
also have "... \<subseteq> rel_frontier U"
- by (rule gim)
+ using gim by blast
finally show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) \<in> (T - K) \<rightarrow> rel_frontier U"
by blast
show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) x = f x" if "x \<in> S" for x
@@ -1112,7 +1081,7 @@
order_trans [OF \<open>S \<subseteq> T\<close> hull_subset [of T affine]])
then obtain K g where "finite K" "disjnt K S"
and contg: "continuous_on (T - K) g"
- and gim: "g ` (T - K) \<subseteq> rel_frontier U"
+ and gim: "g \<in> (T - K) \<rightarrow> rel_frontier U"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset)
then show ?thesis
@@ -1195,7 +1164,7 @@
ultimately have "frontier (cball a d) \<inter> U retract_of (U - {a})"
by metis
then obtain r where contr: "continuous_on (U - {a}) r"
- and rim: "r ` (U - {a}) \<subseteq> sphere a d" "r ` (U - {a}) \<subseteq> U"
+ and rim: "r \<in> (U - {a}) \<rightarrow> sphere a d" "r \<in> (U - {a}) \<rightarrow> U"
and req: "\<And>x. x \<in> sphere a d \<inter> U \<Longrightarrow> r x = x"
using \<open>affine U\<close> by (force simp: retract_of_def retraction_def hull_same)
define j where "j \<equiv> \<lambda>x. if x \<in> ball a d then r x else x"
@@ -1212,8 +1181,7 @@
using rim by auto
then show "j y \<in> S \<union> C - ball a d"
unfolding j_def
- using \<open>r y \<in> sphere a d\<close> \<open>y \<in> U - {a}\<close> \<open>y \<in> S \<union> (C - {a})\<close> d rim
- by (metis Diff_iff Int_iff Un_iff subsetD cball_diff_eq_sphere image_subset_iff)
+ using \<open>y \<in> S \<union> (C - {a})\<close> \<open>y \<in> U - {a}\<close> d rim(2) by auto
qed
have contj: "continuous_on (U - {a}) j"
unfolding j_def Uaeq
@@ -1437,7 +1405,7 @@
and gim: "g \<in> (T - K) \<rightarrow> rel_frontier U"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using assms extend_map_affine_to_sphere_cofinite_simple by metis
- have "(\<exists>y C. C \<in> components (T - S) \<and> x \<in> C \<and> y \<in> C \<and> y \<in> L)" if "x \<in> K" for x
+ have "\<exists>y C. C \<in> components (T - S) \<and> x \<in> C \<and> y \<in> C \<and> y \<in> L" if "x \<in> K" for x
proof -
have "x \<in> T-S"
using \<open>K \<subseteq> T\<close> \<open>disjnt K S\<close> disjnt_def that by fastforce
@@ -1446,7 +1414,7 @@
with ovlap [of C] show ?thesis
by blast
qed
- then obtain \<xi> where \<xi>: "\<And>x. x \<in> K \<Longrightarrow> \<exists>C. C \<in> components (T - S) \<and> x \<in> C \<and> \<xi> x \<in> C \<and> \<xi> x \<in> L"
+ then obtain \<xi> where \<xi>: "\<And>x. x \<in> K \<Longrightarrow> \<exists>C. C \<in> components (T - S) \<and> x \<in> C \<and> \<xi> x \<in> C \<and> \<xi> x \<in> L"
by metis
obtain h where conth: "continuous_on (T - \<xi> ` K) h"
and him: "h \<in> (T - \<xi> ` K) \<rightarrow> rel_frontier U"
@@ -1525,7 +1493,7 @@
define LU where "LU \<equiv> L \<union> (\<Union> {C \<in> components (T - S). \<not>bounded C} - cbox (-(b+One)) (b+One))"
obtain K g where "finite K" "K \<subseteq> LU" "K \<subseteq> T" "disjnt K S"
and contg: "continuous_on (T - K) g"
- and gim: "g ` (T - K) \<subseteq> rel_frontier U"
+ and gim: "g \<in> (T - K) \<rightarrow> rel_frontier U"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (rule extend_map_affine_to_sphere2 [OF SUT aff contf fim])
show "C \<inter> LU \<noteq> {}" if "C \<in> components (T - S)" for C
@@ -1577,7 +1545,7 @@
proof (cases "x \<in> cbox (- c) c")
case True
with \<open>x \<in> T\<close> show ?thesis
- using cbsub(3) Knot by (force simp: closest_point_self)
+ using cbsub(3) Knot by (force simp: closest_point_self)
next
case False
have clo_in_rf: "closest_point (cbox (- c) c \<inter> T) x \<in> rel_frontier (cbox (- c) c \<inter> T)"
@@ -1617,7 +1585,7 @@
by (intro continuous_on_compose continuous_on_closest_point continuous_on_subset [OF contg]; force)
have "g (closest_point (cbox (- c) c \<inter> T) x) \<in> rel_frontier U"
if "x \<in> T" "x \<in> K \<longrightarrow> x \<notin> cbox (- b - One) (b + One)" for x
- using gim [THEN subsetD] that cloTK by blast
+ using cloTK gim that by auto
then show "(g \<circ> closest_point (cbox (- c) c \<inter> T)) \<in> (T - K \<inter> cbox (- (b + One)) (b + One))
\<rightarrow> rel_frontier U"
by force
@@ -1663,8 +1631,7 @@
and "\<And>C. \<lbrakk>C \<in> components(- S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
obtains K g where "finite K" "K \<subseteq> L" "disjnt K S" "continuous_on (- K) g"
"g \<in> (- K) \<rightarrow> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
- using extend_map_affine_to_sphere_cofinite
- [OF \<open>compact S\<close> affine_UNIV subset_UNIV] assms
+ using assms extend_map_affine_to_sphere_cofinite [OF \<open>compact S\<close> affine_UNIV subset_UNIV]
by (metis Compl_eq_Diff_UNIV aff_dim_UNIV of_nat_le_iff)
corollary extend_map_UNIV_to_sphere_no_bounded_component:
@@ -1789,14 +1756,7 @@
by auto
moreover
have "connected (- S) = connected (- sphere a r)"
- proof (rule homotopy_eqv_separation)
- show "S homotopy_eqv sphere a r"
- using hom homeomorphic_imp_homotopy_eqv by blast
- show "compact (sphere a r)"
- by simp
- then show " compact S"
- using hom homeomorphic_compactness by blast
- qed
+ by (meson hom compact_sphere homeomorphic_compactness homeomorphic_imp_homotopy_eqv homotopy_eqv_separation)
ultimately show ?thesis
using connected_Int_frontier [of "- sphere a r" "ball a r"] by (auto simp: \<open>0 < r\<close>)
qed
@@ -1831,7 +1791,7 @@
using S by (auto simp: homeomorphic_def)
show "connected (- T)" if "closed T" "T \<subset> S" for T
proof -
- have "f ` T \<subseteq> sphere a r"
+ have "f \<in> T \<rightarrow> sphere a r"
using \<open>T \<subset> S\<close> hom homeomorphism_image1 by blast
moreover have "f ` T \<noteq> sphere a r"
using \<open>T \<subset> S\<close> hom
@@ -1844,7 +1804,7 @@
moreover then have "compact (f ` T)"
by (meson compact_continuous_image continuous_on_subset hom homeomorphism_def psubsetE \<open>T \<subset> S\<close>)
moreover have "T homotopy_eqv f ` T"
- by (meson \<open>f ` T \<subseteq> sphere a r\<close> dual_order.strict_implies_order hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets \<open>T \<subset> S\<close>)
+ by (meson hom homeomorphic_def homeomorphic_imp_homotopy_eqv homeomorphism_of_subsets order.refl psubsetE that(2))
ultimately show ?thesis
using homotopy_eqv_separation [of T "f`T"] by blast
qed
@@ -1986,7 +1946,7 @@
lemma inv_of_domain_ss0:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
- assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+ assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f \<in> U \<rightarrow> S"
and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
and ope: "openin (top_of_set S) U"
shows "openin (top_of_set S) (f ` U)"
@@ -2019,19 +1979,20 @@
show "open (k ` U)"
by (simp add: ope_iff homeomorphism_imp_open_map [OF homkh ope])
show "inj_on (k \<circ> f \<circ> h) (k ` U)"
- by (smt (verit) comp_apply inj_on_def \<open>U \<subseteq> S\<close> fim homeomorphism_apply2 homhk image_iff injf subsetD)
+ unfolding inj_on_def
+ by (smt (verit, ccfv_threshold) PiE \<open>U \<subseteq> S\<close> assms(3) comp_apply homeomorphism_def homhk imageE inj_on_def injf subset_eq)
qed
moreover
have eq: "f ` U = h ` (k \<circ> f \<circ> h \<circ> k) ` U"
unfolding image_comp [symmetric] using \<open>U \<subseteq> S\<close> fim
- by (metis homeomorphism_image2 homeomorphism_of_subsets homkh subset_image_iff)
+ by (metis homeomorphism_image2 homeomorphism_of_subsets homhk homkh image_subset_iff_funcset top_greatest)
ultimately show ?thesis
by (metis (no_types, opaque_lifting) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
qed
lemma inv_of_domain_ss1:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
- assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
+ assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f \<in> U \<rightarrow> S"
and "subspace S"
and ope: "openin (top_of_set S) U"
shows "openin (top_of_set S) (f ` U)"
@@ -2045,7 +2006,7 @@
show "continuous_on (U \<times> S') g"
unfolding g_def
by (auto intro!: continuous_intros continuous_on_compose2 [OF contf continuous_on_fst])
- show "g ` (U \<times> S') \<subseteq> S \<times> S'"
+ show "g \<in> (U \<times> S') \<rightarrow> S \<times> S'"
using fim by (auto simp: g_def)
show "inj_on g (U \<times> S')"
using injf by (auto simp: g_def inj_on_def)
@@ -2073,7 +2034,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (top_of_set U) S"
and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
and injf: "inj_on f S"
shows "openin (top_of_set V) (f ` S)"
proof -
@@ -2087,7 +2048,7 @@
have eq: "f ` S = k ` (h \<circ> f) ` S"
proof -
have "k ` h ` f ` S = f ` S"
- by (meson fim homeomorphism_def homeomorphism_of_subsets homhk subset_refl)
+ by (meson equalityD2 fim funcset_image homeomorphism_image2 homeomorphism_of_subsets homhk)
then show ?thesis
by (simp add: image_comp)
qed
@@ -2101,11 +2062,11 @@
moreover have "openin (top_of_set U) ((h \<circ> f) ` S)"
proof (rule inv_of_domain_ss1)
show "continuous_on S (h \<circ> f)"
- by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+ by (meson contf continuous_on_compose continuous_on_subset fim funcset_image homeomorphism_cont2 homkh)
show "inj_on (h \<circ> f) S"
- by (smt (verit, ccfv_SIG) comp_apply fim inj_on_def homeomorphism_apply2 [OF homkh] image_subset_iff injf)
- show "(h \<circ> f) ` S \<subseteq> U"
- using \<open>V' \<subseteq> U\<close> hfV' by auto
+ by (smt (verit, ccfv_SIG) Pi_iff comp_apply fim homeomorphism_apply2 homkh inj_on_def injf)
+ show "h \<circ> f \<in> S \<rightarrow> U"
+ using \<open>V' \<subseteq> U\<close> hfV' by blast
qed (auto simp: assms)
ultimately show "openin (top_of_set V') ((h \<circ> f) ` S)"
using openin_subset_trans \<open>V' \<subseteq> U\<close> by force
@@ -2116,7 +2077,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (top_of_set U) S"
and "subspace U" "subspace V"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
and injf: "inj_on f S" and "S \<noteq> {}"
shows "dim U \<le> dim V"
proof -
@@ -2130,11 +2091,12 @@
then obtain h k where homhk: "homeomorphism V T h k"
using homeomorphic_def by blast
have "continuous_on S (h \<circ> f)"
- by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+ by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_def homhk image_subset_iff_funcset)
moreover have "(h \<circ> f) ` S \<subseteq> U"
using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
moreover have "inj_on (h \<circ> f) S"
- by (smt (verit, best) comp_apply inj_on_def fim homeomorphism_apply1 homhk image_subset_iff injf)
+ unfolding inj_on_def
+ by (metis Pi_iff comp_apply fim homeomorphism_def homhk inj_on_def injf)
ultimately have ope_hf: "openin (top_of_set U) ((h \<circ> f) ` S)"
using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by blast
have "(h \<circ> f) ` S \<subseteq> T"
@@ -2155,7 +2117,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (top_of_set U) S"
and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
and injf: "inj_on f S"
shows "openin (top_of_set V) (f ` S)"
proof (cases "S = {}")
@@ -2177,7 +2139,7 @@
by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
- show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+ show "(+) (- b) \<circ> f \<circ> (+) a \<in> (+) (- a) ` S \<rightarrow> (+) (- b) ` V"
using fim by auto
show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
by (auto simp: inj_on_def) (meson inj_onD injf)
@@ -2190,7 +2152,7 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (top_of_set U) S"
and aff: "affine U" "affine V"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> V"
and injf: "inj_on f S" and "S \<noteq> {}"
shows "aff_dim U \<le> aff_dim V"
proof -
@@ -2206,7 +2168,7 @@
by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
- show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+ show "(+) (- b) \<circ> f \<circ> (+) a \<in> (+) (- a) ` S \<rightarrow> (+) (- b) ` V"
using fim by auto
show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
by (auto simp: inj_on_def) (meson inj_onD injf)
@@ -2227,7 +2189,7 @@
corollary continuous_injective_image_subspace_dim_le:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "subspace S" "subspace T"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> T"
and injf: "inj_on f S"
shows "dim S \<le> dim T"
using invariance_of_dimension_subspaces [of S S _ f] assms by (auto simp: subspace_affine)
@@ -2235,7 +2197,7 @@
lemma invariance_of_dimension_convex_domain:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "convex S"
- and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
+ and contf: "continuous_on S f" and fim: "f \<in> S \<rightarrow> affine hull T"
and injf: "inj_on f S"
shows "aff_dim S \<le> aff_dim T"
proof (cases "S = {}")
@@ -2249,7 +2211,7 @@
by (simp add: openin_rel_interior)
show "continuous_on (rel_interior S) f"
using contf continuous_on_subset rel_interior_subset by blast
- show "f ` rel_interior S \<subseteq> affine hull T"
+ show "f \<in> rel_interior S \<rightarrow> affine hull T"
using fim rel_interior_subset by blast
show "inj_on f (rel_interior S)"
using inj_on_subset injf rel_interior_subset by blast
@@ -2271,8 +2233,8 @@
proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
show "continuous_on S h"
using homeomorphism_def homhk by blast
- show "h ` S \<subseteq> affine hull T"
- by (metis homeomorphism_def homhk hull_subset)
+ show "h \<in> S \<rightarrow> affine hull T"
+ using homeomorphism_image1 homhk hull_subset by fastforce
show "inj_on h S"
by (meson homeomorphism_apply1 homhk inj_on_inverseI)
qed
@@ -2342,13 +2304,13 @@
lemma continuous_image_subset_interior:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
- shows "f ` (interior S) \<subseteq> interior(f ` S)"
+ shows "f \<in> (interior S) \<rightarrow> interior(f ` S)"
proof -
have "open (f ` interior S)"
using assms
by (intro invariance_of_domain_gen) (auto simp: subset_inj_on interior_subset continuous_on_subset)
then show ?thesis
- by (simp add: image_mono interior_maximal interior_subset)
+ by (simp add: image_mono interiorI interior_subset)
qed
lemma homeomorphic_interiors_same_dimension:
@@ -2363,9 +2325,9 @@
and contf: "continuous_on S f" and contg: "continuous_on T g"
then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
by (auto simp: inj_on_def intro: rev_image_eqI) metis+
- have fim: "f ` interior S \<subseteq> interior T"
+ have fim: "f \<in> interior S \<rightarrow> interior T"
using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
- have gim: "g ` interior T \<subseteq> interior S"
+ have gim: "g \<in> interior T \<rightarrow> interior S"
using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
show "homeomorphism (interior S) (interior T) f g"
unfolding homeomorphism_def
@@ -2437,16 +2399,14 @@
and contf: "continuous_on S f" and contg: "continuous_on T g"
then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
by (auto simp: inj_on_def intro: rev_image_eqI) metis+
- have "g ` interior T \<subseteq> interior S"
+ have "g \<in> interior T \<rightarrow> interior S"
using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
then have fim: "f ` frontier S \<subseteq> frontier T"
- unfolding frontier_def
- using continuous_image_subset_interior assms(2) assms(3) S by auto
- have "f ` interior S \<subseteq> interior T"
+ unfolding frontier_def using Pi_mem S assms by fastforce
+ have "f \<in> interior S \<rightarrow> interior T"
using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
then have gim: "g ` frontier T \<subseteq> frontier S"
- unfolding frontier_def
- using continuous_image_subset_interior T assms(2) assms(3) by auto
+ unfolding frontier_def using Pi_mem T assms by fastforce
show "homeomorphism (frontier S) (frontier T) f g"
unfolding homeomorphism_def
proof (intro conjI ballI)
@@ -2500,9 +2460,10 @@
lemma continuous_image_subset_rel_interior:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+ assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f \<in> S \<rightarrow> T"
and TS: "aff_dim T \<le> aff_dim S"
- shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)"
+ shows "f \<in> (rel_interior S) \<rightarrow> rel_interior(f ` S)"
+unfolding image_subset_iff_funcset [symmetric]
proof (rule rel_interior_maximal)
show "f ` rel_interior S \<subseteq> f ` S"
by(simp add: image_mono rel_interior_subset)
@@ -2511,9 +2472,9 @@
show "openin (top_of_set (affine hull S)) (rel_interior S)"
by (simp add: openin_rel_interior)
show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)"
- by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
- show "f ` rel_interior S \<subseteq> affine hull f ` S"
- by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans)
+ by (metis TS aff_dim_affine_hull aff_dim_subset fim image_subset_iff_funcset order_trans)
+ show "f \<in> rel_interior S \<rightarrow> affine hull f ` S"
+ using \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset by fastforce
show "continuous_on (rel_interior S) f"
using contf continuous_on_subset rel_interior_subset by blast
show "inj_on f (rel_interior S)"
@@ -2533,10 +2494,10 @@
and contf: "continuous_on S f" and contg: "continuous_on T g"
then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
by (auto simp: inj_on_def intro: rev_image_eqI) metis+
- have fim: "f ` rel_interior S \<subseteq> rel_interior T"
- by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
- have gim: "g ` rel_interior T \<subseteq> rel_interior S"
- by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+ have fim: "f \<in> rel_interior S \<rightarrow> rel_interior T"
+ by (smt (verit, best) PiE Pi_I S \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST)
+ have gim: "g \<in> rel_interior T \<rightarrow> rel_interior S"
+ by (metis T \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior dual_order.refl funcsetI gTS)
show "homeomorphism (rel_interior S) (rel_interior T) f g"
unfolding homeomorphism_def
proof (intro conjI ballI)
@@ -2553,7 +2514,7 @@
by (metis fg \<open>x \<in> rel_interior T\<close> imageI)
qed
moreover have "f ` rel_interior S \<subseteq> rel_interior T"
- by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+ using fim by blast
ultimately show "f ` rel_interior S = rel_interior T"
by blast
show "continuous_on (rel_interior S) f"
@@ -2587,8 +2548,8 @@
proof (rule invariance_of_dimension_affine_sets)
show "continuous_on (rel_interior S) f"
using contf continuous_on_subset rel_interior_subset by blast
- show "f ` rel_interior S \<subseteq> affine hull T"
- by (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
+ show "f \<in> rel_interior S \<rightarrow> affine hull T"
+ by (simp add: S hull_inc mem_rel_interior_ball)
show "inj_on f (rel_interior S)"
by (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
qed (simp_all add: openin_rel_interior assms)
@@ -2625,10 +2586,10 @@
and contf: "continuous_on S f" and contg: "continuous_on T g"
then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
by (auto simp: inj_on_def intro: rev_image_eqI) metis+
- have fim: "f ` rel_interior S \<subseteq> rel_interior T"
- by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
- have gim: "g ` rel_interior T \<subseteq> rel_interior S"
- by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+ have fim: "f \<in> rel_interior S \<rightarrow> rel_interior T"
+ by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior dual_order.refl fST image_subset_iff_funcset)
+ have gim: "g \<in> rel_interior T \<rightarrow> rel_interior S"
+ by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior dual_order.refl gTS image_subset_iff_funcset)
show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
unfolding homeomorphism_def
proof (intro conjI ballI)
@@ -2637,11 +2598,11 @@
show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y"
using T mem_rel_interior_ball by blast
show "f ` (S - rel_interior S) = T - rel_interior T"
- using S fST fim gim by auto
+ using S fST fim gim image_subset_iff_funcset by fastforce
show "continuous_on (S - rel_interior S) f"
using contf continuous_on_subset rel_interior_subset by blast
show "g ` (T - rel_interior T) = S - rel_interior S"
- using T gTS gim fim by auto
+ using T gTS gim fim image_subset_iff_funcset by fastforce
show "continuous_on (T - rel_interior T) g"
using contg continuous_on_subset rel_interior_subset by blast
qed
@@ -2744,7 +2705,7 @@
(q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
- and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
+ and him: "h \<in> ({0..1} \<times> {0..1}) \<rightarrow> S"
and h0: "(\<forall>x. h (0, x) = p x)"
and h1: "(\<forall>x. h (1, x) = q x)"
and h01: "(\<forall>t\<in>{0..1}. h (t, 1) = h (t, 0)) "
@@ -2795,13 +2756,13 @@
lemma simply_connected_eq_homotopic_circlemaps1:
fixes f :: "complex \<Rightarrow> 'a::topological_space" and g :: "complex \<Rightarrow> 'a"
assumes S: "simply_connected S"
- and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
- and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
+ and contf: "continuous_on (sphere 0 1) f" and fim: "f \<in> (sphere 0 1) \<rightarrow> S"
+ and contg: "continuous_on (sphere 0 1) g" and gim: "g \<in> (sphere 0 1) \<rightarrow> S"
shows "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
proof -
let ?h = "(\<lambda>t. complex_of_real (2 * pi * t) * \<i>)"
have "homotopic_loops S (f \<circ> exp \<circ> ?h) (f \<circ> exp \<circ> ?h) \<and> homotopic_loops S (g \<circ> exp \<circ> ?h) (g \<circ> exp \<circ> ?h)"
- by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim)
+ by (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim image_subset_iff_funcset)
then have "homotopic_loops S (f \<circ> exp \<circ> ?h) (g \<circ> exp \<circ> ?h)"
using S simply_connected_homotopic_loops by blast
then show ?thesis
@@ -2812,19 +2773,19 @@
lemma simply_connected_eq_homotopic_circlemaps2a:
fixes h :: "complex \<Rightarrow> 'a::topological_space"
- assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1) \<subseteq> S"
+ assumes conth: "continuous_on (sphere 0 1) h" and him: "h \<in> sphere 0 1 \<rightarrow> S"
and hom: "\<And>f g::complex \<Rightarrow> 'a.
- \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
- continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+ \<lbrakk>continuous_on (sphere 0 1) f; f \<in> (sphere 0 1) \<rightarrow> S;
+ continuous_on (sphere 0 1) g; g \<in> (sphere 0 1) \<rightarrow> S\<rbrakk>
\<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
shows "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
- by (metis conth continuous_on_const him hom image_subset_iff)
+ by (metis conth continuous_on_const him hom image_subset_iff image_subset_iff_funcset)
lemma simply_connected_eq_homotopic_circlemaps2b:
fixes S :: "'a::real_normed_vector set"
assumes "\<And>f g::complex \<Rightarrow> 'a.
- \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
- continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+ \<lbrakk>continuous_on (sphere 0 1) f; f \<in> (sphere 0 1) \<rightarrow> S;
+ continuous_on (sphere 0 1) g; g \<in> (sphere 0 1) \<rightarrow> S\<rbrakk>
\<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
shows "path_connected S"
proof (clarsimp simp add: path_connected_eq_homotopic_points)
@@ -2869,10 +2830,10 @@
fixes S :: "'a::real_normed_vector set"
shows "simply_connected S \<longleftrightarrow>
(\<forall>f g::complex \<Rightarrow> 'a.
- continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
- continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
+ continuous_on (sphere 0 1) f \<and> f \<in> (sphere 0 1) \<rightarrow> S \<and>
+ continuous_on (sphere 0 1) g \<and> g \<in> (sphere 0 1) \<rightarrow> S
\<longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g)"
- by (metis simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a
+ by (metis image_subset_iff_funcset simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a
simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
proposition simply_connected_eq_contractible_circlemap:
@@ -2882,7 +2843,7 @@
(\<forall>f::complex \<Rightarrow> 'a.
continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
\<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
- by (metis simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a
+ by (metis image_subset_iff_funcset simply_connected_eq_homotopic_circlemaps simply_connected_eq_homotopic_circlemaps2a
simply_connected_eq_homotopic_circlemaps3 simply_connected_imp_path_connected)
corollary homotopy_eqv_simple_connectedness:
@@ -2966,12 +2927,7 @@
then obtain f g where hom: "homeomorphism S T f g"
using homeomorphic_def by blast
show "dim S = dim T"
- proof (rule order_antisym)
- show "dim S \<le> dim T"
- by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
- show "dim T \<le> dim S"
- by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
- qed
+ by (metis \<open>S homeomorphic T\<close> aff_dim_subspace assms homeomorphic_convex_sets of_nat_eq_iff subspace_imp_convex)
next
assume "dim S = dim T"
then show "S homeomorphic T"
@@ -3034,11 +2990,11 @@
qed
qed
-subsection\<open>more invariance of domain\<close>(*FIX ME title? *)
+subsection\<open>more invariance of domain\<close> (*FIX ME title? *)
proposition invariance_of_domain_sphere_affine_set_gen:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+ assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f \<in> S \<rightarrow> T"
and U: "bounded U" "convex U"
and "affine T" and affTU: "aff_dim T < aff_dim U"
and ope: "openin (top_of_set (rel_frontier U)) S"
@@ -3085,8 +3041,8 @@
qed (use contf continuous_on_subset hgsub in blast)
show "inj_on (f \<circ> h) (g ` (S - {b}))"
by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf gh Diff_iff comp_apply imageE subset_iff)
- show "(f \<circ> h) ` g ` (S - {b}) \<subseteq> T"
- by (metis fim image_comp image_mono hgsub subset_trans)
+ show "f \<circ> h \<in> g ` (S - {b}) \<rightarrow> T"
+ using fim hgsub by fastforce
qed (auto simp: assms)
moreover
have "openin (top_of_set T) ((f \<circ> k) ` j ` (S - {c}))"
@@ -3100,20 +3056,15 @@
qed (use contf continuous_on_subset kjsub in blast)
show "inj_on (f \<circ> k) (j ` (S - {c}))"
by (smt (verit, del_insts) SU homeomorphism_def inj_on_def injf jk Diff_iff comp_apply imageE subset_iff)
- show "(f \<circ> k) ` j ` (S - {c}) \<subseteq> T"
- by (metis fim image_comp image_mono kjsub subset_trans)
+ show "f \<circ> k \<in> j ` (S - {c}) \<rightarrow> T"
+ using fim kjsub by fastforce
qed (auto simp: assms)
ultimately have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}) \<union> ((f \<circ> k) ` j ` (S - {c})))"
by (rule openin_Un)
moreover have "(f \<circ> h) ` g ` (S - {b}) = f ` (S - {b})"
proof -
have "h ` g ` (S - {b}) = (S - {b})"
- proof
- show "h ` g ` (S - {b}) \<subseteq> S - {b}"
- using homeomorphism_apply1 [OF gh] SU by (fastforce simp add: image_iff image_subset_iff)
- show "S - {b} \<subseteq> h ` g ` (S - {b})"
- by (metis Diff_mono SU gh homeomorphism_image2 homeomorphism_of_subsets set_eq_subset)
- qed
+ by (meson Diff_mono Diff_subset SU gh homeomorphism_def homeomorphism_of_subsets subset_singleton_iff)
then show ?thesis
by (metis image_comp)
qed
@@ -3134,7 +3085,7 @@
lemma invariance_of_domain_sphere_affine_set:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+ assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f \<in> S \<rightarrow> T"
and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
and ope: "openin (top_of_set (sphere a r)) S"
shows "openin (top_of_set T) (f ` S)"
@@ -3166,9 +3117,10 @@
then have "\<not> open (f ` sphere a r)"
using compact_open
by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty)
- then show False
- using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] \<open>r > 0\<close>
- by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
+ then have "r=0"
+ by (metis Pi_I UNIV_I aff_dim_UNIV affine_UNIV contf injf invariance_of_domain_sphere_affine_set
+ of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
+ with \<open>r>0\<close> show False by auto
qed
then show ?thesis
using not_less by blast
@@ -3712,10 +3664,10 @@
assume L: ?lhs
then obtain g where contg: "continuous_on S g" and g: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
using inessential_imp_continuous_logarithm_circle by blast
- have "f ` S \<subseteq> sphere 0 1"
- by (metis L homotopic_with_imp_subset1)
+ have "f \<in> S \<rightarrow> sphere 0 1"
+ by (metis L image_subset_iff_funcset homotopic_with_imp_subset1)
then have "\<And>x. x \<in> S \<Longrightarrow> Re (g x) = 0"
- using g by auto
+ using g by (simp add: Pi_iff)
then show ?rhs
by (rule_tac x="Im \<circ> g" in exI) (auto simp: Euler g intro: contg continuous_intros)
next
@@ -3747,7 +3699,7 @@
shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
proof -
obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
- and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
+ and kim: "k \<in> ({0..1} \<times> S) \<rightarrow> sphere 0 1"
and k0: "\<And>x. k(0, x) = f x"
and k1: "\<And>x. k(1, x) = g x"
using hom by (auto simp: homotopic_with_def)
@@ -3760,8 +3712,8 @@
proposition homotopic_circlemaps_divide:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
- continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
- continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
+ continuous_on S f \<and> f \<in> S \<rightarrow> sphere 0 1 \<and>
+ continuous_on S g \<and> g \<in> S \<rightarrow> sphere 0 1 \<and>
(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
proof -
have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
@@ -3780,8 +3732,8 @@
homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
by auto
have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
- continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
- continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
+ continuous_on S f \<and> f \<in> S \<rightarrow> sphere 0 1 \<and>
+ continuous_on S g \<and> g \<in> S \<rightarrow> sphere 0 1 \<and>
homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
@@ -3802,7 +3754,7 @@
using homotopic_with_eq [OF homotopic_with_sphere_times [OF L cont]]
by (auto simp: divide_inverse norm_inverse)
with L show ?rhs
- by (simp add: homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2)
+ by (simp add: homotopic_with_imp_continuous homotopic_with_imp_funspace1)
next
assume ?rhs then show ?lhs
by (elim conjE homotopic_with_eq [OF homotopic_with_sphere_times]; force)
@@ -3882,7 +3834,7 @@
qed
lemma open_map_iff_lower_hemicontinuous_preimage:
- assumes "f ` S \<subseteq> T"
+ assumes "f \<in> S \<rightarrow> T"
shows "((\<forall>U. openin (top_of_set S) U
\<longrightarrow> openin (top_of_set T) (f ` U)) \<longleftrightarrow>
(\<forall>U. closedin (top_of_set S) U
@@ -3913,7 +3865,7 @@
qed
lemma closed_map_iff_upper_hemicontinuous_preimage:
- assumes "f ` S \<subseteq> T"
+ assumes "f \<in> S \<rightarrow> T"
shows "((\<forall>U. closedin (top_of_set S) U
\<longrightarrow> closedin (top_of_set T) (f ` U)) \<longleftrightarrow>
(\<forall>U. openin (top_of_set S) U
@@ -4519,11 +4471,11 @@
assume contf: "continuous_on (S \<union> T) f" and 0: "\<forall>i\<in>S \<union> T. f i \<noteq> 0"
then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
using continuous_on_subset by auto
- have "\<lbrakk>continuous_on S f; f ` S \<subseteq> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))"
+ have "\<lbrakk>continuous_on S f; f \<in> S \<rightarrow> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))"
using BS by (auto simp: Borsukian_continuous_logarithm)
then obtain g where contg: "continuous_on S g" and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
using "0" contfS by force
- have "\<lbrakk>continuous_on T f; f ` T \<subseteq> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on T g \<and> (\<forall>x \<in> T. f x = exp(g x))"
+ have "\<lbrakk>continuous_on T f; f \<in> T \<rightarrow> -{0}\<rbrakk> \<Longrightarrow> \<exists>g. continuous_on T g \<and> (\<forall>x \<in> T. f x = exp(g x))"
using BT by (auto simp: Borsukian_continuous_logarithm)
then obtain h where conth: "continuous_on T h" and fh: "\<And>x. x \<in> T \<Longrightarrow> f x = exp(h x)"
using "0" contfT by force
@@ -4718,12 +4670,12 @@
proof (rule upper_lower_hemicontinuous_explicit [of T "\<lambda>y. {z \<in> S. f z = y}" S])
show "\<And>U. openin (top_of_set S) U
\<Longrightarrow> openin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
- using closed_map_iff_upper_hemicontinuous_preimage [OF fim [THEN equalityD1]]
- by (simp add: Abstract_Topology_2.continuous_imp_closed_map \<open>compact S\<close> contf fim)
+ using closed_map_iff_upper_hemicontinuous_preimage [of f S T] fim contf \<open>compact S\<close>
+ using Abstract_Topology_2.continuous_imp_closed_map by blast
show "\<And>U. closedin (top_of_set S) U \<Longrightarrow>
closedin (top_of_set T) {x \<in> T. {z \<in> S. f z = x} \<subseteq> U}"
- using ope open_map_iff_lower_hemicontinuous_preimage [OF fim [THEN equalityD1]]
- by meson
+ using ope open_map_iff_lower_hemicontinuous_preimage[of f S T] fim [THEN equalityD1]
+ by blast
show "bounded {z \<in> S. f z = y}"
by (metis (no_types, lifting) compact_imp_bounded [OF \<open>compact S\<close>] bounded_subset mem_Collect_eq subsetI)
qed (use \<open>y \<in> T\<close> \<open>0 < d\<close> fk kTS in \<open>force+\<close>)
@@ -4918,7 +4870,7 @@
assume "connected U" "connected V" and T: "T = U \<union> V"
and cloU: "closedin (top_of_set T) U"
and cloV: "closedin (top_of_set T) V"
- have "f ` (g ` U \<inter> g ` V) \<subseteq> U" "f ` (g ` U \<inter> g ` V) \<subseteq> V"
+ have "f \<in> (g ` U \<inter> g ` V) \<rightarrow> U" "f \<in> (g ` U \<inter> g ` V) \<rightarrow> V"
using gf fim T by auto (metis UnCI image_iff)+
moreover have "U \<inter> V \<subseteq> f ` (g ` U \<inter> g ` V)"
using gf fim by (force simp: image_iff T)
@@ -5393,14 +5345,8 @@
lemma nonseparation_by_component_eq:
fixes S :: "'a :: euclidean_space set"
assumes "open S \<or> closed S"
- shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
-proof
- assume ?lhs with assms show ?rhs
- by (meson separation_by_component_closed separation_by_component_open)
-next
- assume ?rhs with assms show ?lhs
- using component_complement_connected by force
-qed
+ shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))"
+ by (metis assms component_complement_connected double_complement separation_by_component_closed separation_by_component_open)
text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
@@ -5421,7 +5367,7 @@
case False
have anr: "ANR (-{0::complex})"
by (simp add: ANR_delete open_Compl open_imp_ANR)
- obtain g where contg: "continuous_on UNIV g" and gim: "g ` UNIV \<subseteq> -{0}"
+ obtain g where contg: "continuous_on UNIV g" and gim: "g \<in> UNIV \<rightarrow> -{0}"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
show "closedin (top_of_set UNIV) S"
@@ -5456,13 +5402,7 @@
by (auto intro: continuous_on_subset [OF contj] simp flip: homeomorphism_image2 [OF hk])
qed
show "f x = exp ((j \<circ> k) x)" if "x \<in> S" for x
- proof -
- have "f x = (g \<circ> h) (k x)"
- by (simp add: gf that)
- also have "... = exp (j (k x))"
- by (metis rangeI homeomorphism_image2 [OF hk] j)
- finally show ?thesis by simp
- qed
+ by (metis UNIV_I comp_apply gf hk homeomorphism_def image_eqI j that)
qed
then show ?lhs
by (simp add: inessential_eq_continuous_logarithm)
@@ -5487,7 +5427,7 @@
and ope: "openin (top_of_set (\<Union>\<F>)) C"
and "homotopic_with_canon (\<lambda>x. True) C T f (\<lambda>x. a)"
using assms by blast
- with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
+ with \<open>C \<noteq> {}\<close> have "f \<in> C \<rightarrow> T" "a \<in> T"
using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
have "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
proof (rule homotopic_on_clopen_Union)
@@ -5514,15 +5454,9 @@
proposition Janiszewski_dual:
fixes S :: "complex set"
- assumes
- "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
+ assumes "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
shows "connected(S \<inter> T)"
-proof -
- have ST: "compact (S \<union> T)"
- by (simp add: assms compact_Un)
- with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
- show ?thesis
- by (simp add: Borsukian_separation_compact closed_subset compact_imp_closed unicoherentD)
-qed
+ by (meson Borsukian_imp_unicoherent Borsukian_separation_compact assms closed_subset compact_Un
+ compact_imp_closed sup_ge1 sup_ge2 unicoherentD)
end
--- a/src/HOL/Analysis/Homotopy.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Sat Aug 12 10:09:29 2023 +0100
@@ -2950,11 +2950,11 @@
obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "finite B" "card B = dim S" "span B = S"
- by (metis orthonormal_basis_subspace [OF S] independent_finite)
+ by (metis orthonormal_basis_subspace [OF S] independent_imp_finite)
obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
and "independent C" "finite C" "card C = dim T" "span C = T"
- by (metis orthonormal_basis_subspace [OF T] independent_finite)
+ by (metis orthonormal_basis_subspace [OF T] independent_imp_finite)
obtain fb where "fb ` B \<subseteq> C" "inj_on fb B"
by (metis \<open>card B = dim S\<close> \<open>card C = dim T\<close> \<open>finite B\<close> \<open>finite C\<close> card_le_inj d)
then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
@@ -3003,11 +3003,11 @@
obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "finite B" "card B = dim S" "span B = S"
- by (metis orthonormal_basis_subspace [OF S] independent_finite)
+ by (metis orthonormal_basis_subspace [OF S] independent_imp_finite)
obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
and "independent C" "finite C" "card C = dim T" "span C = T"
- by (metis orthonormal_basis_subspace [OF T] independent_finite)
+ by (metis orthonormal_basis_subspace [OF T] independent_imp_finite)
obtain fb where "bij_betw fb B C"
by (metis \<open>finite B\<close> \<open>finite C\<close> bij_betw_iff_card \<open>card B = dim S\<close> \<open>card C = dim T\<close> d)
then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Sat Aug 12 10:09:29 2023 +0100
@@ -102,13 +102,11 @@
lemma sets_Collect_single':
"i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
- using sets_Collect_single[of i I "{x\<in>space (M i). P x}" M]
- by (simp add: space_PiM PiE_iff cong: conj_cong)
+ by auto
lemma (in finite_product_prob_space) finite_measure_PiM_emb:
"(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> measure (PiM I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. measure (M i) (A i))"
- using measure_PiM_emb[of I A] finite_index prod_emb_PiE_same_index[OF sets.sets_into_space, of I A M]
- by auto
+ by (rule prob_times)
lemma (in product_prob_space) PiM_component:
assumes "i \<in> I"
--- a/src/HOL/Topological_Spaces.thy Sun Aug 06 19:00:06 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy Sat Aug 12 10:09:29 2023 +0100
@@ -1220,6 +1220,11 @@
"f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
unfolding tendsto_def eventually_sequentially by auto
+lemma closed_sequentially:
+ assumes "closed S" and "\<And>n. f n \<in> S" and "f \<longlonglongrightarrow> l"
+ shows "l \<in> S"
+ by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)
+
subsection \<open>Monotone sequences and subsequences\<close>