Moved material from AFP to Analysis/Number_Theory
authorManuel Eberl <eberlm@in.tum.de>
Tue Dec 05 12:14:36 2017 +0100 (4 months ago)
changeset 671351a94352812f4
parent 67134 66ce07e8dbf2
child 67141 94fca35f80ab
Moved material from AFP to Analysis/Number_Theory
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Winding_Numbers.thy
src/HOL/Library/Nonpos_Ints.thy
src/HOL/Number_Theory/Prime_Powers.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Dec 04 23:10:52 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Dec 05 12:14:36 2017 +0100
     1.3 @@ -367,6 +367,10 @@
     1.4    "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
     1.5    unfolding holomorphic_on_def by (metis field_differentiable_sum)
     1.6  
     1.7 +lemma holomorphic_on_prod [holomorphic_intros]:
     1.8 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on s"
     1.9 +  by (induction I rule: infinite_finite_induct) (auto intro: holomorphic_intros)
    1.10 +
    1.11  lemma holomorphic_pochhammer [holomorphic_intros]:
    1.12    "f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
    1.13    by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Dec 04 23:10:52 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Dec 05 12:14:36 2017 +0100
     2.3 @@ -1790,8 +1790,8 @@
     2.4    shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
     2.5    by (simp_all add: powr_def exp_eq_polar)
     2.6  
     2.7 -lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
     2.8 -  by (metis linear not_le of_real_Re powr_of_real)
     2.9 +lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x \<ge> 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
    2.10 +  by (metis not_le of_real_Re powr_of_real)
    2.11  
    2.12  lemma norm_powr_real_mono:
    2.13      "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
    2.14 @@ -1943,6 +1943,32 @@
    2.15    with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
    2.16  qed
    2.17  
    2.18 +lemma tendsto_neg_powr_complex_of_real:
    2.19 +  assumes "filterlim f at_top F" and "Re s < 0"
    2.20 +  shows   "((\<lambda>x. complex_of_real (f x) powr s) \<longlongrightarrow> 0) F"
    2.21 +proof -
    2.22 +  have "((\<lambda>x. norm (complex_of_real (f x) powr s)) \<longlongrightarrow> 0) F"
    2.23 +  proof (rule Lim_transform_eventually)
    2.24 +    from assms(1) have "eventually (\<lambda>x. f x \<ge> 0) F"
    2.25 +      by (auto simp: filterlim_at_top)
    2.26 +    thus "eventually (\<lambda>x. f x powr Re s = norm (of_real (f x) powr s)) F"
    2.27 +      by eventually_elim (simp add: norm_powr_real_powr)
    2.28 +    from assms show "((\<lambda>x. f x powr Re s) \<longlongrightarrow> 0) F"
    2.29 +      by (intro tendsto_neg_powr)
    2.30 +  qed
    2.31 +  thus ?thesis by (simp add: tendsto_norm_zero_iff)
    2.32 +qed
    2.33 +
    2.34 +lemma tendsto_neg_powr_complex_of_nat:
    2.35 +  assumes "filterlim f at_top F" and "Re s < 0"
    2.36 +  shows   "((\<lambda>x. of_nat (f x) powr s) \<longlongrightarrow> 0) F"
    2.37 +proof -
    2.38 +  have "((\<lambda>x. of_real (real (f x)) powr s) \<longlongrightarrow> 0) F" using assms(2)
    2.39 +    by (intro filterlim_compose[OF _ tendsto_neg_powr_complex_of_real]
    2.40 +              filterlim_compose[OF _ assms(1)] filterlim_real_sequentially filterlim_ident) auto
    2.41 +  thus ?thesis by simp
    2.42 +qed
    2.43 +
    2.44  lemma continuous_powr_complex:
    2.45    assumes "f (netlimit F) \<notin> \<real>\<^sub>\<le>\<^sub>0" "continuous F f" "continuous F g"
    2.46    shows   "continuous F (\<lambda>z. f z powr g z :: complex)"
     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Mon Dec 04 23:10:52 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Dec 05 12:14:36 2017 +0100
     3.3 @@ -2991,6 +2991,17 @@
     3.4      by (auto elim!: no_isolated_singularity)
     3.5  qed
     3.6  
     3.7 +lemma not_is_pole_holomorphic:
     3.8 +  assumes "open A" "x \<in> A" "f holomorphic_on A"
     3.9 +  shows   "\<not>is_pole f x"
    3.10 +proof -
    3.11 +  have "continuous_on A f" by (intro holomorphic_on_imp_continuous_on) fact
    3.12 +  with assms have "isCont f x" by (simp add: continuous_on_eq_continuous_at)
    3.13 +  hence "f \<midarrow>x\<rightarrow> f x" by (simp add: isCont_def)
    3.14 +  thus "\<not>is_pole f x" unfolding is_pole_def
    3.15 +    using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto
    3.16 +qed
    3.17 +
    3.18  
    3.19  (*order of the zero of f at z*)
    3.20  definition zorder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Dec 04 23:10:52 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Dec 05 12:14:36 2017 +0100
     4.3 @@ -279,7 +279,31 @@
     4.4    by (auto simp: convex_bound_lt inner_add)
     4.5  
     4.6  lemma convex_halfspace_gt: "convex {x. inner a x > b}"
     4.7 -   using convex_halfspace_lt[of "-a" "-b"] by auto
     4.8 +  using convex_halfspace_lt[of "-a" "-b"] by auto
     4.9 +
    4.10 +lemma convex_halfspace_Re_ge: "convex {x. Re x \<ge> b}"
    4.11 +  using convex_halfspace_ge[of b "1::complex"] by simp
    4.12 +
    4.13 +lemma convex_halfspace_Re_le: "convex {x. Re x \<le> b}"
    4.14 +  using convex_halfspace_le[of "1::complex" b] by simp
    4.15 +
    4.16 +lemma convex_halfspace_Im_ge: "convex {x. Im x \<ge> b}"
    4.17 +  using convex_halfspace_ge[of b \<i>] by simp
    4.18 +
    4.19 +lemma convex_halfspace_Im_le: "convex {x. Im x \<le> b}"
    4.20 +  using convex_halfspace_le[of \<i> b] by simp
    4.21 +
    4.22 +lemma convex_halfspace_Re_gt: "convex {x. Re x > b}"
    4.23 +  using convex_halfspace_gt[of b "1::complex"] by simp
    4.24 +
    4.25 +lemma convex_halfspace_Re_lt: "convex {x. Re x < b}"
    4.26 +  using convex_halfspace_lt[of "1::complex" b] by simp
    4.27 +
    4.28 +lemma convex_halfspace_Im_gt: "convex {x. Im x > b}"
    4.29 +  using convex_halfspace_gt[of b \<i>] by simp
    4.30 +
    4.31 +lemma convex_halfspace_Im_lt: "convex {x. Im x < b}"
    4.32 +  using convex_halfspace_lt[of \<i> b] by simp
    4.33  
    4.34  lemma convex_real_interval [iff]:
    4.35    fixes a b :: "real"
     5.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Dec 04 23:10:52 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Dec 05 12:14:36 2017 +0100
     5.3 @@ -819,6 +819,11 @@
     5.4      unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg)
     5.5  qed
     5.6  
     5.7 +lemma lebesgue_real_scale:
     5.8 +  assumes "c \<noteq> 0"
     5.9 +  shows   "lebesgue = density (distr lebesgue lebesgue (\<lambda>x. c * x)) (\<lambda>x. ennreal \<bar>c\<bar>)"
    5.10 +  using assms by (subst lebesgue_affine_euclidean[of "\<lambda>_. c" 0]) simp_all
    5.11 +
    5.12  lemma divideR_right:
    5.13    fixes x y :: "'a::real_normed_vector"
    5.14    shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
     6.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Dec 04 23:10:52 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Dec 05 12:14:36 2017 +0100
     6.3 @@ -706,7 +706,7 @@
     6.4        - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
     6.5        using z_notin_ed z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
     6.6        by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
     6.7 -    show "- complex_of_real d \<noteq> complex_of_real e"
     6.8 +    show "- d \<noteq> e"
     6.9        using ad_not_ae by auto
    6.10      show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z \<noteq> 0"
    6.11        using z1 by auto
     7.1 --- a/src/HOL/Library/Nonpos_Ints.thy	Mon Dec 04 23:10:52 2017 +0100
     7.2 +++ b/src/HOL/Library/Nonpos_Ints.thy	Tue Dec 05 12:14:36 2017 +0100
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:    HOL/Library/Nonpos_Ints.thy
     7.5 +  (*  Title:    HOL/Library/Nonpos_Ints.thy
     7.6      Author:   Manuel Eberl, TU M√ľnchen
     7.7  *)
     7.8  
     7.9 @@ -237,7 +237,6 @@
    7.10  lemma uminus_nonneg_Reals_iff [simp]: "-x \<in> \<real>\<^sub>\<ge>\<^sub>0 \<longleftrightarrow> x \<in> \<real>\<^sub>\<le>\<^sub>0"
    7.11    apply (auto simp: nonpos_Reals_def nonneg_Reals_def)
    7.12    apply (metis nonpos_Reals_of_real_iff minus_minus neg_le_0_iff_le of_real_minus)
    7.13 -  apply (metis neg_0_le_iff_le of_real_minus)
    7.14    done
    7.15  
    7.16  lemma uminus_nonpos_Reals_iff [simp]: "-x \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> x \<in> \<real>\<^sub>\<ge>\<^sub>0"
     8.1 --- a/src/HOL/Number_Theory/Prime_Powers.thy	Mon Dec 04 23:10:52 2017 +0100
     8.2 +++ b/src/HOL/Number_Theory/Prime_Powers.thy	Tue Dec 05 12:14:36 2017 +0100
     8.3 @@ -127,6 +127,12 @@
     8.4  lemma primepow_not_unit [simp]: "primepow p \<Longrightarrow> \<not>is_unit p"
     8.5    by (auto simp: primepow_def is_unit_power_iff)
     8.6  
     8.7 +lemma not_primepow_Suc_0_nat [simp]: "\<not>primepow (Suc 0)"
     8.8 +  using primepow_gt_Suc_0[of "Suc 0"] by auto
     8.9 +
    8.10 +lemma primepow_gt_0_nat: "primepow n \<Longrightarrow> n > (0::nat)"
    8.11 +  using primepow_gt_Suc_0[of n] by simp
    8.12 +
    8.13  lemma unit_factor_primepow: "primepow p \<Longrightarrow> unit_factor p = 1"
    8.14    by (auto simp: primepow_def unit_factor_power)
    8.15  
    8.16 @@ -204,6 +210,10 @@
    8.17      by (auto simp: primepow_def power_mult intro!: exI[of _ q] exI[of _ "k * n"])
    8.18  qed
    8.19  
    8.20 +lemma primepow_power_iff_nat:
    8.21 +  "p > 0 \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> primepow (p :: nat) \<and> n > 0"
    8.22 +  by (rule primepow_power_iff) (simp_all add: unit_factor_nat_def)
    8.23 +
    8.24  lemma primepow_prime [simp]: "prime n \<Longrightarrow> primepow n"
    8.25    by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"])
    8.26  
    8.27 @@ -211,6 +221,51 @@
    8.28      "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
    8.29    by (subst primepow_power_iff) auto
    8.30  
    8.31 +lemma aprimedivisor_vimage:
    8.32 +  assumes "prime (p :: 'a :: factorial_semiring)"
    8.33 +  shows   "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
    8.34 +proof safe
    8.35 +  fix q assume q: "q \<in> primepow_factors n"
    8.36 +  hence q': "q \<noteq> 0" "q \<noteq> 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one)
    8.37 +  let ?n = "multiplicity (aprimedivisor q) q"
    8.38 +  from q q' have "q = aprimedivisor q ^ ?n \<and> ?n > 0 \<and> aprimedivisor q ^ ?n dvd n"
    8.39 +    by (auto simp: primepow_decompose primepow_factors_def prime_multiplicity_gt_zero_iff
    8.40 +          prime_aprimedivisor' prime_imp_prime_elem aprimedivisor_dvd')
    8.41 +  thus "\<exists>k. q = aprimedivisor q ^ k \<and> k > 0 \<and> aprimedivisor q ^ k dvd n" ..
    8.42 +next
    8.43 +  fix k :: nat assume k: "p ^ k dvd n" "k > 0"
    8.44 +  with assms show "p ^ k \<in> aprimedivisor -` {p}"
    8.45 +    by (auto simp: aprimedivisor_prime_power)
    8.46 +  with assms k show "p ^ k \<in> primepow_factors n"
    8.47 +    by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI)
    8.48 +qed
    8.49 +
    8.50 +lemma aprimedivisor_nat:
    8.51 +  assumes "n \<noteq> (Suc 0::nat)"
    8.52 +  shows   "prime (aprimedivisor n)" "aprimedivisor n dvd n"
    8.53 +proof -
    8.54 +  from assms have "\<exists>p. prime p \<and> p dvd n" by (intro prime_factor_nat) auto
    8.55 +  from someI_ex[OF this, folded aprimedivisor_def] 
    8.56 +    show "prime (aprimedivisor n)" "aprimedivisor n dvd n" by blast+
    8.57 +qed
    8.58 +  
    8.59 +lemma aprimedivisor_gt_Suc_0:
    8.60 +  assumes "n \<noteq> Suc 0"
    8.61 +  shows   "aprimedivisor n > Suc 0"
    8.62 +proof -
    8.63 +  from assms have "prime (aprimedivisor n)" by (rule aprimedivisor_nat)
    8.64 +  thus "aprimedivisor n > Suc 0" by (simp add: prime_nat_iff)
    8.65 +qed
    8.66 +
    8.67 +lemma aprimedivisor_le_nat:
    8.68 +  assumes "n > Suc 0"
    8.69 +  shows   "aprimedivisor n \<le> n"
    8.70 +proof -
    8.71 +  from assms have "aprimedivisor n dvd n" by (intro aprimedivisor_nat) simp_all
    8.72 +  with assms show "aprimedivisor n \<le> n"
    8.73 +    by (intro dvd_imp_le) simp_all
    8.74 +qed
    8.75 +
    8.76  lemma bij_betw_primepows: 
    8.77    "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring) 
    8.78       (Collect prime \<times> UNIV) (Collect primepow)"
    8.79 @@ -260,28 +315,7 @@
    8.80    by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric],
    8.81        subst primepow_prime_power) 
    8.82       (insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0)
    8.83 -
    8.84 -lemma aprimedivisor_vimage:
    8.85 -  assumes "prime (p :: 'a :: factorial_semiring)"
    8.86 -  shows   "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
    8.87 -proof safe
    8.88 -  fix q assume q: "q \<in> primepow_factors n"
    8.89 -  hence q': "q \<noteq> 0" "q \<noteq> 1" by (auto simp: primepow_def primepow_factors_def prime_power_not_one)
    8.90 -  let ?n = "multiplicity (aprimedivisor q) q"
    8.91 -  from q q' have "q = aprimedivisor q ^ ?n \<and> ?n > 0 \<and> aprimedivisor q ^ ?n dvd n"
    8.92 -    using prime_aprimedivisor'[of q] aprimedivisor_dvd'[of q]
    8.93 -    by (subst primepow_decompose [symmetric])
    8.94 -       (auto simp: primepow_factors_def multiplicity_gt_zero_iff unit_factor_primepow
    8.95 -             intro: dvd_trans[OF multiplicity_dvd])
    8.96 -  thus "\<exists>k. q = aprimedivisor q ^ k \<and> k > 0 \<and> aprimedivisor q ^ k dvd n" ..
    8.97 -next
    8.98 -  fix k :: nat assume k: "p ^ k dvd n" "k > 0"
    8.99 -  with assms show "p ^ k \<in> aprimedivisor -` {p}"
   8.100 -    by (auto simp: aprimedivisor_prime_power)
   8.101 -  with assms k show "p ^ k \<in> primepow_factors n"
   8.102 -    by (auto simp: primepow_factors_def primepow_def aprimedivisor_prime_power intro: Suc_leI)
   8.103 -qed
   8.104 -  
   8.105 + 
   8.106  lemma primepow_factors_altdef:
   8.107    fixes x :: "'a :: factorial_semiring"
   8.108    assumes "x \<noteq> 0"
   8.109 @@ -307,6 +341,84 @@
   8.110    finally show ?thesis .
   8.111  qed
   8.112  
   8.113 +lemma aprimedivisor_primepow_factors_conv_prime_factorization:
   8.114 +  assumes [simp]: "n \<noteq> (0 :: 'a :: factorial_semiring)"
   8.115 +  shows   "image_mset aprimedivisor (mset_set (primepow_factors n)) = prime_factorization n" 
   8.116 +          (is "?lhs = ?rhs")
   8.117 +proof (intro multiset_eqI)
   8.118 +  fix p :: 'a
   8.119 +  show "count ?lhs p = count ?rhs p"
   8.120 +  proof (cases "prime p")
   8.121 +    case False
   8.122 +    have "p \<notin># image_mset aprimedivisor (mset_set (primepow_factors n))"
   8.123 +    proof
   8.124 +      assume "p \<in># image_mset aprimedivisor (mset_set (primepow_factors n))"
   8.125 +      then obtain q where "p = aprimedivisor q" "q \<in> primepow_factors n"
   8.126 +        by (auto simp: finite_primepow_factors)
   8.127 +      with False prime_aprimedivisor'[of q] have "q = 0 \<or> is_unit q" by auto
   8.128 +      with \<open>q \<in> primepow_factors n\<close> show False by (auto simp: primepow_factors_def primepow_def)
   8.129 +    qed
   8.130 +    hence "count ?lhs p = 0" by (simp only: Multiset.not_in_iff)
   8.131 +    with False show ?thesis by (simp add: count_prime_factorization)
   8.132 +  next
   8.133 +    case True
   8.134 +    hence p: "p \<noteq> 0" "\<not>is_unit p" by auto
   8.135 +    have "count ?lhs p = card (aprimedivisor -` {p} \<inter> primepow_factors n)"
   8.136 +      by (simp add: count_image_mset finite_primepow_factors)
   8.137 +    also have "aprimedivisor -` {p} \<inter> primepow_factors n = {p^k |k. k > 0 \<and> p ^ k dvd n}"
   8.138 +      using True by (rule aprimedivisor_vimage)
   8.139 +    also from True have "\<dots> = (\<lambda>k. p ^ k) ` {0<..multiplicity p n}"
   8.140 +      by (subst power_dvd_iff_le_multiplicity) auto
   8.141 +    also from p True have "card \<dots> = multiplicity p n"
   8.142 +      by (subst card_image) (auto intro!: inj_onI dest: prime_power_inj)
   8.143 +    also from True have "\<dots> = count (prime_factorization n) p" 
   8.144 +      by (simp add: count_prime_factorization)
   8.145 +    finally show ?thesis .
   8.146 +  qed
   8.147 +qed
   8.148 +
   8.149 +lemma prime_elem_aprimedivisor_nat: "d > Suc 0 \<Longrightarrow> prime_elem (aprimedivisor d)"
   8.150 +  using prime_aprimedivisor'[of d] by simp
   8.151 +
   8.152 +lemma aprimedivisor_gt_0_nat [simp]: "d > Suc 0 \<Longrightarrow> aprimedivisor d > 0"
   8.153 +  using prime_aprimedivisor'[of d] by (simp add: prime_gt_0_nat)
   8.154 +
   8.155 +lemma aprimedivisor_gt_Suc_0_nat [simp]: "d > Suc 0 \<Longrightarrow> aprimedivisor d > Suc 0"
   8.156 +  using prime_aprimedivisor'[of d] by (simp add: prime_gt_Suc_0_nat)
   8.157 +
   8.158 +lemma aprimedivisor_not_Suc_0_nat [simp]: "d > Suc 0 \<Longrightarrow> aprimedivisor d \<noteq> Suc 0"
   8.159 +  using aprimedivisor_gt_Suc_0[of d] by (intro notI) auto
   8.160 +
   8.161 +lemma multiplicity_aprimedivisor_gt_0_nat [simp]:
   8.162 +  "d > Suc 0 \<Longrightarrow> multiplicity (aprimedivisor d) d > 0"
   8.163 +  by (subst multiplicity_gt_zero_iff) (auto intro: aprimedivisor_dvd')
   8.164 +
   8.165 +lemma primepowI:
   8.166 +  "prime p \<Longrightarrow> k > 0 \<Longrightarrow> p ^ k = n \<Longrightarrow> primepow n \<and> aprimedivisor n = p"
   8.167 +  unfolding primepow_def by (auto simp: aprimedivisor_prime_power)
   8.168 +
   8.169 +lemma not_primepowI:
   8.170 +  assumes "prime p" "prime q" "p \<noteq> q" "p dvd n" "q dvd n"
   8.171 +  shows   "\<not>primepow n"
   8.172 +  using assms by (auto simp: primepow_def dest!: prime_dvd_power[rotated] dest: primes_dvd_imp_eq)
   8.173 +
   8.174 +lemma sum_prime_factorization_conv_sum_primepow_factors:
   8.175 +  assumes "n \<noteq> 0"
   8.176 +  shows "(\<Sum>q\<in>primepow_factors n. f (aprimedivisor q)) = (\<Sum>p\<in>#prime_factorization n. f p)"
   8.177 +proof -
   8.178 +  from assms have "prime_factorization n = image_mset aprimedivisor (mset_set (primepow_factors n))"
   8.179 +    by (rule aprimedivisor_primepow_factors_conv_prime_factorization [symmetric])
   8.180 +  also have "(\<Sum>p\<in>#\<dots>. f p) = (\<Sum>q\<in>primepow_factors n. f (aprimedivisor q))"
   8.181 +    by (simp add: image_mset.compositionality sum_unfold_sum_mset o_def)
   8.182 +  finally show ?thesis ..
   8.183 +qed    
   8.184 +
   8.185 +lemma multiplicity_aprimedivisor_Suc_0_iff:
   8.186 +  assumes "primepow (n :: 'a :: factorial_semiring)"
   8.187 +  shows   "multiplicity (aprimedivisor n) n = Suc 0 \<longleftrightarrow> prime n"
   8.188 +  by (subst (3) primepow_decompose [OF assms, symmetric])
   8.189 +     (insert assms, auto simp add: prime_power_iff intro!: prime_aprimedivisor')
   8.190 +
   8.191  
   8.192  definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where
   8.193    "mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"
   8.194 @@ -342,5 +454,50 @@
   8.195    also have "\<dots> = n" using assms by (intro prime_factorization_nat [symmetric]) simp
   8.196    finally show ?thesis .
   8.197  qed
   8.198 -  
   8.199 +
   8.200 +lemma mangoldt_primepow:
   8.201 +   "prime p \<Longrightarrow> mangoldt (p ^ k) = (if k > 0 then of_real (ln (real p)) else 0)"
   8.202 +  by (simp add: mangoldt_def aprimedivisor_prime_power)
   8.203 +
   8.204 +lemma mangoldt_primepow' [simp]: "prime p \<Longrightarrow> k > 0 \<Longrightarrow> mangoldt (p ^ k) = of_real (ln (real p))"
   8.205 +  by (subst mangoldt_primepow) auto
   8.206 +
   8.207 +lemma mangoldt_prime [simp]: "prime p \<Longrightarrow> mangoldt p = of_real (ln (real p))"    
   8.208 +  using mangoldt_primepow[of p 1] by simp
   8.209 +
   8.210 +lemma mangoldt_nonneg: "0 \<le> (mangoldt d :: real)"
   8.211 +  using aprimedivisor_gt_Suc_0_nat[of d]
   8.212 +  by (auto simp: mangoldt_def of_nat_le_iff[of 1 x for x, unfolded of_nat_1] Suc_le_eq
   8.213 +           intro!: ln_ge_zero dest: primepow_gt_Suc_0)
   8.214 +
   8.215 +lemma norm_mangoldt [simp]:
   8.216 +  "norm (mangoldt n :: 'a :: real_normed_algebra_1) = mangoldt n"
   8.217 +proof (cases "primepow n")
   8.218 +  case True
   8.219 +  hence "prime (aprimedivisor n)"
   8.220 +    by (intro prime_aprimedivisor') 
   8.221 +       (auto simp: primepow_def prime_gt_0_nat)
   8.222 +  hence "aprimedivisor n > 1" by (simp add: prime_gt_Suc_0_nat)
   8.223 +  with True show ?thesis by (auto simp: mangoldt_def abs_if)
   8.224 +qed (auto simp: mangoldt_def)
   8.225 +
   8.226 +lemma abs_mangoldt [simp]: "abs (mangoldt n :: real) = mangoldt n"
   8.227 +  using norm_mangoldt[of n, where ?'a = real, unfolded real_norm_def] .
   8.228 +
   8.229 +lemma mangoldt_le: 
   8.230 +  assumes "n > 0"
   8.231 +  shows   "mangoldt n \<le> ln n"
   8.232 +proof (cases "primepow n")
   8.233 +  case True
   8.234 +  from True have "prime (aprimedivisor n)"
   8.235 +    by (intro prime_aprimedivisor') 
   8.236 +       (auto simp: primepow_def prime_gt_0_nat)
   8.237 +  hence gt_1: "aprimedivisor n > 1" by (simp add: prime_gt_Suc_0_nat)
   8.238 +  from True have "mangoldt n = ln (aprimedivisor n)"
   8.239 +    by (simp add: mangoldt_def)
   8.240 +  also have "\<dots> \<le> ln n" using True gt_1 
   8.241 +    by (subst ln_le_cancel_iff) (auto intro!: Nat.gr0I dvd_imp_le aprimedivisor_dvd')
   8.242 +  finally show ?thesis .
   8.243 +qed (insert assms, auto simp: mangoldt_def)
   8.244 +
   8.245  end
   8.246 \ No newline at end of file
     9.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Dec 04 23:10:52 2017 +0100
     9.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Dec 05 12:14:36 2017 +0100
     9.3 @@ -366,6 +366,12 @@
     9.4  lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
     9.5  lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified]
     9.6  
     9.7 +lemma minus_of_real_eq_of_real_iff [simp]: "-of_real x = of_real y \<longleftrightarrow> -x = y"
     9.8 +  using of_real_eq_iff[of "-x" y] by (simp only: of_real_minus)
     9.9 +
    9.10 +lemma of_real_eq_minus_of_real_iff [simp]: "of_real x = -of_real y \<longleftrightarrow> x = -y"
    9.11 +  using of_real_eq_iff[of x "-y"] by (simp only: of_real_minus)
    9.12 +
    9.13  lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
    9.14    by (rule ext) (simp add: of_real_def)
    9.15  
    9.16 @@ -445,10 +451,7 @@
    9.17    done
    9.18  
    9.19  lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
    9.20 -  apply (auto simp add: Reals_def)
    9.21 -  apply (rule range_eqI)
    9.22 -  apply (rule of_real_minus [symmetric])
    9.23 -  done
    9.24 +  by (auto simp add: Reals_def)
    9.25  
    9.26  lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
    9.27    apply (auto simp add: Reals_def)