equal
deleted
inserted
replaced
12 |
12 |
13 (* to be moved elsewhere *) |
13 (* to be moved elsewhere *) |
14 |
14 |
15 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}" |
15 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}" |
16 unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner) |
16 unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner) |
17 apply(auto simp add:power2_eq_square) unfolding euclidean_component.diff .. |
17 apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff .. |
18 |
18 |
19 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)" |
19 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)" |
20 apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)") |
20 apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)") |
21 apply(rule member_le_setL2) by auto |
21 apply(rule member_le_setL2) by auto |
22 |
22 |
1910 |
1910 |
1911 lemma bounded_scaling: |
1911 lemma bounded_scaling: |
1912 fixes S :: "'a::real_normed_vector set" |
1912 fixes S :: "'a::real_normed_vector set" |
1913 shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)" |
1913 shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)" |
1914 apply (rule bounded_linear_image, assumption) |
1914 apply (rule bounded_linear_image, assumption) |
1915 apply (rule scaleR.bounded_linear_right) |
1915 apply (rule bounded_linear_scaleR_right) |
1916 done |
1916 done |
1917 |
1917 |
1918 lemma bounded_translation: |
1918 lemma bounded_translation: |
1919 fixes S :: "'a::real_normed_vector set" |
1919 fixes S :: "'a::real_normed_vector set" |
1920 assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)" |
1920 assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)" |
3535 assumes "uniformly_continuous_on s f" |
3535 assumes "uniformly_continuous_on s f" |
3536 shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))" |
3536 shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))" |
3537 proof- |
3537 proof- |
3538 { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially" |
3538 { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially" |
3539 hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially" |
3539 hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially" |
3540 using scaleR.tendsto [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c] |
3540 using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c] |
3541 unfolding scaleR_zero_right scaleR_right_diff_distrib by auto |
3541 unfolding scaleR_zero_right scaleR_right_diff_distrib by auto |
3542 } |
3542 } |
3543 thus ?thesis using assms unfolding uniformly_continuous_on_sequentially' |
3543 thus ?thesis using assms unfolding uniformly_continuous_on_sequentially' |
3544 unfolding dist_norm tendsto_norm_zero_iff by auto |
3544 unfolding dist_norm tendsto_norm_zero_iff by auto |
3545 qed |
3545 qed |
4363 lemma compact_scaling: |
4363 lemma compact_scaling: |
4364 fixes s :: "'a::real_normed_vector set" |
4364 fixes s :: "'a::real_normed_vector set" |
4365 assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)" |
4365 assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)" |
4366 proof- |
4366 proof- |
4367 let ?f = "\<lambda>x. scaleR c x" |
4367 let ?f = "\<lambda>x. scaleR c x" |
4368 have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right) |
4368 have *:"bounded_linear ?f" by (rule bounded_linear_scaleR_right) |
4369 show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] |
4369 show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] |
4370 using linear_continuous_at[OF *] assms by auto |
4370 using linear_continuous_at[OF *] assms by auto |
4371 qed |
4371 qed |
4372 |
4372 |
4373 lemma compact_negations: |
4373 lemma compact_negations: |
4949 hence "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto } |
4949 hence "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto } |
4950 hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially" |
4950 hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially" |
4951 unfolding Lim_sequentially by(auto simp add: dist_norm) |
4951 unfolding Lim_sequentially by(auto simp add: dist_norm) |
4952 hence "(f ---> x) sequentially" unfolding f_def |
4952 hence "(f ---> x) sequentially" unfolding f_def |
4953 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
4953 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
4954 using scaleR.tendsto [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } |
4954 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } |
4955 ultimately have "x \<in> closure {a<..<b}" |
4955 ultimately have "x \<in> closure {a<..<b}" |
4956 using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto } |
4956 using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto } |
4957 thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast |
4957 thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast |
4958 qed |
4958 qed |
4959 |
4959 |
5569 |
5569 |
5570 |
5570 |
5571 subsection {* Some properties of a canonical subspace *} |
5571 subsection {* Some properties of a canonical subspace *} |
5572 |
5572 |
5573 (** move **) |
5573 (** move **) |
5574 declare euclidean_component.zero[simp] |
5574 declare euclidean_component_zero[simp] |
5575 |
5575 |
5576 lemma subspace_substandard: |
5576 lemma subspace_substandard: |
5577 "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}" |
5577 "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}" |
5578 unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *) |
5578 unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *) |
5579 |
5579 |
6025 |
6025 |
6026 text {* Legacy theorem names *} |
6026 text {* Legacy theorem names *} |
6027 |
6027 |
6028 lemmas Lim_ident_at = LIM_ident |
6028 lemmas Lim_ident_at = LIM_ident |
6029 lemmas Lim_const = tendsto_const |
6029 lemmas Lim_const = tendsto_const |
6030 lemmas Lim_cmul = scaleR.tendsto [OF tendsto_const] |
6030 lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const] |
6031 lemmas Lim_neg = tendsto_minus |
6031 lemmas Lim_neg = tendsto_minus |
6032 lemmas Lim_add = tendsto_add |
6032 lemmas Lim_add = tendsto_add |
6033 lemmas Lim_sub = tendsto_diff |
6033 lemmas Lim_sub = tendsto_diff |
6034 lemmas Lim_mul = scaleR.tendsto |
6034 lemmas Lim_mul = tendsto_scaleR |
6035 lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const] |
6035 lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const] |
6036 lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric] |
6036 lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric] |
6037 lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl] |
6037 lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl] |
6038 lemmas Lim_component = euclidean_component.tendsto |
6038 lemmas Lim_component = tendsto_euclidean_component |
6039 lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id |
6039 lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id |
6040 |
6040 |
6041 end |
6041 end |