--- a/src/HOL/Algebra/Algebra.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy Fri Apr 05 15:02:55 2019 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Algebra/Algebra.thy *)
theory Algebra
- imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Product_Groups
+ imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
begin
end
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy Fri Apr 05 15:02:55 2019 +0100
@@ -2,7 +2,7 @@
theory Free_Abelian_Groups
imports
- Product_Groups "HOL-Cardinals.Cardinal_Arithmetic"
+ Product_Groups "../Cardinals/Cardinal_Arithmetic"
"HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence"
begin
@@ -594,7 +594,6 @@
by (auto simp: hom_def free_Abelian_group_def Pi_def)
qed
-
proposition iso_free_Abelian_group_sum:
assumes "pairwise (\<lambda>i j. disjnt (S i) (S j)) I"
shows "(\<lambda>f. sum' f I) \<in> iso (sum_group I (\<lambda>i. free_Abelian_group(S i))) (free_Abelian_group (\<Union>(S ` I)))"
@@ -610,8 +609,7 @@
done
show "?h (x \<otimes>\<^bsub>?G\<^esub> y) = ?h x \<otimes>\<^bsub>?H\<^esub> ?h y"
if "x \<in> carrier ?G" "y \<in> carrier ?G" for x y
- using that apply (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib')
- sorry
+ using that by (simp add: sum.finite_Collect_op carrier_sum_group sum.distrib')
qed
interpret GH: group_hom "?G" "?H" "?h"
using hom by (simp add: group_hom_def group_hom_axioms_def)
@@ -668,8 +666,7 @@
have "finite {i \<in> I. Abs_poly_mapping (?f i) \<noteq> 0}"
by (rule finite_subset [OF _ fin]) (use \<open>i \<in> I\<close> J_def eq in \<open>auto simp: in_keys_iff\<close>)
with \<open>i \<in> I\<close> have "?h (\<lambda>j\<in>I. Abs_poly_mapping (?f j)) = Abs_poly_mapping (?f i) + sum' (\<lambda>j. Abs_poly_mapping (?f j)) (I - {i})"
- apply (simp add: sum_diff1')
- sorry
+ by (simp add: sum_diff1')
then show ?thesis
by (simp add: 1 2 Poly_Mapping.lookup_add)
next
--- a/src/HOL/Analysis/Abstract_Limits.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Limits.thy Fri Apr 05 15:02:55 2019 +0100
@@ -53,11 +53,11 @@
lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
by (simp add: limitin_def)
-lemma limitin_const: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
+lemma limitin_const_iff [simp]: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
by (simp add: limitin_def)
-lemma limitin_real_const: "limitin euclideanreal (\<lambda>a. l) l F"
- by (simp add: limitin_def)
+lemma limitin_const: "limitin euclidean (\<lambda>a. l) l F"
+ by simp
lemma limitin_eventually:
"\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limitin X f l F"
@@ -91,6 +91,11 @@
qed (auto simp: limitin_def topspace_subtopology)
+lemma limitin_canonical_iff_gen [simp]:
+ assumes "open S"
+ shows "limitin (top_of_set S) f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F \<and> l \<in> S"
+ using assms by (auto simp: limitin_subtopology tendsto_def)
+
lemma limitin_sequentially:
"limitin X S l sequentially \<longleftrightarrow>
l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"
--- a/src/HOL/Analysis/Abstract_Topology.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Fri Apr 05 15:02:55 2019 +0100
@@ -1694,7 +1694,7 @@
"continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
by (auto simp: continuous_map_def)
-lemma continuous_map_iff_continuous [simp]: "continuous_map (subtopology euclidean S) euclidean g = continuous_on S g"
+lemma continuous_map_iff_continuous [simp]: "continuous_map (top_of_set S) euclidean g = continuous_on S g"
by (fastforce simp add: continuous_map openin_subtopology continuous_on_open_invariant)
lemma continuous_map_iff_continuous2 [simp]: "continuous_map euclidean euclidean g = continuous_on UNIV g"
@@ -3782,12 +3782,17 @@
using assms continuous_on_closed by blast
lemma continuous_map_subtopology_eu [simp]:
- "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+ "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
apply safe
apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+lemma continuous_map_euclidean_top_of_set:
+ assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f"
+ shows "continuous_map euclidean (top_of_set S) f"
+ by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage)
+
subsection%unimportant \<open>Half-global and completely global cases\<close>
lemma continuous_openin_preimage_gen:
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Fri Apr 05 15:02:55 2019 +0100
@@ -800,10 +800,11 @@
unfolding comp_def by auto
next
assume *: "\<forall>x. continuous_map T euclidean (\<lambda>y. blinfun_apply (f y) x)"
- have "continuous_map T euclidean (blinfun_apply o f)"
- unfolding euclidean_product_topology
- apply (rule continuous_map_coordinatewise_then_product, auto)
+ have "\<And>i. continuous_map T euclidean (\<lambda>x. blinfun_apply (f x) i)"
using * unfolding comp_def by auto
+ then have "continuous_map T euclidean (blinfun_apply o f)"
+ unfolding o_def
+ by (metis (no_types) continuous_map_componentwise_UNIV euclidean_product_topology)
show "continuous_map T strong_operator_topology f"
unfolding strong_operator_topology_def
apply (rule continuous_map_pullback')
@@ -815,6 +816,4 @@
by (subst continuous_on_strong_operator_topo_iff_coordinatewise,
auto simp add: linear_continuous_on)
-
-
end
--- a/src/HOL/Analysis/Conformal_Mappings.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Fri Apr 05 15:02:55 2019 +0100
@@ -3101,7 +3101,7 @@
define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)"
have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- apply (subst netlimit_within)
+ apply (subst Lim_ident_at)
using \<open>n>m\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
@@ -3130,7 +3130,7 @@
define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)"
have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def continuous_def
- apply (subst netlimit_within)
+ apply (subst Lim_ident_at)
using \<open>m>n\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
--- a/src/HOL/Analysis/Derivative.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy Fri Apr 05 15:02:55 2019 +0100
@@ -2015,7 +2015,7 @@
using *
apply (cases "at x within S \<noteq> bot")
apply (intro refl conj_cong filterlim_cong)
- apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono)
+ apply (auto simp: Lim_ident_at eventually_at_filter elim: eventually_mono)
done
lemma islimpt_closure_open:
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Fri Apr 05 15:02:55 2019 +0100
@@ -620,7 +620,7 @@
apply (simp add: norm_sgn sgn_zero_iff x)
done
then show ?thesis
- by (rule netlimit_within [of a UNIV])
+ by (rule Lim_ident_at [of a UNIV])
qed simp
subsection \<open>Boundedness\<close>
--- a/src/HOL/Analysis/Elementary_Topology.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy Fri Apr 05 15:02:55 2019 +0100
@@ -1472,13 +1472,10 @@
abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a"
where "netlimit F \<equiv> Lim F (\<lambda>x. x)"
-lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
- by (rule tendsto_Lim) (auto intro: tendsto_intros)
-
lemma netlimit_at [simp]:
fixes a :: "'a::{perfect_space,t2_space}"
shows "netlimit (at a) = a"
- using netlimit_within [of a UNIV] by simp
+ using Lim_ident_at [of a UNIV] by simp
lemma lim_within_interior:
"x \<in> interior S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at x)"
@@ -2750,5 +2747,4 @@
finally show ?thesis .
qed
-
end
\ No newline at end of file
--- a/src/HOL/Analysis/Function_Topology.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Function_Topology.thy Fri Apr 05 15:02:55 2019 +0100
@@ -565,8 +565,14 @@
end
+lemma open_PiE [intro?]:
+ fixes X::"'i \<Rightarrow> ('b::topological_space) set"
+ assumes "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
+ shows "open (Pi\<^sub>E UNIV X)"
+ by (simp add: assms open_fun_def product_topology_basis)
+
lemma euclidean_product_topology:
- "euclidean = product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV"
+ "product_topology (\<lambda>i. euclidean::('b::topological_space) topology) UNIV = euclidean"
by (metis open_openin topology_eq open_fun_def)
proposition product_topology_basis':
@@ -582,8 +588,7 @@
have **: "finite {i. X i \<noteq> UNIV}"
unfolding X_def V_def J_def using assms(1) by auto
have "open (Pi\<^sub>E UNIV X)"
- unfolding open_fun_def
- by (simp_all add: * ** product_topology_basis)
+ by (simp add: "*" "**" open_PiE)
moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
proof (auto)
@@ -618,8 +623,8 @@
lemma continuous_on_product_then_coordinatewise_UNIV:
assumes "continuous_on UNIV f"
shows "continuous_on UNIV (\<lambda>x. f x i)"
- using assms unfolding continuous_map_iff_continuous2 [symmetric] euclidean_product_topology
- by fastforce
+ unfolding continuous_map_iff_continuous2 [symmetric]
+ by (rule continuous_map_product_then_coordinatewise [where I=UNIV]) (use assms in \<open>auto simp: euclidean_product_topology\<close>)
lemma continuous_on_product_then_coordinatewise:
assumes "continuous_on S f"
@@ -724,7 +729,8 @@
text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
have "countable (B i)" for i unfolding B_def by auto
-
+ have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
+ by (auto simp: B_def A)
define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
have "Pi\<^sub>E UNIV (\<lambda>i. UNIV) \<in> K"
unfolding K_def B_def by auto
@@ -737,10 +743,7 @@
have "x \<in> k" if "k \<in> K" for k
using that unfolding K_def B_def apply auto using A(1) by auto
have "open k" if "k \<in> K" for k
- using that unfolding open_fun_def K_def B_def apply (auto)
- apply (rule product_topology_basis)
- unfolding topspace_euclidean by (auto, metis imageE open_UNIV A(2))
-
+ using that unfolding K_def by (blast intro: open_B open_PiE elim: )
have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
proof -
have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
@@ -854,9 +857,7 @@
next
fix U assume "U \<in> K"
show "open U"
- using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
- apply (rule product_topology_basis)
- using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV by auto
+ using \<open>U \<in> K\<close> unfolding open_fun_def K_def by clarify (metis \<open>U \<in> K\<close> i open_PiE open_fun_def)
qed
show ?thesis using i ii iii by auto
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Apr 05 15:02:55 2019 +0100
@@ -32,6 +32,74 @@
by (auto intro!: real_le_rsqrt)
qed
+subsection \<open>Continuity of the representation WRT an orthogonal basis\<close>
+
+lemma representation_bound:
+ fixes B :: "'N::real_inner set"
+ assumes "finite B" "independent B" "b \<in> B" and orth: "pairwise orthogonal B"
+ obtains m where "m > 0" "\<And>x. x \<in> span B \<Longrightarrow> \<bar>representation B x b\<bar> \<le> m * norm x"
+proof
+ fix x
+ assume x: "x \<in> span B"
+ have "b \<noteq> 0"
+ using \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by blast
+ have [simp]: "b \<bullet> b' = (if b' = b then (norm b)\<^sup>2 else 0)"
+ if "b \<in> B" "b' \<in> B" for b b'
+ using orth by (simp add: orthogonal_def pairwise_def norm_eq_sqrt_inner that)
+ have "norm x = norm (\<Sum>b\<in>B. representation B x b *\<^sub>R b)"
+ using real_vector.sum_representation_eq [OF \<open>independent B\<close> x \<open>finite B\<close> order_refl]
+ by simp
+ also have "\<dots> = sqrt ((\<Sum>b\<in>B. representation B x b *\<^sub>R b) \<bullet> (\<Sum>b\<in>B. representation B x b *\<^sub>R b))"
+ by (simp add: norm_eq_sqrt_inner)
+ also have "\<dots> = sqrt (\<Sum>b\<in>B. (representation B x b *\<^sub>R b) \<bullet> (representation B x b *\<^sub>R b))"
+ using \<open>finite B\<close>
+ by (simp add: inner_sum_left inner_sum_right if_distrib [of "\<lambda>x. _ * x"] cong: if_cong sum.cong_simp)
+ also have "\<dots> = sqrt (\<Sum>b\<in>B. (norm (representation B x b *\<^sub>R b))\<^sup>2)"
+ by (simp add: mult.commute mult.left_commute power2_eq_square)
+ also have "\<dots> = sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
+ by (simp add: norm_mult power_mult_distrib)
+ finally have "norm x = sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)" .
+ moreover
+ have "sqrt ((representation B x b)\<^sup>2 * (norm b)\<^sup>2) \<le> sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
+ using \<open>b \<in> B\<close> \<open>finite B\<close> by (auto intro: member_le_sum)
+ then have "\<bar>representation B x b\<bar> \<le> (1 / norm b) * sqrt (\<Sum>b\<in>B. (representation B x b)\<^sup>2 * (norm b)\<^sup>2)"
+ using \<open>b \<noteq> 0\<close> by (simp add: divide_simps real_sqrt_mult del: real_sqrt_le_iff)
+ ultimately show "\<bar>representation B x b\<bar> \<le> (1 / norm b) * norm x"
+ by simp
+next
+ show "0 < 1 / norm b"
+ using \<open>independent B\<close> \<open>b \<in> B\<close> dependent_zero by auto
+qed
+
+lemma continuous_on_representation:
+ fixes B :: "'N::euclidean_space set"
+ assumes "finite B" "independent B" "b \<in> B" "pairwise orthogonal B"
+ shows "continuous_on (span B) (\<lambda>x. representation B x b)"
+proof
+ show "\<exists>d>0. \<forall>x'\<in>span B. dist x' x < d \<longrightarrow> dist (representation B x' b) (representation B x b) \<le> e"
+ if "e > 0" "x \<in> span B" for x e
+ proof -
+ obtain m where "m > 0" and m: "\<And>x. x \<in> span B \<Longrightarrow> \<bar>representation B x b\<bar> \<le> m * norm x"
+ using assms representation_bound by blast
+ show ?thesis
+ unfolding dist_norm
+ proof (intro exI conjI ballI impI)
+ show "e/m > 0"
+ by (simp add: \<open>e > 0\<close> \<open>m > 0\<close>)
+ show "norm (representation B x' b - representation B x b) \<le> e"
+ if x': "x' \<in> span B" and less: "norm (x'-x) < e/m" for x'
+ proof -
+ have "\<bar>representation B (x'-x) b\<bar> \<le> m * norm (x'-x)"
+ using m [of "x'-x"] \<open>x \<in> span B\<close> span_diff x' by blast
+ also have "\<dots> < e"
+ by (metis \<open>m > 0\<close> less mult.commute pos_less_divide_eq)
+ finally have "\<bar>representation B (x'-x) b\<bar> \<le> e" by simp
+ then show ?thesis
+ by (simp add: \<open>x \<in> span B\<close> \<open>independent B\<close> representation_diff x')
+ qed
+ qed
+ qed
+qed
subsection%unimportant\<open>Balls in Euclidean Space\<close>
--- a/src/HOL/Library/FuncSet.thy Fri Apr 05 14:08:39 2019 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Apr 05 15:02:55 2019 +0100
@@ -220,6 +220,12 @@
lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
by (auto simp: restrict_def Pi_def)
+lemma sum_restrict' [simp]: "sum' (\<lambda>i\<in>I. g i) I = sum' (\<lambda>i. g i) I"
+ by (simp add: sum.G_def conj_commute cong: conj_cong)
+
+lemma prod_restrict' [simp]: "prod' (\<lambda>i\<in>I. g i) I = prod' (\<lambda>i. g i) I"
+ by (simp add: prod.G_def conj_commute cong: conj_cong)
+
subsection \<open>Bijections Between Sets\<close>