Moved analysis material from AFP
authorManuel Eberl <eberlm@in.tum.de>
Tue Dec 12 10:01:14 2017 +0100 (17 months ago)
changeset 6716788d1c9d86f48
parent 67166 a77d54ef718b
child 67168 bea1258d9a27
Moved analysis material from AFP
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Infinite_Set_Sum.thy
src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Dec 11 17:28:32 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Dec 12 10:01:14 2017 +0100
     1.3 @@ -379,6 +379,28 @@
     1.4    "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
     1.5    by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
     1.6  
     1.7 +lemma holomorphic_on_Un [holomorphic_intros]:
     1.8 +  assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
     1.9 +  shows   "f holomorphic_on (A \<union> B)"
    1.10 +  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A] 
    1.11 +                             at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
    1.12 +
    1.13 +lemma holomorphic_on_If_Un [holomorphic_intros]:
    1.14 +  assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B"
    1.15 +  assumes "\<And>z. z \<in> A \<Longrightarrow> z \<in> B \<Longrightarrow> f z = g z"
    1.16 +  shows   "(\<lambda>z. if z \<in> A then f z else g z) holomorphic_on (A \<union> B)" (is "?h holomorphic_on _")
    1.17 +proof (intro holomorphic_on_Un)
    1.18 +  note \<open>f holomorphic_on A\<close>
    1.19 +  also have "f holomorphic_on A \<longleftrightarrow> ?h holomorphic_on A"
    1.20 +    by (intro holomorphic_cong) auto
    1.21 +  finally show \<dots> .
    1.22 +next
    1.23 +  note \<open>g holomorphic_on B\<close>
    1.24 +  also have "g holomorphic_on B \<longleftrightarrow> ?h holomorphic_on B"
    1.25 +    using assms by (intro holomorphic_cong) auto
    1.26 +  finally show \<dots> .
    1.27 +qed (insert assms, auto)
    1.28 +
    1.29  lemma DERIV_deriv_iff_field_differentiable:
    1.30    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
    1.31    unfolding field_differentiable_def by (metis DERIV_imp_deriv)
     2.1 --- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Mon Dec 11 17:28:32 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Tue Dec 12 10:01:14 2017 +0100
     2.3 @@ -256,6 +256,27 @@
     2.4      show "f abs_summable_on insert x A" by simp
     2.5  qed
     2.6  
     2.7 +lemma abs_summable_sum: 
     2.8 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
     2.9 +  shows   "(\<lambda>y. \<Sum>x\<in>A. f x y) abs_summable_on B"
    2.10 +  using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
    2.11 +
    2.12 +lemma abs_summable_Re: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Re (f x)) abs_summable_on A"
    2.13 +  by (simp add: abs_summable_on_def)
    2.14 +
    2.15 +lemma abs_summable_Im: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. Im (f x)) abs_summable_on A"
    2.16 +  by (simp add: abs_summable_on_def)
    2.17 +
    2.18 +lemma abs_summable_on_finite_diff:
    2.19 +  assumes "f abs_summable_on A" "A \<subseteq> B" "finite (B - A)"
    2.20 +  shows   "f abs_summable_on B"
    2.21 +proof -
    2.22 +  have "f abs_summable_on (A \<union> (B - A))"
    2.23 +    by (intro abs_summable_on_union assms abs_summable_on_finite)
    2.24 +  also from assms have "A \<union> (B - A) = B" by blast
    2.25 +  finally show ?thesis .
    2.26 +qed
    2.27 +
    2.28  lemma abs_summable_on_reindex_bij_betw:
    2.29    assumes "bij_betw g A B"
    2.30    shows   "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B"
    2.31 @@ -407,6 +428,27 @@
    2.32  lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0"
    2.33    by simp
    2.34  
    2.35 +lemma infsetsum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> f x \<ge> (0::real)) \<Longrightarrow> infsetsum f A \<ge> 0"
    2.36 +  unfolding infsetsum_def by (rule Bochner_Integration.integral_nonneg) auto
    2.37 +
    2.38 +lemma sum_infsetsum:
    2.39 +  assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
    2.40 +  shows   "(\<Sum>x\<in>A. \<Sum>\<^sub>ay\<in>B. f x y) = (\<Sum>\<^sub>ay\<in>B. \<Sum>x\<in>A. f x y)"
    2.41 +  using assms by (simp add: infsetsum_def abs_summable_on_def Bochner_Integration.integral_sum)
    2.42 +
    2.43 +lemma Re_infsetsum: "f abs_summable_on A \<Longrightarrow> Re (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Re (f x))"
    2.44 +  by (simp add: infsetsum_def abs_summable_on_def)
    2.45 +
    2.46 +lemma Im_infsetsum: "f abs_summable_on A \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
    2.47 +  by (simp add: infsetsum_def abs_summable_on_def)
    2.48 +
    2.49 +lemma infsetsum_of_real: 
    2.50 +  shows "infsetsum (\<lambda>x. of_real (f x) 
    2.51 +           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
    2.52 +             of_real (infsetsum f A)"
    2.53 +  unfolding infsetsum_def
    2.54 +  by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
    2.55 +
    2.56  lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
    2.57    by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
    2.58  
     3.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Mon Dec 11 17:28:32 2017 +0100
     3.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Tue Dec 12 10:01:14 2017 +0100
     3.3 @@ -602,6 +602,9 @@
     3.4      by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
     3.5  qed
     3.6  
     3.7 +lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
     3.8 +  unfolding One_nat_def [symmetric] using prime_factorization_1 .
     3.9 +
    3.10  instance int :: normalization_euclidean_semiring ..
    3.11  
    3.12  instance int :: euclidean_ring_gcd
     4.1 --- a/src/HOL/Series.thy	Mon Dec 11 17:28:32 2017 +0100
     4.2 +++ b/src/HOL/Series.thy	Tue Dec 12 10:01:14 2017 +0100
     4.3 @@ -1223,4 +1223,32 @@
     4.4    ultimately show ?thesis by simp
     4.5  qed
     4.6  
     4.7 +lemma summable_bounded_partials:
     4.8 +  fixes f :: "nat \<Rightarrow> 'a :: {real_normed_vector,complete_space}"
     4.9 +  assumes bound: "eventually (\<lambda>x0. \<forall>a\<ge>x0. \<forall>b>a. norm (sum f {a<..b}) \<le> g a) sequentially"
    4.10 +  assumes g: "g \<longlonglongrightarrow> 0"
    4.11 +  shows   "summable f" unfolding summable_iff_convergent'
    4.12 +proof (intro Cauchy_convergent CauchyI', goal_cases)
    4.13 +  case (1 \<epsilon>)
    4.14 +  with g have "eventually (\<lambda>x. \<bar>g x\<bar> < \<epsilon>) sequentially"
    4.15 +    by (auto simp: tendsto_iff)
    4.16 +  from eventually_conj[OF this bound] obtain x0 where x0:
    4.17 +    "\<And>x. x \<ge> x0 \<Longrightarrow> \<bar>g x\<bar> < \<epsilon>" "\<And>a b. x0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> norm (sum f {a<..b}) \<le> g a" 
    4.18 +    unfolding eventually_at_top_linorder by auto
    4.19 +
    4.20 +  show ?case
    4.21 +  proof (intro exI[of _ x0] allI impI)
    4.22 +    fix m n assume mn: "x0 \<le> m" "m < n"
    4.23 +    have "dist (sum f {..m}) (sum f {..n}) = norm (sum f {..n} - sum f {..m})"
    4.24 +      by (simp add: dist_norm norm_minus_commute)
    4.25 +    also have "sum f {..n} - sum f {..m} = sum f ({..n} - {..m})"
    4.26 +      using mn by (intro Groups_Big.sum_diff [symmetric]) auto
    4.27 +    also have "{..n} - {..m} = {m<..n}" using mn by auto
    4.28 +    also have "norm (sum f {m<..n}) \<le> g m" using mn by (intro x0) auto
    4.29 +    also have "\<dots> \<le> \<bar>g m\<bar>" by simp
    4.30 +    also have "\<dots> < \<epsilon>" using mn by (intro x0) auto
    4.31 +    finally show "dist (sum f {..m}) (sum f {..n}) < \<epsilon>" .
    4.32 +  qed
    4.33 +qed
    4.34 +
    4.35  end