diff --git a/thys/Buffons_Needle/Buffons_Needle.thy b/thys/Buffons_Needle/Buffons_Needle.thy --- a/thys/Buffons_Needle/Buffons_Needle.thy +++ b/thys/Buffons_Needle/Buffons_Needle.thy @@ -1,487 +1,442 @@ (* File: Buffons_Needle.thy Author: Manuel Eberl A formal solution of Buffon's needle problem. *) section \Buffon's Needle Problem\ theory Buffons_Needle imports "HOL-Probability.Probability" begin subsection \Auxiliary material\ lemma sin_le_zero': "sin x \ 0" if "x \ -pi" "x \ 0" for x by (metis minus_le_iff neg_0_le_iff_le sin_ge_zero sin_minus that(1) that(2)) -lemma emeasure_Un': - assumes "A \ sets M" "B \ sets M" "A \ B \ null_sets M" - shows "emeasure M (A \ B) = emeasure M A + emeasure M B" -proof - - have "A \ B = A \ (B - A \ B)" by blast - also have "emeasure M \ = emeasure M A + emeasure M (B - A \ B)" - using assms by (subst plus_emeasure) auto - also have "emeasure M (B - A \ B) = emeasure M B" - using assms by (intro emeasure_Diff_null_set) auto - finally show ?thesis . -qed - -lemma integral_shift: - fixes f :: "real \ 'a::euclidean_space" - assumes cont: "continuous_on {a + c..b + c} f" - shows "integral {a..b} (f \ (\x. x + c)) = integral {a + c..b + c} f" -proof (cases "a \ b") - case True - have "((\x. 1 *\<^sub>R f (x + c)) has_integral integral {a+c..b+c} f) {a..b}" - using True cont - by (intro has_integral_substitution[where c = "a + c" and d = "b + c"]) - (auto intro!: derivative_eq_intros) - thus ?thesis by (simp add: has_integral_iff o_def) -qed auto - -lemma arcsin_le_iff: - assumes "x \ -1" "x \ 1" "y \ -pi/2" "y \ pi/2" - shows "arcsin x \ y \ x \ sin y" -proof - - have "arcsin x \ y \ sin (arcsin x) \ sin y" - using arcsin_bounded[of x] assms by (subst sin_mono_le_eq) auto - also from assms have "sin (arcsin x) = x" by simp - finally show ?thesis . -qed - -lemma le_arcsin_iff: - assumes "x \ -1" "x \ 1" "y \ -pi/2" "y \ pi/2" - shows "arcsin x \ y \ x \ sin y" -proof - - have "arcsin x \ y \ sin (arcsin x) \ sin y" - using arcsin_bounded[of x] assms by (subst sin_mono_le_eq) auto - also from assms have "sin (arcsin x) = x" by simp - finally show ?thesis . -qed - subsection \Problem definition\ text \ Consider a needle of length $l$ whose centre has the $x$-coordinate $x$. The following then defines the set of all $x$-coordinates that the needle covers (i.e. the projection of the needle onto the $x$-axis.) \ definition needle :: "real \ real \ real \ real set" where "needle l x \ = closed_segment (x - l / 2 * sin \) (x + l / 2 * sin \)" text \ Buffon's Needle problem is then this: Assuming the needle's $x$ position is chosen uniformly at random in a strip of width $d$ centred at the origin, what is the probability that the needle crosses at least one of the left/right boundaries of that strip (located at $x = \pm\frac{1}{2}d$)? \ definition buffon :: "real \ real \ bool measure" where "buffon l d = do { (x, \) \ uniform_measure lborel ({-d/2..d/2} \ {-pi..pi}); return (count_space UNIV) (needle l x \ \ {-d/2, d/2} \ {}) }" subsection \Derivation of the solution\ text \ The following form is a bit easier to handle. \ lemma buffon_altdef: "buffon l d = do { (x, \) \ uniform_measure lborel ({-d/2..d/2} \ {-pi..pi}); return (count_space UNIV) (let a = x - l / 2 * sin \; b = x + l / 2 * sin \ in min a b + d/2 \ 0 \ max a b + d/2 \ 0 \ min a b - d/2 \ 0 \ max a b - d/2 \ 0) }" proof - note buffon_def[of l d] also { have "(\(x,\). needle l x \ \ {-d/2, d/2} \ {}) = (\(x,\). let a = x - l / 2 * sin \; b = x + l / 2 * sin \ in -d/2 \ min a b \ -d/2 \ max a b \ min a b \ d/2 \ max a b \ d/2)" by (auto simp: needle_def Let_def closed_segment_eq_real_ivl min_def max_def) also have "\ = (\(x,\). let a = x - l / 2 * sin \; b = x + l / 2 * sin \ in min a b + d/2 \ 0 \ max a b + d/2 \ 0 \ min a b - d/2 \ 0 \ max a b - d/2 \ 0)" by (auto simp add: algebra_simps Let_def) finally have "(\(x, \). return (count_space UNIV) (needle l x \ \ {- d/2, d/2} \ {})) = (\(x,\). return (count_space UNIV) (let a = x - l / 2 * sin \; b = x + l / 2 * sin \ in min a b + d/2 \ 0 \ max a b + d/2 \ 0 \ min a b - d/2 \ 0 \ max a b - d/2 \ 0))" by (simp add: case_prod_unfold fun_eq_iff) } finally show ?thesis . qed text \ It is obvious that the problem boils down to determining the measure of the following set: \ definition buffon_set :: "real \ real \ (real \ real) set" where "buffon_set l d = {(x,\) \ {-d/2..d/2} \ {-pi..pi}. abs x \ d / 2 - abs (sin \) * l / 2}" text \ By using the symmetry inherent in the problem, we can reduce the problem to the following set, which corresponds to one quadrant of the original set: \ definition buffon_set' :: "real \ real \ (real \ real) set" where "buffon_set' l d = {(x,\) \ {0..d/2} \ {0..pi}. x \ d / 2 - sin \ * l / 2}" lemma closed_buffon_set [simp, intro, measurable]: "closed (buffon_set l d)" proof - have "buffon_set l d = ({-d/2..d/2} \ {-pi..pi}) \ (\z. abs (fst z) + abs (sin (snd z)) * l / 2 - d / 2) -` {0..}" (is "_ = ?A") unfolding buffon_set_def by auto also have "closed \" by (intro closed_Int closed_vimage closed_Times) (auto intro!: continuous_intros) finally show ?thesis by simp qed lemma closed_buffon_set' [simp, intro, measurable]: "closed (buffon_set' l d)" proof - have "buffon_set' l d = ({0..d/2} \ {0..pi}) \ (\z. fst z + sin (snd z) * l / 2 - d / 2) -` {0..}" (is "_ = ?A") unfolding buffon_set'_def by auto also have "closed \" by (intro closed_Int closed_vimage closed_Times) (auto intro!: continuous_intros) finally show ?thesis by simp qed lemma measurable_buffon_set [measurable]: "buffon_set l d \ sets borel" by measurable lemma measurable_buffon_set' [measurable]: "buffon_set' l d \ sets borel" by measurable context fixes d l :: real assumes d: "d > 0" and l: "l > 0" begin lemma buffon_altdef': "buffon l d = distr (uniform_measure lborel ({-d/2..d/2} \ {-pi..pi})) (count_space UNIV) (\z. z \ buffon_set l d)" proof - let ?P = "\(x,\). let a = x - l / 2 * sin \; b = x + l / 2 * sin \ in min a b + d/2 \ 0 \ max a b + d/2 \ 0 \ min a b - d/2 \ 0 \ max a b - d/2 \ 0" have "buffon l d = uniform_measure lborel ({- d / 2..d / 2} \ {-pi..pi}) \ (\z. return (count_space UNIV) (?P z))" unfolding buffon_altdef case_prod_unfold by simp also have "\ = uniform_measure lborel ({- d / 2..d / 2} \ {-pi..pi}) \ (\z. return (count_space UNIV) (z \ buffon_set l d))" proof (intro bind_cong_AE AE_uniform_measureI AE_I2 impI refl return_measurable, goal_cases) show "(\z. return (count_space UNIV) (?P z)) \ uniform_measure lborel ({- d / 2..d / 2} \ {- pi..pi}) \\<^sub>M subprob_algebra (count_space UNIV)" unfolding Let_def case_prod_unfold lborel_prod [symmetric] by measurable show "(\z. return (count_space UNIV) (z \ buffon_set l d)) \ uniform_measure lborel ({- d / 2..d / 2} \ {- pi..pi}) \\<^sub>M subprob_algebra (count_space UNIV)" by simp case (4 z) hence "?P z \ z \ buffon_set l d" proof (cases "snd z \ 0") case True with 4 have "fst z - l / 2 * sin (snd z) \ fst z + l / 2 * sin (snd z)" using l by (auto simp: sin_ge_zero) moreover from True and 4 have "sin (snd z) \ 0" by (auto simp: sin_ge_zero) ultimately show ?thesis using 4 True unfolding buffon_set_def by (force simp: field_simps Let_def min_def max_def case_prod_unfold abs_if) next case False with 4 have "fst z - l / 2 * sin (snd z) \ fst z + l / 2 * sin (snd z)" using l by (auto simp: sin_le_zero' mult_nonneg_nonpos) moreover from False and 4 have "sin (snd z) \ 0" by (auto simp: sin_le_zero') ultimately show ?thesis using 4 and False unfolding buffon_set_def using l d by (force simp: field_simps Let_def min_def max_def case_prod_unfold abs_if) qed thus ?case by (simp only: ) qed (simp_all add: borel_prod [symmetric]) also have "\ = distr (uniform_measure lborel ({-d/2..d/2} \ {-pi..pi})) (count_space UNIV) (\z. z \ buffon_set l d)" by (rule bind_return_distr') simp_all finally show ?thesis . qed lemma buffon_prob_aux: "emeasure (buffon l d) {True} = emeasure lborel (buffon_set l d) / ennreal (2 * d * pi)" proof - have [measurable]: "A \ B \ sets borel" if "A \ sets borel" "B \ sets borel" for A B :: "real set" using that unfolding borel_prod [symmetric] by simp have "emeasure (buffon l d) {True} = emeasure (uniform_measure lborel ({- (d / 2)..d / 2} \ {-pi..pi})) ((\z. z \ buffon_set l d) -` {True})" (is "_ = emeasure ?M _") by (simp add: buffon_altdef' emeasure_distr) also have "(\z. z \ buffon_set l d) -` {True} = buffon_set l d" by auto also have "buffon_set l d \ {-d/2..d/2} \ {-pi..pi}" using l d by (auto simp: buffon_set_def) hence "emeasure ?M (buffon_set l d) = emeasure lborel (buffon_set l d) / emeasure lborel ({- (d / 2)..d / 2} \ {-pi..pi})" by (subst emeasure_uniform_measure) (simp_all add: Int_absorb1) also have "emeasure lborel ({- (d / 2)..d / 2} \ {-pi..pi}) = ennreal (2 * pi * d)" using d by (simp add: lborel_prod [symmetric] lborel.emeasure_pair_measure_Times ennreal_mult algebra_simps) finally show ?thesis by (simp add: mult_ac) qed lemma emeasure_buffon_set_conv_buffon_set': "emeasure lborel (buffon_set l d) = 4 * emeasure lborel (buffon_set' l d)" proof - have distr_lborel [simp]: "distr M lborel f = distr M borel f" for M and f :: "real \ real" by (rule distr_cong) simp_all define A where "A = buffon_set' l d" define B C D where "B = (\x. (-fst x, snd x)) -` A" and "C = (\x. (fst x, -snd x)) -` A" and "D = (\x. (-fst x, -snd x)) -` A" have meas [measurable]: "(\x::real \ real. (-fst x, snd x)) \ borel_measurable borel" "(\x::real \ real. (fst x, -snd x)) \ borel_measurable borel" "(\x::real \ real. (-fst x, -snd x)) \ borel_measurable borel" unfolding borel_prod [symmetric] by measurable have meas' [measurable]: "A \ sets borel" "B \ sets borel" "C \ sets borel" "D \ sets borel" unfolding A_def B_def C_def D_def by (rule measurable_buffon_set' measurable_sets_borel meas)+ have *: "buffon_set l d = A \ B \ C \ D" proof (intro equalityI subsetI, goal_cases) case (1 z) show ?case proof (cases "fst z \ 0"; cases "snd z \ 0") assume "fst z \ 0" "snd z \ 0" with 1 have "z \ A" by (auto split: prod.splits simp: buffon_set_def buffon_set'_def sin_ge_zero A_def) thus ?thesis by blast next assume "\(fst z \ 0)" "snd z \ 0" with 1 have "z \ B" by (auto split: prod.splits simp: buffon_set_def buffon_set'_def sin_ge_zero A_def B_def) thus ?thesis by blast next assume "fst z \ 0" "\(snd z \ 0)" with 1 have "z \ C" by (auto split: prod.splits simp: buffon_set_def buffon_set'_def sin_le_zero' A_def C_def) thus ?thesis by blast next assume "\(fst z \ 0)" "\(snd z \ 0)" with 1 have "z \ D" by (auto split: prod.splits simp: buffon_set_def buffon_set'_def sin_le_zero' A_def D_def) thus ?thesis by blast qed qed (auto simp: buffon_set_def buffon_set'_def sin_ge_zero sin_le_zero' A_def B_def C_def D_def) have "A \ B = {0} \ ({0..pi} \ {\. sin \ * l - d \ 0})" using d l by (auto simp: buffon_set'_def A_def B_def C_def D_def) moreover have "emeasure lborel \ = 0" unfolding lborel_prod [symmetric] by (subst lborel.emeasure_pair_measure_Times) simp_all ultimately have AB: "(A \ B) \ null_sets lborel" unfolding lborel_prod [symmetric] by (simp add: null_sets_def) have "C \ D = {0} \ ({-pi..0} \ {\. -sin \ * l - d \ 0})" using d l by (auto simp: buffon_set'_def A_def B_def C_def D_def) moreover have "emeasure lborel \ = 0" unfolding lborel_prod [symmetric] by (subst lborel.emeasure_pair_measure_Times) simp_all ultimately have CD: "(C \ D) \ null_sets lborel" unfolding lborel_prod [symmetric] by (simp add: null_sets_def) have "A \ D = {}" "B \ C = {}" using d l by (auto simp: buffon_set'_def A_def D_def B_def C_def) moreover have "A \ C = {(d/2, 0)}" "B \ D = {(-d/2, 0)}" using d l by (auto simp: case_prod_unfold buffon_set'_def A_def B_def C_def D_def) ultimately have AD: "A \ D \ null_sets lborel" and BC: "B \ C \ null_sets lborel" and AC: "A \ C \ null_sets lborel" and BD: "B \ D \ null_sets lborel" by auto note * also have "emeasure lborel (A \ B \ C \ D) = emeasure lborel (A \ B \ C) + emeasure lborel D" using AB AC AD BC BD CD by (intro emeasure_Un') (auto simp: Int_Un_distrib2) also have "emeasure lborel (A \ B \ C) = emeasure lborel (A \ B) + emeasure lborel C" using AB AC BC using AB AC AD BC BD CD by (intro emeasure_Un') (auto simp: Int_Un_distrib2) also have "emeasure lborel (A \ B) = emeasure lborel A + emeasure lborel B" using AB using AB AC AD BC BD CD by (intro emeasure_Un') (auto simp: Int_Un_distrib2) also have "emeasure lborel B = emeasure (distr lborel lborel (\(x,y). (-x, y))) A" (is "_ = emeasure ?M _") unfolding B_def by (subst emeasure_distr) (simp_all add: case_prod_unfold) also have "?M = lborel" unfolding lborel_prod [symmetric] by (subst pair_measure_distr [symmetric]) (simp_all add: sigma_finite_lborel lborel_distr_uminus) also have "emeasure lborel C = emeasure (distr lborel lborel (\(x,y). (x, -y))) A" (is "_ = emeasure ?M _") unfolding C_def by (subst emeasure_distr) (simp_all add: case_prod_unfold) also have "?M = lborel" unfolding lborel_prod [symmetric] by (subst pair_measure_distr [symmetric]) (simp_all add: sigma_finite_lborel lborel_distr_uminus) also have "emeasure lborel D = emeasure (distr lborel lborel (\(x,y). (-x, -y))) A" (is "_ = emeasure ?M _") unfolding D_def by (subst emeasure_distr) (simp_all add: case_prod_unfold) also have "?M = lborel" unfolding lborel_prod [symmetric] by (subst pair_measure_distr [symmetric]) (simp_all add: sigma_finite_lborel lborel_distr_uminus) finally have "emeasure lborel (buffon_set l d) = of_nat (Suc (Suc (Suc (Suc 0)))) * emeasure lborel A" unfolding of_nat_Suc ring_distribs by simp also have "of_nat (Suc (Suc (Suc (Suc 0)))) = (4 :: ennreal)" by simp finally show ?thesis unfolding A_def . qed text \ It only remains now to compute the measure of @{const buffon_set'}. We first reduce this problem to a relatively simple integral: \ lemma emeasure_buffon_set': "emeasure lborel (buffon_set' l d) = ennreal (integral {0..pi} (\x. min (d / 2) (sin x * l / 2)))" (is "emeasure lborel ?A = _") proof - have "emeasure lborel ?A = nn_integral lborel (\x. indicator ?A x)" by (intro nn_integral_indicator [symmetric]) simp_all also have "(lborel :: (real \ real) measure) = lborel \\<^sub>M lborel" by (simp only: lborel_prod) also have "nn_integral \ (indicator ?A) = (\\<^sup>+\. \\<^sup>+x. indicator ?A (x, \) \lborel \lborel)" by (subst lborel_pair.nn_integral_snd [symmetric]) (simp_all add: lborel_prod borel_prod) also have "\ = (\\<^sup>+\. \\<^sup>+x. indicator {0..pi} \ * indicator {max 0 (d/2 - sin \ * l / 2) .. d/2} x \lborel \lborel)" using d l by (intro nn_integral_cong) (auto simp: indicator_def field_simps buffon_set'_def) also have "\ = \\<^sup>+ \. indicator {0..pi} \ * emeasure lborel {max 0 (d / 2 - sin \ * l / 2)..d / 2} \lborel" by (subst nn_integral_cmult) simp_all also have "\ = \\<^sup>+ \. ennreal (indicator {0..pi} \ * min (d / 2) (sin \ * l / 2)) \lborel" (is "_ = ?I") using d l by (intro nn_integral_cong) (auto simp: indicator_def sin_ge_zero max_def min_def) also have "integrable lborel (\\. (d / 2) * indicator {0..pi} \)" by simp hence int: "integrable lborel (\\. indicator {0..pi} \ * min (d / 2) (sin \ * l / 2))" by (rule Bochner_Integration.integrable_bound) (insert l d, auto intro!: AE_I2 simp: indicator_def min_def sin_ge_zero) hence "?I = set_lebesgue_integral lborel {0..pi} (\\. min (d / 2) (sin \ * l / 2))" by (subst nn_integral_eq_integral, assumption) (insert d l, auto intro!: AE_I2 simp: sin_ge_zero min_def indicator_def set_lebesgue_integral_def) also have "\ = ennreal (integral {0..pi} (\x. min (d / 2) (sin x * l / 2)))" (is "_ = ennreal ?I") using int by (subst set_borel_integral_eq_integral) (simp_all add: set_integrable_def) finally show ?thesis by (simp add: lborel_prod) qed text \ We now have to distinguish two cases: The first and easier one is that where the length of the needle, $l$, is less than or equal to the strip width, $d$: \ context assumes l_le_d: "l \ d" begin lemma emeasure_buffon_set'_short: "emeasure lborel (buffon_set' l d) = ennreal l" proof - have "emeasure lborel (buffon_set' l d) = ennreal (integral {0..pi} (\x. min (d / 2) (sin x * l / 2)))" (is "_ = ennreal ?I") by (rule emeasure_buffon_set') also have *: "sin \ * l \ d" if "\ \ 0" "\ \ pi" for \ using mult_mono[OF l_le_d sin_le_one _ sin_ge_zero] that d by (simp add: algebra_simps) have "?I = integral {0..pi} (\x. (l / 2) * sin x)" using l d l_le_d by (intro integral_cong) (auto dest: * simp: min_def sin_ge_zero) also have "\ = l / 2 * integral {0..pi} sin" by simp also have "(sin has_integral (-cos pi - (- cos 0))) {0..pi}" by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative [symmetric]) hence "integral {0..pi} sin = -cos pi - (-cos 0)" by (simp add: has_integral_iff) finally show ?thesis by (simp add: lborel_prod) qed lemma emeasure_buffon_set_short: "emeasure lborel (buffon_set l d) = 4 * ennreal l" by (simp add: emeasure_buffon_set_conv_buffon_set' emeasure_buffon_set'_short l_le_d) theorem buffon_short: "emeasure (buffon l d) {True} = ennreal (2 * l / (d * pi))" proof - have "emeasure (buffon l d) {True} = ennreal (4 * l) / ennreal (2 * d * pi)" using d l by (subst buffon_prob_aux) (simp add: emeasure_buffon_set_short ennreal_mult) also have "\ = ennreal (4 * l / (2 * d * pi))" using d l by (subst divide_ennreal) simp_all also have "4 * l / (2 * d * pi) = 2 * l / (d * pi)" by simp finally show ?thesis . qed end text \ The other case where the needle is at least as long as the strip width is more complicated: \ context assumes l_ge_d: "l \ d" begin lemma emeasure_buffon_set'_long: "emeasure lborel (buffon_set' l d) = ennreal (l * (1 - sqrt (1 - (d / l)\<^sup>2)) + arccos (d / l) * d)" proof - define \' where "\' = arcsin (d / l)" have \'_nonneg: "\' \ 0" unfolding \'_def using d l l_ge_d arcsin_le_mono[of 0 "d/l"] by (simp add: \'_def) have \'_le: "\' \ pi / 2" unfolding \'_def using arcsin_bounded[of "d/l"] d l l_ge_d by (simp add: field_simps) have ge_phi': "sin \ \ d / l" if "\ \ \'" "\ \ pi / 2" for \ using arcsin_le_iff[of "d / l" "\"] d l_ge_d that \'_nonneg by (auto simp: \'_def field_simps) have le_phi': "sin \ \ d / l" if "\ \ \'" "\ \ 0" for \ using le_arcsin_iff[of "d / l" "\"] d l_ge_d that \'_le by (auto simp: \'_def field_simps) let ?f = "(\x. min (d / 2) (sin x * l / 2))" have "emeasure lborel (buffon_set' l d) = ennreal (integral {0..pi} ?f)" (is "_ = ennreal ?I") by (rule emeasure_buffon_set') also have "?I = integral {0..pi/2} ?f + integral {pi/2..pi} ?f" by (rule Henstock_Kurzweil_Integration.integral_combine [symmetric]) (auto intro!: integrable_continuous_real continuous_intros) also have "integral {pi/2..pi} ?f = integral {-pi/2..0} (?f \ (\\. \ + pi))" by (subst integral_shift) (auto intro!: continuous_intros) also have "\ = integral {-(pi/2)..-0} (\x. min (d / 2) (sin (-x) * l / 2))" by (simp add: o_def) also have "\ = integral {0..pi/2} ?f" (is "_ = ?I") by (subst Henstock_Kurzweil_Integration.integral_reflect_real) simp_all also have "\ + \ = 2 * \" by simp also have "?I = integral {0..\'} ?f + integral {\'..pi/2} ?f" using l d l_ge_d \'_nonneg \'_le by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric]) (auto intro!: integrable_continuous_real continuous_intros) also have "integral {0..\'} ?f = integral {0..\'} (\x. l / 2 * sin x)" using l by (intro integral_cong) (auto simp: min_def field_simps dest: le_phi') also have "((\x. l / 2 * sin x) has_integral (- (l / 2 * cos \') - (- (l / 2 * cos 0)))) {0..\'}" using \'_nonneg by (intro fundamental_theorem_of_calculus) (auto simp: has_field_derivative_iff_has_vector_derivative [symmetric] intro!: derivative_eq_intros) hence "integral {0..\'} (\x. l / 2 * sin x) = (1 - cos \') * l / 2" by (simp add: has_integral_iff algebra_simps) also have "integral {\'..pi/2} ?f = integral {\'..pi/2} (\_. d / 2)" using l by (intro integral_cong) (auto simp: min_def field_simps dest: ge_phi') also have "\ = arccos (d / l) * d / 2" using \'_le d l l_ge_d by (subst arccos_arcsin_eq) (auto simp: field_simps \'_def) also have "cos \' = sqrt (1 - (d / l)^2)" unfolding \'_def by (rule cos_arcsin) (insert d l l_ge_d, auto simp: field_simps) also have "2 * ((1 - sqrt (1 - (d / l)\<^sup>2)) * l / 2 + arccos (d / l) * d / 2) = l * (1 - sqrt (1 - (d / l)\<^sup>2)) + arccos (d / l) * d" using d l by (simp add: field_simps) finally show ?thesis . qed lemma emeasure_buffon_set_long: "emeasure lborel (buffon_set l d) = 4 * ennreal (l * (1 - sqrt (1 - (d / l)\<^sup>2)) + arccos (d / l) * d)" by (simp add: emeasure_buffon_set_conv_buffon_set' emeasure_buffon_set'_long l_ge_d) theorem buffon_long: "emeasure (buffon l d) {True} = ennreal (2 / pi * ((l / d) - sqrt ((l / d)\<^sup>2 - 1) + arccos (d / l)))" proof - have *: "l * sqrt ((l\<^sup>2 - d\<^sup>2) / l\<^sup>2) + 0 \ l + d * arccos (d / l)" using d l_ge_d by (intro add_mono mult_nonneg_nonneg arccos_lbound) (auto simp: field_simps) have "emeasure (buffon l d) {True} = ennreal (4 * (l - l * sqrt (1 - (d / l)\<^sup>2) + arccos (d / l) * d)) / ennreal (2 * d * pi)" using d l l_ge_d * unfolding buffon_prob_aux emeasure_buffon_set_long ennreal_numeral [symmetric] by (subst ennreal_mult [symmetric]) (auto intro!: add_nonneg_nonneg mult_nonneg_nonneg simp: field_simps) also have "\ = ennreal ((4 * (l - l * sqrt (1 - (d / l)\<^sup>2) + arccos (d / l) * d)) / (2 * d * pi))" using d l * by (subst divide_ennreal) (auto simp: field_simps) also have "(4 * (l - l * sqrt (1 - (d / l)\<^sup>2) + arccos (d / l) * d)) / (2 * d * pi) = 2 / pi * (l / d - l / d * sqrt ((d / l)^2 * ((l / d)^2 - 1)) + arccos (d / l))" using d l by (simp add: field_simps) also have "l / d * sqrt ((d / l)^2 * ((l / d)^2 - 1)) = sqrt ((l / d) ^ 2 - 1)" using d l l_ge_d unfolding real_sqrt_mult real_sqrt_abs by simp finally show ?thesis . qed end end end diff --git a/thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy b/thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy --- a/thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy +++ b/thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy @@ -1,2048 +1,2041 @@ section \Auxiliary material\ theory Prime_Number_Theorem_Library imports Zeta_Function.Zeta_Function "HOL-Real_Asymp.Real_Asymp" begin (* TODO: Move *) lemma asymp_equivD_strong: assumes "f \[F] g" "eventually (\x. f x \ 0 \ g x \ 0) F" shows "((\x. f x / g x) \ 1) F" proof - from assms(1) have "((\x. if f x = 0 \ g x = 0 then 1 else f x / g x) \ 1) F" by (rule asymp_equivD) also have "?this \ ?thesis" by (intro filterlim_cong eventually_mono[OF assms(2)]) auto finally show ?thesis . qed -(* TODO: replace in library *)thm real_root_decreasing -lemma real_root_decreasing: "0 < n \ n \ N \ 1 \ x \ root N x \ root n x" - by (auto simp add: order_le_less real_root_strict_decreasing) - -lemma real_root_increasing: "0 < n \ n \ N \ 0 \ x \ x \ 1 \ root n x \ root N x" - by (auto simp add: order_le_less real_root_strict_increasing) - lemma frontier_real_Ici [simp]: fixes a :: real shows "frontier {a..} = {a}" unfolding frontier_def by (auto simp: interior_real_atLeast) lemma sum_upto_ln_conv_sum_upto_mangoldt: "sum_upto (\n. ln (real n)) x = sum_upto (\n. mangoldt n * nat \x / real n\) x" proof - have "sum_upto (\n. ln (real n)) x = sum_upto (\n. \d | d dvd n. mangoldt d) x" by (intro sum_upto_cong) (simp_all add: mangoldt_sum) also have "\ = sum_upto (\k. sum_upto (\d. mangoldt k) (x / real k)) x" by (rule sum_upto_sum_divisors) also have "\ = sum_upto (\n. mangoldt n * nat \x / real n\) x" unfolding sum_upto_altdef by (simp add: mult_ac) finally show ?thesis . qed lemma ln_fact_conv_sum_upto_mangoldt: "ln (fact n) = sum_upto (\k. mangoldt k * (n div k)) n" proof - have [simp]: "{0<..Suc n} = insert (Suc n) {0<..n}" for n by auto have "ln (fact n) = sum_upto (\n. ln (real n)) n" by (induction n) (auto simp: sum_upto_altdef nat_add_distrib ln_mult) also have "\ = sum_upto (\k. mangoldt k * (n div k)) n" unfolding sum_upto_ln_conv_sum_upto_mangoldt by (intro sum_upto_cong) (auto simp: floor_divide_of_nat_eq) finally show ?thesis . qed lemma powr_sum: "x \ 0 \ finite A \ x powr sum f A = (\y\A. x powr f y)" by (simp add: powr_def exp_sum sum_distrib_right) lemma fds_abs_converges_comparison_test: fixes s :: "'a :: dirichlet_series" assumes "eventually (\n. norm (fds_nth f n) \ fds_nth g n) at_top" and "fds_converges g (s \ 1)" shows "fds_abs_converges f s" unfolding fds_abs_converges_def proof (rule summable_comparison_test_ev) from assms(2) show "summable (\n. fds_nth g n / n powr (s \ 1))" by (auto simp: fds_converges_def) from assms(1) eventually_gt_at_top[of 0] show "eventually (\n. norm (norm (fds_nth f n / nat_power n s)) \ fds_nth g n / real n powr (s \ 1)) at_top" by eventually_elim (auto simp: norm_divide norm_nat_power intro!: divide_right_mono) qed lemma fds_converges_scaleR [intro]: assumes "fds_converges f s" shows "fds_converges (c *\<^sub>R f) s" proof - from assms have "summable (\n. c *\<^sub>R (fds_nth f n / nat_power n s))" by (intro summable_scaleR_right) (auto simp: fds_converges_def) also have "(\n. c *\<^sub>R (fds_nth f n / nat_power n s)) = (\n. (c *\<^sub>R fds_nth f n / nat_power n s))" by (simp add: scaleR_conv_of_real) finally show ?thesis by (simp add: fds_converges_def) qed lemma fds_abs_converges_scaleR [intro]: assumes "fds_abs_converges f s" shows "fds_abs_converges (c *\<^sub>R f) s" proof - from assms have "summable (\n. abs c * norm (fds_nth f n / nat_power n s))" by (intro summable_mult) (auto simp: fds_abs_converges_def) also have "(\n. abs c * norm (fds_nth f n / nat_power n s)) = (\n. norm ((c *\<^sub>R fds_nth f n) / nat_power n s))" by (simp add: norm_divide) finally show ?thesis by (simp add: fds_abs_converges_def) qed lemma conv_abscissa_scaleR: "conv_abscissa (scaleR c f) \ conv_abscissa f" by (rule conv_abscissa_mono) auto lemma abs_conv_abscissa_scaleR: "abs_conv_abscissa (scaleR c f) \ abs_conv_abscissa f" by (rule abs_conv_abscissa_mono) auto lemma fds_converges_mult_const_left [intro]: "fds_converges f s \ fds_converges (fds_const c * f) s" by (auto simp: fds_converges_def dest: summable_mult[of _ c]) lemma fds_abs_converges_mult_const_left [intro]: "fds_abs_converges f s \ fds_abs_converges (fds_const c * f) s" by (auto simp: fds_abs_converges_def norm_mult norm_divide dest: summable_mult[of _ "norm c"]) lemma conv_abscissa_mult_const_left: "conv_abscissa (fds_const c * f) \ conv_abscissa f" by (intro conv_abscissa_mono) auto lemma abs_conv_abscissa_mult_const_left: "abs_conv_abscissa (fds_const c * f) \ abs_conv_abscissa f" by (intro abs_conv_abscissa_mono) auto lemma fds_converges_mult_const_right [intro]: "fds_converges f s \ fds_converges (f * fds_const c) s" by (auto simp: fds_converges_def dest: summable_mult2[of _ c]) lemma fds_abs_converges_mult_const_right [intro]: "fds_abs_converges f s \ fds_abs_converges (f * fds_const c) s" by (auto simp: fds_abs_converges_def norm_mult norm_divide dest: summable_mult2[of _ "norm c"]) lemma conv_abscissa_mult_const_right: "conv_abscissa (f * fds_const c) \ conv_abscissa f" by (intro conv_abscissa_mono) auto lemma abs_conv_abscissa_mult_const_right: "abs_conv_abscissa (f * fds_const c) \ abs_conv_abscissa f" by (intro abs_conv_abscissa_mono) auto lemma bounded_coeffs_imp_fds_abs_converges: fixes s :: "'a :: dirichlet_series" and f :: "'a fds" assumes "Bseq (fds_nth f)" "s \ 1 > 1" shows "fds_abs_converges f s" proof - from assms obtain C where C: "\n. norm (fds_nth f n) \ C" by (auto simp: Bseq_def) show ?thesis proof (rule fds_abs_converges_comparison_test) from \s \ 1 > 1\ show "fds_converges (C *\<^sub>R fds_zeta) (s \ 1)" by (intro fds_abs_converges_imp_converges) auto from C show "eventually (\n. norm (fds_nth f n) \ fds_nth (C *\<^sub>R fds_zeta) n) at_top" by (intro always_eventually) (auto simp: fds_nth_zeta) qed qed lemma bounded_coeffs_imp_fds_abs_converges': fixes s :: "'a :: dirichlet_series" and f :: "'a fds" assumes "Bseq (\n. fds_nth f n * nat_power n s0)" "s \ 1 > 1 - s0 \ 1" shows "fds_abs_converges f s" proof - have "fds_nth (fds_shift s0 f) = (\n. fds_nth f n * nat_power n s0)" by (auto simp: fun_eq_iff) with assms have "Bseq (fds_nth (fds_shift s0 f))" by simp with assms(2) have "fds_abs_converges (fds_shift s0 f) (s + s0)" by (intro bounded_coeffs_imp_fds_abs_converges) (auto simp: algebra_simps) thus ?thesis by simp qed lemma bounded_coeffs_imp_abs_conv_abscissa_le: fixes s :: "'a :: dirichlet_series" and f :: "'a fds" and c :: ereal assumes "Bseq (\n. fds_nth f n * nat_power n s)" "1 - s \ 1 \ c" shows "abs_conv_abscissa f \ c" proof (rule abs_conv_abscissa_leI_weak) fix x assume "c < ereal x" have "ereal (1 - s \ 1) \ c" by fact also have "\ < ereal x" by fact finally have "1 - s \ 1 < ereal x" by simp thus "fds_abs_converges f (of_real x)" by (intro bounded_coeffs_imp_fds_abs_converges'[OF assms(1)]) auto qed lemma bounded_coeffs_imp_abs_conv_abscissa_le_1: fixes s :: "'a :: dirichlet_series" and f :: "'a fds" assumes "Bseq (\n. fds_nth f n)" shows "abs_conv_abscissa f \ 1" proof - have [simp]: "fds_nth f n * nat_power n 0 = fds_nth f n" for n by (cases "n = 0") auto show ?thesis by (rule bounded_coeffs_imp_abs_conv_abscissa_le[where s = 0]) (insert assms, auto simp:) qed (* TODO: replace library version *) (* EXAMPLE: This might make a good example to illustrate real_asymp *) lemma fixes a b c :: real assumes ab: "a + b > 0" and c: "c < -1" shows set_integrable_powr_at_top: "(\x. (b + x) powr c) absolutely_integrable_on {a<..}" and set_lebesgue_integral_powr_at_top: "(\x\{a<..}. ((b + x) powr c) \lborel) = -((b + a) powr (c + 1) / (c + 1))" and powr_has_integral_at_top: "((\x. (b + x) powr c) has_integral -((b + a) powr (c + 1) / (c + 1))) {a<..}" proof - let ?f = "\x. (b + x) powr c" and ?F = "\x. (b + x) powr (c + 1) / (c + 1)" have limits: "((?F \ real_of_ereal) \ ?F a) (at_right (ereal a))" "((?F \ real_of_ereal) \ 0) (at_left \)" using c ab unfolding ereal_tendsto_simps1 by (real_asymp simp: field_simps)+ have 1: "set_integrable lborel (einterval a \) ?f" using ab c limits by (intro interval_integral_FTC_nonneg) (auto intro!: derivative_eq_intros) thus 2: "?f absolutely_integrable_on {a<..}" by (auto simp: set_integrable_def integrable_completion) have "LBINT x=ereal a..\. (b + x) powr c = 0 - ?F a" using ab c limits by (intro interval_integral_FTC_nonneg) (auto intro!: derivative_eq_intros) thus 3: "(\x\{a<..}. ((b + x) powr c) \lborel) = -((b + a) powr (c + 1) / (c + 1))" by (simp add: interval_integral_to_infinity_eq) show "(?f has_integral -((b + a) powr (c + 1) / (c + 1))) {a<..}" using set_borel_integral_eq_integral[OF 1] 3 by (simp add: has_integral_iff) qed lemma fds_converges_altdef2: "fds_converges f s \ convergent (\N. eval_fds (fds_truncate N f) s)" unfolding fds_converges_def summable_iff_convergent' eval_fds_truncate by (auto simp: not_le intro!: convergent_cong always_eventually sum.mono_neutral_right) lemma tendsto_eval_fds_truncate: assumes "fds_converges f s" shows "(\N. eval_fds (fds_truncate N f) s) \ eval_fds f s" proof - have "(\N. eval_fds (fds_truncate N f) s) \ eval_fds f s \ (\N. \i\N. fds_nth f i / nat_power i s) \ eval_fds f s" unfolding eval_fds_truncate by (intro filterlim_cong always_eventually allI sum.mono_neutral_left) (auto simp: not_le) also have \ using assms by (simp add: fds_converges_iff sums_def' atLeast0AtMost) finally show ?thesis . qed lemma linepath_translate_left: "linepath (c + a) (c + a) = (\x. c + a) \ linepath a b" by (auto simp: fun_eq_iff linepath_def algebra_simps) lemma linepath_translate_right: "linepath (a + c) (b + c) = (\x. x + c) \ linepath a b" by (auto simp: fun_eq_iff linepath_def algebra_simps) lemma integrable_on_affinity: assumes "m \ 0" "f integrable_on (cbox a b)" shows "(\x. f (m *\<^sub>R x + c)) integrable_on ((\x. (1 / m) *\<^sub>R x - ((1 / m) *\<^sub>R c)) ` cbox a b)" proof - from assms obtain I where "(f has_integral I) (cbox a b)" by (auto simp: integrable_on_def) from has_integral_affinity[OF this assms(1), of c] show ?thesis by (auto simp: integrable_on_def) qed lemma has_integral_cmul_iff: assumes "c \ 0" shows "((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R I)) A \ (f has_integral I) A" using assms has_integral_cmul[of f I A c] has_integral_cmul[of "\x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"] by (auto simp: field_simps) lemma has_integral_affinity': fixes a :: "'a::euclidean_space" assumes "(f has_integral i) (cbox a b)" and "m > 0" shows "((\x. f(m *\<^sub>R x + c)) has_integral (i /\<^sub>R m ^ DIM('a))) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))" proof (cases "cbox a b = {}") case True hence "(cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) = {}" using \m > 0\ unfolding box_eq_empty by (auto simp: algebra_simps) with True and assms show ?thesis by simp next case False have "((\x. f (m *\<^sub>R x + c)) has_integral (1 / \m\ ^ DIM('a)) *\<^sub>R i) ((\x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)" using assms by (intro has_integral_affinity) auto also have "((\x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b) = ((\x. - ((1 / m) *\<^sub>R c) + x) ` (\x. (1 / m) *\<^sub>R x) ` cbox a b)" by (simp add: image_image algebra_simps) also have "(\x. (1 / m) *\<^sub>R x) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)" using \m > 0\ False by (subst image_smult_cbox) simp_all also have "(\x. - ((1 / m) *\<^sub>R c) + x) ` \ = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)" by (subst cbox_translation [symmetric]) (simp add: field_simps vector_add_divide_simps) finally show ?thesis using \m > 0\ by (simp add: field_simps) qed lemma has_integral_affinity_iff: fixes f :: "'a :: euclidean_space \ 'b :: real_normed_vector" assumes "m > 0" shows "((\x. f (m *\<^sub>R x + c)) has_integral (I /\<^sub>R m ^ DIM('a))) (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \ (f has_integral I) (cbox a b)" (is "?lhs = ?rhs") proof assume ?lhs from has_integral_affinity'[OF this, of "1 / m" "-c /\<^sub>R m"] and \m > 0\ show ?rhs by (simp add: field_simps vector_add_divide_simps) next assume ?rhs from has_integral_affinity'[OF this, of m c] and \m > 0\ show ?lhs by simp qed lemma has_contour_integral_linepath_Reals_iff: fixes a b :: complex and f :: "complex \ complex" assumes "a \ Reals" "b \ Reals" "Re a < Re b" shows "(f has_contour_integral I) (linepath a b) \ ((\x. f (of_real x)) has_integral I) {Re a..Re b}" proof - from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b" by (simp_all add: complex_eq_iff) from assms have "a \ b" by auto have "((\x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \ ((\x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}" by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric]) (insert assms, simp_all add: field_simps scaleR_conv_of_real) also have "(\x. f (a + b * of_real x - a * of_real x)) = (\x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))" using \a \ b\ by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real) - also have "(\ has_integral I /\<^sub>R (Re b - Re a)) {0..1} \ + also have "(\ has_integral I /\<^sub>R (Re b - Re a)) {0..1} \ ((\x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps) also have "\ \ (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def by (intro has_integral_cong) (simp add: vector_derivative_linepath_within) finally show ?thesis by simp qed lemma contour_integrable_linepath_Reals_iff: fixes a b :: complex and f :: "complex \ complex" assumes "a \ Reals" "b \ Reals" "Re a < Re b" shows "(f contour_integrable_on linepath a b) \ (\x. f (of_real x)) integrable_on {Re a..Re b}" using has_contour_integral_linepath_Reals_iff[OF assms, of f] by (auto simp: contour_integrable_on_def integrable_on_def) lemma contour_integral_linepath_Reals_eq: fixes a b :: complex and f :: "complex \ complex" assumes "a \ Reals" "b \ Reals" "Re a < Re b" shows "contour_integral (linepath a b) f = integral {Re a..Re b} (\x. f (of_real x))" proof (cases "f contour_integrable_on linepath a b") case True thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f] using has_contour_integral_integral has_contour_integral_unique by blast next case False thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f] by (simp add: not_integrable_contour_integral not_integrable_integral) qed lemma has_contour_integral_linepath_same_Im_iff: fixes a b :: complex and f :: "complex \ complex" assumes "Im a = Im b" "Re a < Re b" shows "(f has_contour_integral I) (linepath a b) \ ((\x. f (of_real x + Im a * \)) has_integral I) {Re a..Re b}" proof - have deriv: "vector_derivative ((\x. x - Im a * \) \ linepath a b) (at y) = b - a" for y using linepath_translate_right[of a "-Im a * \" b, symmetric] by simp have "(f has_contour_integral I) (linepath a b) \ ((\x. f (x + Im a * \)) has_contour_integral I) (linepath (a - Im a * \) (b - Im a * \))" using linepath_translate_right[of a "-Im a * \" b] deriv by (simp add: has_contour_integral) also have "\ \ ((\x. f (x + Im a * \)) has_integral I) {Re a..Re b}" using assms by (subst has_contour_integral_linepath_Reals_iff) (auto simp: complex_is_Real_iff) finally show ?thesis . qed lemma contour_integrable_linepath_same_Im_iff: fixes a b :: complex and f :: "complex \ complex" assumes "Im a = Im b" "Re a < Re b" shows "(f contour_integrable_on linepath a b) \ (\x. f (of_real x + Im a * \)) integrable_on {Re a..Re b}" using has_contour_integral_linepath_same_Im_iff[OF assms, of f] by (auto simp: contour_integrable_on_def integrable_on_def) lemma contour_integral_linepath_same_Im: fixes a b :: complex and f :: "complex \ complex" assumes "Im a = Im b" "Re a < Re b" shows "contour_integral (linepath a b) f = integral {Re a..Re b} (\x. f (x + Im a * \))" proof (cases "f contour_integrable_on linepath a b") case True thus ?thesis using has_contour_integral_linepath_same_Im_iff[OF assms, of f] using has_contour_integral_integral has_contour_integral_unique by blast next case False thus ?thesis using contour_integrable_linepath_same_Im_iff[OF assms, of f] by (simp add: not_integrable_contour_integral not_integrable_integral) qed lemmas [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1 lemma continuous_on_compact_bound: assumes "compact A" "continuous_on A f" obtains B where "B \ 0" "\x. x \ A \ norm (f x) \ B" proof - from assms(2,1) have "compact (f ` A)" by (rule compact_continuous_image) then obtain B where "\x\A. norm (f x) \ B" by (auto dest!: compact_imp_bounded simp: bounded_iff) hence "max B 0 \ 0" and "\x\A. norm (f x) \ max B 0" by auto thus ?thesis using that by blast qed interpretation cis: periodic_fun_simple cis "2 * pi" by standard (simp_all add: complex_eq_iff) lemma open_contains_cbox: fixes x :: "'a :: euclidean_space" assumes "open A" "x \ A" obtains a b where "cbox a b \ A" "x \ box a b" "\i\Basis. a \ i < b \ i" proof - from assms obtain R where R: "R > 0" "ball x R \ A" by (auto simp: open_contains_ball) define r :: real where "r = R / (2 * sqrt DIM('a))" from \R > 0\ have [simp]: "r > 0" by (auto simp: r_def) define d :: 'a where "d = r *\<^sub>R Topology_Euclidean_Space.One" have "cbox (x - d) (x + d) \ A" proof safe fix y assume y: "y \ cbox (x - d) (x + d)" have "dist x y = sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2)" by (subst euclidean_dist_l2) (auto simp: L2_set_def) also from y have "sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2) \ sqrt (\i\(Basis::'a set). r\<^sup>2)" by (intro real_sqrt_le_mono sum_mono power_mono) (auto simp: dist_norm d_def cbox_def algebra_simps) also have "\ = sqrt (DIM('a) * r\<^sup>2)" by simp also have "DIM('a) * r\<^sup>2 = (R / 2) ^ 2" by (simp add: r_def power_divide) also have "sqrt \ = R / 2" using \R > 0\ by simp also from \R > 0\ have "\ < R" by simp finally have "y \ ball x R" by simp with R show "y \ A" by blast qed thus ?thesis using that[of "x - d" "x + d"] by (auto simp: algebra_simps d_def box_def) qed lemma open_contains_box: fixes x :: "'a :: euclidean_space" assumes "open A" "x \ A" obtains a b where "box a b \ A" "x \ box a b" "\i\Basis. a \ i < b \ i" proof - from open_contains_cbox[OF assms] guess a b . with that[of a b] box_subset_cbox[of a b] show ?thesis by auto qed lemma analytic_onE_box: assumes "f analytic_on A" "s \ A" obtains a b where "Re a < Re b" "Im a < Im b" "s \ box a b" "f analytic_on box a b" proof - from assms obtain r where r: "r > 0" "f holomorphic_on ball s r" by (auto simp: analytic_on_def) with open_contains_box[of "ball s r" s] obtain a b where "box a b \ ball s r" "s \ box a b" "\i\Basis. a \ i < b \ i" by auto moreover from r have "f analytic_on ball s r" by (simp add: analytic_on_open) ultimately show ?thesis using that[of a b] analytic_on_subset[of _ "ball s r" "box a b"] by (auto simp: Basis_complex_def) qed lemma inner_image_box: assumes "(i :: 'a :: euclidean_space) \ Basis" assumes "\i\Basis. a \ i < b \ i" shows "(\x. x \ i) ` box a b = {a \ i<.. i}" proof safe fix x assume x: "x \ {a \ i<.. i}" let ?y = "(\j\Basis. (if i = j then x else (a + b) \ j / 2) *\<^sub>R j)" from x assms have "?y \ i \ (\x. x \ i) ` box a b" by (intro imageI) (auto simp: box_def algebra_simps) also have "?y \ i = (\j\Basis. (if i = j then x else (a + b) \ j / 2) * (j \ i))" by (simp add: inner_sum_left) also have "\ = (\j\Basis. if i = j then x else 0)" by (intro sum.cong) (auto simp: inner_not_same_Basis assms) also have "\ = x" using assms by simp finally show "x \ (\x. x \ i) ` box a b" . qed (insert assms, auto simp: box_def) lemma Re_image_box: assumes "Re a < Re b" "Im a < Im b" shows "Re ` box a b = {Re a<..::complex" a b] assms by (auto simp: Basis_complex_def) lemma inner_image_cbox: assumes "(i :: 'a :: euclidean_space) \ Basis" assumes "\i\Basis. a \ i \ b \ i" shows "(\x. x \ i) ` cbox a b = {a \ i..b \ i}" proof safe fix x assume x: "x \ {a \ i..b \ i}" let ?y = "(\j\Basis. (if i = j then x else a \ j) *\<^sub>R j)" from x assms have "?y \ i \ (\x. x \ i) ` cbox a b" by (intro imageI) (auto simp: cbox_def) also have "?y \ i = (\j\Basis. (if i = j then x else a \ j) * (j \ i))" by (simp add: inner_sum_left) also have "\ = (\j\Basis. if i = j then x else 0)" by (intro sum.cong) (auto simp: inner_not_same_Basis assms) also have "\ = x" using assms by simp finally show "x \ (\x. x \ i) ` cbox a b" . qed (insert assms, auto simp: cbox_def) lemma Re_image_cbox: assumes "Re a \ Re b" "Im a \ Im b" shows "Re ` cbox a b = {Re a..Re b}" using inner_image_cbox[of "1::complex" a b] assms by (auto simp: Basis_complex_def) lemma Im_image_cbox: assumes "Re a \ Re b" "Im a \ Im b" shows "Im ` cbox a b = {Im a..Im b}" using inner_image_cbox[of "\::complex" a b] assms by (auto simp: Basis_complex_def) lemma analytic_onE_cball: assumes "f analytic_on A" "s \ A" "ub > (0::real)" obtains R where "R > 0" "R < ub" "f analytic_on cball s R" proof - from assms obtain r where "r > 0" "f holomorphic_on ball s r" by (auto simp: analytic_on_def) hence "f analytic_on ball s r" by (simp add: analytic_on_open) hence "f analytic_on cball s (min (ub / 2) (r / 2))" by (rule analytic_on_subset, subst cball_subset_ball_iff) (use \r > 0\ in auto) moreover have "min (ub / 2) (r / 2) > 0" and "min (ub / 2) (r / 2) < ub" using \r > 0\ and \ub > 0\ by (auto simp: min_def) ultimately show ?thesis using that[of "min (ub / 2) (r / 2)"] by blast qed corollary analytic_pre_zeta' [analytic_intros]: assumes "f analytic_on A" "a > 0" shows "(\x. pre_zeta a (f x)) analytic_on A" using analytic_on_compose_gen[OF assms(1) analytic_pre_zeta[of a UNIV]] assms(2) by (auto simp: o_def) corollary analytic_hurwitz_zeta' [analytic_intros]: assumes "f analytic_on A" "(\x. x \ A \ f x \ 1)" "a > 0" shows "(\x. hurwitz_zeta a (f x)) analytic_on A" using analytic_on_compose_gen[OF assms(1) analytic_hurwitz_zeta[of a "-{1}"]] assms(2,3) by (auto simp: o_def) corollary analytic_zeta' [analytic_intros]: assumes "f analytic_on A" "(\x. x \ A \ f x \ 1)" shows "(\x. zeta (f x)) analytic_on A" using analytic_on_compose_gen[OF assms(1) analytic_zeta[of "-{1}"]] assms(2) by (auto simp: o_def) lemma logderiv_zeta_analytic: "(\s. deriv zeta s / zeta s) analytic_on {s. Re s \ 1} - {1}" using zeta_Re_ge_1_nonzero by (auto intro!: analytic_intros) lemma cis_pi_half [simp]: "cis (pi / 2) = \" by (simp add: complex_eq_iff) lemma mult_real_sqrt: "x \ 0 \ x * sqrt y = sqrt (x ^ 2 * y)" by (simp add: real_sqrt_mult) lemma arcsin_pos: "x \ {0<..1} \ arcsin x > 0" using arcsin_less_arcsin[of 0 x] by simp lemmas analytic_imp_holomorphic' = holomorphic_on_subset[OF analytic_imp_holomorphic] lemma residue_simple': assumes "open s" "0 \ s" "f holomorphic_on s" shows "residue (\w. f w / w) 0 = f 0" using residue_simple[of s 0 f] assms by simp lemma fds_converges_cong: assumes "eventually (\n. fds_nth f n = fds_nth g n) at_top" "s = s'" shows "fds_converges f s \ fds_converges g s'" unfolding fds_converges_def by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms) lemma fds_abs_converges_cong: assumes "eventually (\n. fds_nth f n = fds_nth g n) at_top" "s = s'" shows "fds_abs_converges f s \ fds_abs_converges g s'" unfolding fds_abs_converges_def by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms) lemma conv_abscissa_cong: assumes "eventually (\n. fds_nth f n = fds_nth g n) at_top" shows "conv_abscissa f = conv_abscissa g" proof - have "fds_converges f = fds_converges g" by (intro ext fds_converges_cong assms refl) thus ?thesis by (simp add: conv_abscissa_def) qed lemma abs_conv_abscissa_cong: assumes "eventually (\n. fds_nth f n = fds_nth g n) at_top" shows "abs_conv_abscissa f = abs_conv_abscissa g" proof - have "fds_abs_converges f = fds_abs_converges g" by (intro ext fds_abs_converges_cong assms refl) thus ?thesis by (simp add: abs_conv_abscissa_def) qed definition fds_remainder where "fds_remainder m = fds_subseries (\n. n > m)" lemma fds_nth_remainder: "fds_nth (fds_remainder m f) = (\n. if n > m then fds_nth f n else 0)" by (simp add: fds_remainder_def fds_subseries_def fds_nth_fds') lemma fds_converges_remainder_iff [simp]: "fds_converges (fds_remainder m f) s \ fds_converges f s" by (intro fds_converges_cong eventually_mono[OF eventually_gt_at_top[of m]]) (auto simp: fds_nth_remainder) lemma fds_abs_converges_remainder_iff [simp]: "fds_abs_converges (fds_remainder m f) s \ fds_abs_converges f s" by (intro fds_abs_converges_cong eventually_mono[OF eventually_gt_at_top[of m]]) (auto simp: fds_nth_remainder) lemma fds_converges_remainder [intro]: "fds_converges f s \ fds_converges (fds_remainder m f) s" and fds_abs_converges_remainder [intro]: "fds_abs_converges f s \ fds_abs_converges (fds_remainder m f) s" by simp_all lemma conv_abscissa_remainder [simp]: "conv_abscissa (fds_remainder m f) = conv_abscissa f" by (intro conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]]) (auto simp: fds_nth_remainder) lemma abs_conv_abscissa_remainder [simp]: "abs_conv_abscissa (fds_remainder m f) = abs_conv_abscissa f" by (intro abs_conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]]) (auto simp: fds_nth_remainder) lemma eval_fds_remainder: "eval_fds (fds_remainder m f) s = (\n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)" (is "_ = suminf (\n. ?f (n + Suc m))") proof (cases "fds_converges f s") case False hence "\fds_converges (fds_remainder m f) s" by simp hence "(\x. (\n. fds_nth (fds_remainder m f) n / nat_power n s) sums x) = (\_. False)" by (auto simp: fds_converges_def summable_def) hence "eval_fds (fds_remainder m f) s = (THE _. False)" by (simp add: eval_fds_def suminf_def) moreover from False have "\summable (\n. ?f (n + Suc m))" unfolding fds_converges_def by (subst summable_iff_shift) auto hence "(\x. (\n. ?f (n + Suc m)) sums x) = (\_. False)" by (auto simp: summable_def) hence "suminf (\n. ?f (n + Suc m)) = (THE _. False)" by (simp add: suminf_def) ultimately show ?thesis by simp next case True hence *: "fds_converges (fds_remainder m f) s" by simp have "eval_fds (fds_remainder m f) s = (\n. fds_nth (fds_remainder m f) n / nat_power n s)" unfolding eval_fds_def .. also have "\ = (\n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)" using * unfolding fds_converges_def by (subst suminf_minus_initial_segment) (auto simp: fds_nth_remainder) also have "(\n. fds_nth (fds_remainder m f) (n + Suc m)) = (\n. fds_nth f (n + Suc m))" by (intro ext) (auto simp: fds_nth_remainder) finally show ?thesis . qed lemma fds_truncate_plus_remainder: "fds_truncate m f + fds_remainder m f = f" by (intro fds_eqI) (auto simp: fds_truncate_def fds_remainder_def fds_subseries_def) lemma holomorphic_fds_eval' [holomorphic_intros]: assumes "g holomorphic_on A" "\x. x \ A \ Re (g x) > conv_abscissa f" shows "(\x. eval_fds f (g x)) holomorphic_on A" using holomorphic_on_compose_gen[OF assms(1) holomorphic_fds_eval[OF order.refl, of f]] assms(2) by (auto simp: o_def) lemma analytic_fds_eval' [analytic_intros]: assumes "g analytic_on A" "\x. x \ A \ Re (g x) > conv_abscissa f" shows "(\x. eval_fds f (g x)) analytic_on A" using analytic_on_compose_gen[OF assms(1) analytic_fds_eval[OF order.refl, of f]] assms(2) by (auto simp: o_def) lemma homotopic_loopsI: fixes h :: "real \ real \ _" assumes "continuous_on ({0..1} \ {0..1}) h" "h ` ({0..1} \ {0..1}) \ s" "\x. x \ {0..1} \ h (0, x) = p x" "\x. x \ {0..1} \ h (1, x) = q x" "\x. x \ {0..1} \ pathfinish (h \ Pair x) = pathstart (h \ Pair x)" shows "homotopic_loops s p q" using assms unfolding homotopic_loops by (intro exI[of _ h]) auto lemma continuous_on_linepath [continuous_intros]: assumes "continuous_on A a" "continuous_on A b" "continuous_on A f" shows "continuous_on A (\x. linepath (a x) (b x) (f x))" using assms by (auto simp: linepath_def intro!: continuous_intros assms) lemma continuous_on_part_circlepath [continuous_intros]: assumes "continuous_on A c" "continuous_on A r" "continuous_on A a" "continuous_on A b" "continuous_on A f" shows "continuous_on A (\x. part_circlepath (c x) (r x) (a x) (b x) (f x))" using assms by (auto simp: part_circlepath_def intro!: continuous_intros assms) lemma homotopic_loops_part_circlepath: assumes "sphere c r \ A" and "r \ 0" and "b1 = a1 + 2 * of_int k * pi" and "b2 = a2 + 2 * of_int k * pi" shows "homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)" proof - define h where "h = (\(x,y). part_circlepath c r (linepath a1 a2 x) (linepath b1 b2 x) y)" show ?thesis proof (rule homotopic_loopsI) show "continuous_on ({0..1} \ {0..1}) h" by (auto simp: h_def case_prod_unfold intro!: continuous_intros) next from assms have "h ` ({0..1} \ {0..1}) \ sphere c r" by (auto simp: h_def part_circlepath_def dist_norm norm_mult) also have "\ \ A" by fact finally show "h ` ({0..1} \ {0..1}) \ A" . next fix x :: real assume x: "x \ {0..1}" show "h (0, x) = part_circlepath c r a1 b1 x" and "h (1, x) = part_circlepath c r a2 b2 x" by (simp_all add: h_def linepath_def) have "cis (pi * (real_of_int k * 2)) = 1" using cis.plus_of_int[of 0 k] by (simp add: algebra_simps) thus "pathfinish (h \ Pair x) = pathstart (h \ Pair x)" by (simp add: h_def o_def exp_eq_polar linepath_def algebra_simps cis_mult [symmetric] cis_divide [symmetric] assms) qed qed lemma homotopic_pathsI: fixes h :: "real \ real \ _" assumes "continuous_on ({0..1} \ {0..1}) h" assumes "h ` ({0..1} \ {0..1}) \ s" assumes "\x. x \ {0..1} \ h (0, x) = p x" assumes "\x. x \ {0..1} \ h (1, x) = q x" assumes "\x. x \ {0..1} \ pathstart (h \ Pair x) = pathstart p" assumes "\x. x \ {0..1} \ pathfinish (h \ Pair x) = pathfinish p" shows "homotopic_paths s p q" using assms unfolding homotopic_paths by (intro exI[of _ h]) auto lemma part_circlepath_conv_subpath: "part_circlepath c r a b = subpath (a / (2*pi)) (b / (2*pi)) (circlepath c r)" by (simp add: part_circlepath_def circlepath_def subpath_def linepath_def algebra_simps exp_eq_polar) lemma homotopic_paths_part_circlepath: assumes "a \ b" "b \ c" assumes "path_image (part_circlepath C r a c) \ A" "r \ 0" shows "homotopic_paths A (part_circlepath C r a c) (part_circlepath C r a b +++ part_circlepath C r b c)" (is "homotopic_paths _ ?g (?h1 +++ ?h2)") proof (cases "a = c") case False with assms have "a < c" by simp define slope where "slope = (b - a) / (c - a)" from assms and \a < c\ have slope: "slope \ {0..1}" by (auto simp: field_simps slope_def) define f :: "real \ real" where "f = linepath 0 slope +++ linepath slope 1" show ?thesis proof (rule homotopic_paths_reparametrize) fix t :: real assume t: "t \ {0..1}" show "(?h1 +++ ?h2) t = ?g (f t)" proof (cases "t \ 1 / 2") case True hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)" by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def) also from True \a < c\ have "(1 - f t) * a + f t * c = (1 - 2 * t) * a + 2 * t * b" unfolding f_def slope_def linepath_def joinpaths_def by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1) (simp add: algebra_simps)? also from True have "C + r * cis \ = (?h1 +++ ?h2) t" by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def) finally show ?thesis .. next case False hence "?g (f t) = C + r * cis ((1 - f t) * a + f t * c)" by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def) also from False \a < c\ have "(1 - f t) * a + f t * c = (2 - 2 * t) * b + (2 * t - 1) * c" unfolding f_def slope_def linepath_def joinpaths_def by (simp add: divide_simps del: div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1) (simp add: algebra_simps)? also from False have "C + r * cis \ = (?h1 +++ ?h2) t" by (simp add: joinpaths_def part_circlepath_def exp_eq_polar linepath_def) finally show ?thesis .. qed next from slope have "path_image f \ {0..1}" by (auto simp: f_def path_image_join closed_segment_eq_real_ivl) thus "f ` {0..1} \ {0..1}" by (simp add: path_image_def) next have "path f" unfolding f_def by auto thus "continuous_on {0..1} f" by (simp add: path_def) qed (insert assms, auto simp: f_def joinpaths_def linepath_def) next case [simp]: True with assms have [simp]: "b = c" by auto have "part_circlepath C r c c +++ part_circlepath C r c c = part_circlepath C r c c" by (simp add: fun_eq_iff joinpaths_def part_circlepath_def) thus ?thesis using assms by simp qed lemma has_contour_integral_mirror_iff: assumes "valid_path g" shows "(f has_contour_integral I) (-g) \ ((\x. -f (- x)) has_contour_integral I) g" proof - from assms have "g piecewise_differentiable_on {0..1}" by (auto simp: valid_path_def piecewise_C1_imp_differentiable) then obtain S where S: "finite S" "\x. x \ {0..1} - S \ g differentiable at x within {0..1}" unfolding piecewise_differentiable_on_def by blast have S': "g differentiable at x" if "x \ {0..1} - ({0, 1} \ S)" for x proof - from that have "x \ interior {0..1}" by auto with S(2)[of x] that show ?thesis by (auto simp: at_within_interior[of _ "{0..1}"]) qed have "(f has_contour_integral I) (-g) \ ((\x. f (- g x) * vector_derivative (-g) (at x)) has_integral I) {0..1}" by (simp add: has_contour_integral) also have "\ \ ((\x. -f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}" by (intro has_integral_spike_finite_eq[of "S \ {0, 1}"]) (insert \finite S\ S', auto simp: o_def fun_Compl_def) also have "\ \ ((\x. -f (-x)) has_contour_integral I) g" by (simp add: has_contour_integral) finally show ?thesis . qed lemma contour_integral_on_mirror_iff: assumes "valid_path g" shows "f contour_integrable_on (-g) \ (\x. -f (- x)) contour_integrable_on g" by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff assms) lemma contour_integral_mirror: assumes "valid_path g" shows "contour_integral (-g) f = contour_integral g (\x. -f (- x))" proof (cases "f contour_integrable_on (-g)") case True then obtain I where I: "(f has_contour_integral I) (-g)" by (auto simp: contour_integrable_on_def) also note has_contour_integral_mirror_iff[OF assms] finally have "((\x. - f (- x)) has_contour_integral I) g" . with I show ?thesis using contour_integral_unique by blast next case False hence "\(\x. -f (-x)) contour_integrable_on g" by (auto simp: contour_integral_on_mirror_iff assms) from False and this show ?thesis by (simp add: not_integrable_contour_integral) qed lemma contour_integrable_neg_iff: "(\x. -f x) contour_integrable_on g \ f contour_integrable_on g" using contour_integrable_neg[of f g] contour_integrable_neg[of "\x. -f x" g] by auto lemma contour_integral_neg: shows "contour_integral g (\x. -f x) = -contour_integral g f" proof (cases "f contour_integrable_on g") case True thus ?thesis by (simp add: contour_integral_neg) next case False hence "\(\x. -f x) contour_integrable_on g" by (simp add: contour_integrable_neg_iff) with False show ?thesis by (simp add: not_integrable_contour_integral) qed lemma minus_cis: "-cis x = cis (x + pi)" by (simp add: complex_eq_iff) lemma path_image_part_circlepath_subset: assumes "a \ a'" "a' \ b'" "b' \ b" shows "path_image (part_circlepath c r a' b') \ path_image (part_circlepath c r a b)" using assms by (subst (1 2) path_image_part_circlepath) auto lemma part_circlepath_mirror: assumes "a' = a + pi + 2 * pi * of_int k" "b' = b + pi + 2 * pi * of_int k" "c' = -c" shows "-part_circlepath c r a b = part_circlepath c' r a' b'" proof fix x :: real have "part_circlepath c' r a' b' x = c' + r * cis (linepath a b x + pi + k * (2 * pi))" by (simp add: part_circlepath_def exp_eq_polar assms linepath_translate_right mult_ac) also have "cis (linepath a b x + pi + k * (2 * pi)) = cis (linepath a b x + pi)" by (rule cis.plus_of_int) also have "\ = -cis (linepath a b x)" by (simp add: minus_cis) also have "c' + r * \ = -part_circlepath c r a b x" by (simp add: part_circlepath_def assms exp_eq_polar) finally show "(- part_circlepath c r a b) x = part_circlepath c' r a' b' x" by simp qed - + lemma path_mirror [intro]: "path (g :: _ \ 'b::topological_group_add) \ path (-g)" by (auto simp: path_def intro!: continuous_intros) lemma path_mirror_iff [simp]: "path (-g :: _ \ 'b::topological_group_add) \ path g" using path_mirror[of g] path_mirror[of "-g"] by (auto simp: fun_Compl_def) lemma valid_path_mirror [intro]: "valid_path g \ valid_path (-g)" by (auto simp: valid_path_def fun_Compl_def piecewise_C1_differentiable_neg) lemma valid_path_mirror_iff [simp]: "valid_path (-g) \ valid_path g" using valid_path_mirror[of g] valid_path_mirror[of "-g"] by (auto simp: fun_Compl_def) lemma pathstart_mirror [simp]: "pathstart (-g) = -pathstart g" and pathfinish_mirror [simp]: "pathfinish (-g) = -pathfinish g" by (simp_all add: pathstart_def pathfinish_def) lemma path_image_mirror: "path_image (-g) = uminus ` path_image g" by (auto simp: path_image_def) lemma contour_integral_bound_part_circlepath: assumes "f contour_integrable_on part_circlepath c r a b" assumes "B \ 0" "r \ 0" "\x. x \ path_image (part_circlepath c r a b) \ norm (f x) \ B" shows "norm (contour_integral (part_circlepath c r a b) f) \ B * r * \b - a\" proof - let ?I = "integral {0..1} (\x. f (part_circlepath c r a b x) * \ * of_real (r * (b - a)) * exp (\ * linepath a b x))" have "norm ?I \ integral {0..1} (\x::real. B * 1 * (r * \b - a\) * 1)" proof (rule integral_norm_bound_integral, goal_cases) case 1 with assms(1) show ?case by (simp add: contour_integrable_on vector_derivative_part_circlepath mult_ac) next case (3 x) with assms(2-) show ?case unfolding norm_mult norm_of_real abs_mult by (intro mult_mono) (auto simp: path_image_def) qed auto also have "?I = contour_integral (part_circlepath c r a b) f" by (simp add: contour_integral_integral vector_derivative_part_circlepath mult_ac) finally show ?thesis by simp qed lemma contour_integral_spike_finite_simple_path: assumes "finite A" "simple_path g" "g = g'" "\x. x \ path_image g - A \ f x = f' x" shows "contour_integral g f = contour_integral g' f'" unfolding contour_integral_integral proof (rule integral_spike) have "finite (g -` A \ {0<..<1})" using \simple_path g\ \finite A\ by (intro finite_vimage_IntI simple_path_inj_on) auto hence "finite ({0, 1} \ g -` A \ {0<..<1})" by auto thus "negligible ({0, 1} \ g -` A \ {0<..<1})" by (rule negligible_finite) next fix x assume "x \ {0..1} - ({0, 1} \ g -` A \ {0<..<1})" hence "g x \ path_image g - A" by (auto simp: path_image_def) from assms(4)[OF this] and assms(3) show "f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)" by simp qed proposition contour_integral_bound_part_circlepath_strong: assumes fi: "f contour_integrable_on part_circlepath z r s t" and "finite k" and le: "0 \ B" "0 < r" "s \ t" and B: "\x. x \ path_image(part_circlepath z r s t) - k \ norm(f x) \ B" shows "cmod (contour_integral (part_circlepath z r s t) f) \ B * r * (t - s)" proof - from fi have "(f has_contour_integral contour_integral (part_circlepath z r s t) f) (part_circlepath z r s t)" by (rule has_contour_integral_integral) from has_contour_integral_bound_part_circlepath_strong[OF this assms(2-)] show ?thesis by auto qed lemma cos_le_zero: assumes "x \ {pi/2..3*pi/2}" shows "cos x \ 0" proof - have "cos x = -cos (x - pi)" by (simp add: cos_diff) moreover from assms have "cos (x - pi) \ 0" by (intro cos_ge_zero) auto ultimately show ?thesis by simp qed lemma cos_le_zero': "x \ {-3*pi/2..-pi/2} \ cos x \ 0" using cos_le_zero[of "-x"] by simp lemma cis_minus_pi_half [simp]: "cis (- (pi / 2)) = -\" by (simp add: complex_eq_iff) lemma winding_number_join_pos_combined': "\valid_path \1 \ z \ path_image \1 \ 0 < Re (winding_number \1 z); valid_path \2 \ z \ path_image \2 \ 0 < Re (winding_number \2 z); pathfinish \1 = pathstart \2\ \ valid_path(\1 +++ \2) \ z \ path_image(\1 +++ \2) \ 0 < Re(winding_number(\1 +++ \2) z)" by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path) lemma Union_atLeastAtMost_real_of_nat: - assumes "a < b" + assumes "a < b" shows "(\n\{a.. {real a..real b}" thus "x \ (\n\{a.. real a" "x < real b" by simp_all hence "x \ real (nat \x\)" "x \ real (Suc (nat \x\))" by linarith+ - moreover from x have "nat \x\ \ a" "nat \x\ < b" by linarith+ + moreover from x have "nat \x\ \ a" "nat \x\ < b" by linarith+ ultimately have "\n\{a.. {real n..real (n + 1)}" by (intro bexI[of _ "nat \x\"]) simp_all thus ?thesis by blast qed qed auto lemma nat_sum_has_integral_floor: fixes f :: "nat \ 'a :: banach" assumes mn: "m < n" shows "((\x. f (nat \x\)) has_integral sum f {m..i. {real i..real (Suc i)}) ` {m..x. f (nat \x\)) has_integral (\X\D. f (nat \Inf X\))) {real m..real n}" proof (rule has_integral_combine_division) fix X assume X: "X \ D" have "nat \x\ = nat \Inf X\" if "x \ X - {Sup X}" for x using that X by (auto simp: D_def nat_eq_iff floor_eq_iff) hence "((\x. f (nat \x\)) has_integral f (nat \Inf X\)) X \ ((\x. f (nat \Inf X\)) has_integral f (nat \Inf X\)) X" using X by (intro has_integral_spike_eq[of "{Sup X}"]) auto also from X have "\" using has_integral_const_real[of "f (nat \Inf X\)" "Inf X" "Sup X"] by (auto simp: D_def) finally show "((\x. f (nat \x\)) has_integral f (nat \Inf X\)) X" . qed fact+ also have "(\X\D. f (nat \Inf X\)) = (\k\{m.. 'a :: banach" assumes mn: "m < n" shows "((\x. f (nat \x\)) has_integral sum f {m<..n}) {real m..real n}" proof - define D where "D = (\i. {real i..real (Suc i)}) ` {m..x. f (nat \x\)) has_integral (\X\D. f (nat \Sup X\))) {real m..real n}" proof (rule has_integral_combine_division) fix X assume X: "X \ D" have "nat \x\ = nat \Sup X\" if "x \ X - {Inf X}" for x using that X by (auto simp: D_def nat_eq_iff ceiling_eq_iff) hence "((\x. f (nat \x\)) has_integral f (nat \Sup X\)) X \ ((\x. f (nat \Sup X\)) has_integral f (nat \Sup X\)) X" using X by (intro has_integral_spike_eq[of "{Inf X}"]) auto also from X have "\" using has_integral_const_real[of "f (nat \Sup X\)" "Inf X" "Sup X"] by (auto simp: D_def) finally show "((\x. f (nat \x\)) has_integral f (nat \Sup X\)) X" . qed fact+ also have "(\X\D. f (nat \Sup X\)) = (\k\{m.. = (\k\{m<..n}. f k)" by (intro sum.reindex_bij_witness[of _ "\x. x - 1" Suc]) auto finally show ?thesis . qed lemma zeta_partial_sum_le: fixes x :: real and m :: nat assumes x: "x \ {0<..1}" shows "(\k=1..m. real k powr (x - 1)) \ real m powr x / x" proof - consider "m = 0" | "m = 1" | "m > 1" by force thus ?thesis proof cases assume m: "m > 1" hence "{1..m} = insert 1 {1<..m}" by auto also have "(\k\\. real k powr (x - 1)) = 1 + (\k\{1<..m}. real k powr (x - 1))" by simp also have "(\k\{1<..m}. real k powr (x - 1)) \ real m powr x / x - 1 / x" proof (rule has_integral_le) show "((\t. (nat \t\) powr (x - 1)) has_integral (\n\{1<..m}. n powr (x - 1))) {real 1..m}" using m by (intro nat_sum_has_integral_ceiling) auto next have "((\t. t powr (x - 1)) has_integral (real m powr x / x - real 1 powr x / x)) {real 1..real m}" by (intro fundamental_theorem_of_calculus) (insert x m, auto simp flip: has_field_derivative_iff_has_vector_derivative intro!: derivative_eq_intros) thus "((\t. t powr (x - 1)) has_integral (real m powr x / x - 1 / x)) {real 1..real m}" by simp qed (insert x, auto intro!: powr_mono2') also have "1 + (real m powr x / x - 1 / x) \ real m powr x / x" using x by (simp add: field_simps) finally show ?thesis by simp qed (use assms in auto) qed lemma zeta_partial_sum_le': fixes x :: real and m :: nat assumes x: "x > 0" and m: "m > 0" shows "(\n=1..m. real n powr (x - 1)) \ m powr x * (1 / x + 1 / m)" proof (cases "x > 1") case False with assms have "(\n=1..m. real n powr (x - 1)) \ m powr x / x" by (intro zeta_partial_sum_le) auto also have "\ \ m powr x * (1 / x + 1 / m)" using assms by (simp add: field_simps) finally show ?thesis . next case True have "(\n\{1..m}. n powr (x - 1)) = (\n\insert m {0.. = m powr (x - 1) + (\n\{0..n\{0.. real m powr x / x" proof (rule has_integral_le) show "((\t. (nat \t\) powr (x - 1)) has_integral (\n\{0..t. t powr (x - 1)) has_integral (real m powr x / x)) {real 0..real m}" using has_integral_powr_from_0[of "x - 1"] x by auto next fix t assume "t \ {real 0..real m}" with \x > 1\ show "real (nat \t\) powr (x - 1) \ t powr (x - 1)" by (cases "t = 0") (auto intro: powr_mono2) qed also have "m powr (x - 1) + m powr x / x = m powr x * (1 / x + 1 / m)" using m x by (simp add: powr_diff field_simps) finally show ?thesis by simp qed lemma natfun_bigo_1E: assumes "(f :: nat \ _) \ O(\_. 1)" obtains C where "C \ lb" "\n. norm (f n) \ C" proof - from assms obtain C N where "\n\N. norm (f n) \ C" by (auto elim!: landau_o.bigE simp: eventually_at_top_linorder) hence *: "norm (f n) \ Max ({C, lb} \ (norm ` f ` {.. N") (subst Max_ge_iff; force simp: image_iff)+ moreover have "Max ({C, lb} \ (norm ` f ` {.. lb" by (intro Max.coboundedI) auto ultimately show ?thesis using that by blast qed lemma natfun_bigo_iff_Bseq: "f \ O(\_. 1) \ Bseq f" proof assume "Bseq f" then obtain C where "C > 0" "\n. norm (f n) \ C" by (auto simp: Bseq_def) thus "f \ O(\_. 1)" by (intro bigoI[of _ C]) auto next assume "f \ O(\_. 1)" from natfun_bigo_1E[OF this, where lb = 1] obtain C where "C \ 1" "\n. norm (f n) \ C" by auto thus "Bseq f" by (auto simp: Bseq_def intro!: exI[of _ C]) qed lemma enn_decreasing_sum_le_set_nn_integral: fixes f :: "real \ ennreal" assumes decreasing: "\x y. 0 \ x \ x \ y \ f y \ f x" shows "(\n. f (real (Suc n))) \ set_nn_integral lborel {0..} f" proof - have "(\n. (f (Suc n))) = (\n. \\<^sup>+x\{real n<..real (Suc n)}. (f (Suc n)) \lborel)" by (subst nn_integral_cmult_indicator) auto also have "nat \x\ = Suc n" if "x \ {real n<..real (Suc n)}" for x n using that by (auto simp: nat_eq_iff ceiling_eq_iff) hence "(\n. \\<^sup>+x\{real n<..real (Suc n)}. (f (Suc n)) \lborel) = (\n. \\<^sup>+x\{real n<..real (Suc n)}. (f (real (nat \x\))) \lborel)" by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def) also have "\ = (\\<^sup>+x\(\i. {real i<..real (Suc i)}). (f (nat \x::real\)) \lborel)" by (subst nn_integral_disjoint_family) (auto simp: disjoint_family_on_def) also have "\ \ (\\<^sup>+x\{0..}. (f x) \lborel)" by (intro nn_integral_mono) (auto simp: indicator_def intro!: decreasing) finally show ?thesis . qed (* TODO replace version in library *) lemma nn_integral_has_integral_lebesgue: fixes f :: "'a::euclidean_space \ real" assumes nonneg: "\x. x \ \ \ 0 \ f x" and I: "(f has_integral I) \" shows "integral\<^sup>N lborel (\x. indicator \ x * f x) = I" proof - from I have "(\x. indicator \ x *\<^sub>R f x) \ lebesgue \\<^sub>M borel" by (rule has_integral_implies_lebesgue_measurable) then obtain f' :: "'a \ real" where [measurable]: "f' \ borel \\<^sub>M borel" and eq: "AE x in lborel. indicator \ x * f x = f' x" by (auto dest: completion_ex_borel_measurable_real) from I have "((\x. abs (indicator \ x * f x)) has_integral I) UNIV" using nonneg by (simp add: indicator_def if_distrib[of "\x. x * f y" for y] cong: if_cong) also have "((\x. abs (indicator \ x * f x)) has_integral I) UNIV \ ((\x. abs (f' x)) has_integral I) UNIV" using eq by (intro has_integral_AE) auto finally have "integral\<^sup>N lborel (\x. abs (f' x)) = I" by (rule nn_integral_has_integral_lborel[rotated 2]) auto also have "integral\<^sup>N lborel (\x. abs (f' x)) = integral\<^sup>N lborel (\x. abs (indicator \ x * f x))" using eq by (intro nn_integral_cong_AE) auto also have "(\x. abs (indicator \ x * f x)) = (\x. indicator \ x * f x)" using nonneg by (auto simp: indicator_def fun_eq_iff) finally show ?thesis . qed lemma decreasing_sum_le_integral: fixes f :: "real \ real" assumes nonneg: "\x. x \ 0 \ f x \ 0" assumes decreasing: "\x y. 0 \ x \ x \ y \ f y \ f x" assumes integral: "(f has_integral I) {0..}" shows "summable (\i. f (real (Suc i)))" and "suminf (\i. f (real (Suc i))) \ I" proof - have [simp]: "I \ 0" by (intro has_integral_nonneg[OF integral] nonneg) auto have "(\n. ennreal (f (Suc n))) = (\n. \\<^sup>+x\{real n<..real (Suc n)}. ennreal (f (Suc n)) \lborel)" by (subst nn_integral_cmult_indicator) auto also have "nat \x\ = Suc n" if "x \ {real n<..real (Suc n)}" for x n using that by (auto simp: nat_eq_iff ceiling_eq_iff) hence "(\n. \\<^sup>+x\{real n<..real (Suc n)}. ennreal (f (Suc n)) \lborel) = (\n. \\<^sup>+x\{real n<..real (Suc n)}. ennreal (f (real (nat \x\))) \lborel)" by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def) also have "\ = (\\<^sup>+x\(\i. {real i<..real (Suc i)}). ennreal (f (nat \x::real\)) \lborel)" by (subst nn_integral_disjoint_family) (auto simp: disjoint_family_on_def intro!: measurable_completion) also have "\ \ (\\<^sup>+x\{0..}. ennreal (f x) \lborel)" by (intro nn_integral_mono) (auto simp: indicator_def nonneg intro!: decreasing) also have "\ = (\\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \lborel)" by (intro nn_integral_cong) (auto simp: indicator_def) also have "\ = ennreal I" using nn_integral_has_integral_lebesgue[OF nonneg integral] by (auto simp: nonneg) finally have *: "(\n. ennreal (f (Suc n))) \ ennreal I" . from * show summable: "summable (\i. f (real (Suc i)))" by (intro summable_suminf_not_top) (auto simp: top_unique intro: nonneg) note * also from summable have "(\n. ennreal (f (Suc n))) = ennreal (\n. f (Suc n))" by (subst suminf_ennreal2) (auto simp: o_def nonneg) finally show "(\n. f (real (Suc n))) \ I" by (subst (asm) ennreal_le_iff) auto qed lemma decreasing_sum_le_integral': fixes f :: "real \ real" assumes "\x. x \ 0 \ f x \ 0" assumes "\x y. 0 \ x \ x \ y \ f y \ f x" assumes "(f has_integral I) {0..}" shows "summable (\i. f (real i))" and "suminf (\i. f (real i)) \ f 0 + I" proof - have "summable ((\i. f (real (Suc i))))" using decreasing_sum_le_integral[OF assms] by (simp add: o_def) thus *: "summable (\i. f (real i))" by (subst (asm) summable_Suc_iff) have "(\n. f (real (Suc n))) \ I" by (intro decreasing_sum_le_integral assms) thus "suminf (\i. f (real i)) \ f 0 + I" using * by (subst (asm) suminf_split_head) auto qed lemma norm_suminf_le: assumes "\n. norm (f n :: 'a :: banach) \ g n" "summable g" shows "norm (suminf f) \ suminf g" proof - have *: "summable (\n. norm (f n))" using assms by (intro summable_norm summable_comparison_test[OF _ assms(2)] exI[of _ 0]) auto hence "norm (suminf f) \ (\n. norm (f n))" by (intro summable_norm) auto also have "\ \ suminf g" by (intro suminf_le * assms allI) finally show ?thesis . qed lemma of_nat_powr_neq_1_complex [simp]: assumes "n > 1" "Re s \ 0" shows "of_nat n powr s \ (1::complex)" proof - have "norm (of_nat n powr s) = real n powr Re s" by (simp add: norm_powr_real_powr) also have "\ \ 1" using assms by (auto simp: powr_def) finally show ?thesis by auto qed lemma abs_summable_on_uminus_iff: "(\x. -f x) abs_summable_on A \ f abs_summable_on A" using abs_summable_on_uminus[of f A] abs_summable_on_uminus[of "\x. -f x" A] by auto lemma abs_summable_on_cmult_right_iff: fixes f :: "'a \ 'b :: {banach, real_normed_field, second_countable_topology}" assumes "c \ 0" shows "(\x. c * f x) abs_summable_on A \ f abs_summable_on A" using assms abs_summable_on_cmult_right[of c f A] abs_summable_on_cmult_right[of "inverse c" "\x. c * f x" A] by (auto simp: field_simps) lemma abs_summable_on_cmult_left_iff: fixes f :: "'a \ 'b :: {banach, real_normed_field, second_countable_topology}" assumes "c \ 0" shows "(\x. f x * c) abs_summable_on A \ f abs_summable_on A" using assms abs_summable_on_cmult_left[of c f A] abs_summable_on_cmult_left[of "inverse c" "\x. f x * c" A] by (auto simp: field_simps) lemma fds_logderiv_completely_multiplicative: fixes f :: "'a :: {real_normed_field} fds" assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 \ 0" shows "fds_deriv f / f = - fds (\n. fds_nth f n * mangoldt n)" proof - have "fds_deriv f / f = - fds (\n. fds_nth f n * mangoldt n) * f / f" using completely_multiplicative_fds_deriv[of "fds_nth f"] assms by simp also have "\ = - fds (\n. fds_nth f n * mangoldt n)" using assms by (simp add: divide_fds_def fds_right_inverse) finally show ?thesis . qed lemma fds_nth_logderiv_completely_multiplicative: fixes f :: "'a :: {real_normed_field} fds" assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 \ 0" shows "fds_nth (fds_deriv f / f) n = -fds_nth f n * mangoldt n" using assms by (subst fds_logderiv_completely_multiplicative) (simp_all add: fds_nth_fds') lemma eval_fds_logderiv_completely_multiplicative: fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds" defines "h \ fds_deriv f / f" assumes "completely_multiplicative_function (fds_nth f)" and [simp]: "fds_nth f 1 \ 0" assumes "s \ 1 > abs_conv_abscissa f" shows "(\p. of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1)) abs_summable_on {p. prime p}" (is ?th1) and "eval_fds h s = -(\\<^sub>ap | prime p. of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))" (is ?th2) proof - let ?P = "{p::nat. prime p}" interpret f: completely_multiplicative_function "fds_nth f" by fact have "fds_abs_converges h s" using abs_conv_abscissa_completely_multiplicative_log_deriv[OF assms(2)] assms by (intro fds_abs_converges) auto hence *: "(\n. fds_nth h n / nat_power n s) abs_summable_on UNIV" by (auto simp: h_def fds_abs_converges_altdef') note * also have "(\n. fds_nth h n / nat_power n s) abs_summable_on UNIV \ (\x. -fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow" unfolding h_def using fds_nth_logderiv_completely_multiplicative[OF assms(2)] by (intro abs_summable_on_cong_neutral) (auto simp: fds_nth_fds mangoldt_def) finally have sum1: "(\x. -fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow" by (rule abs_summable_on_subset) auto also have "?this \ (\(p,k). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on (?P \ UNIV)" using bij_betw_primepows unfolding case_prod_unfold by (intro abs_summable_on_reindex_bij_betw [symmetric]) also have "\ \ (\(p,k). -((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on (?P \ UNIV)" unfolding case_prod_unfold by (intro abs_summable_on_cong, subst mangoldt_primepow) (auto simp: f.mult f.power nat_power_mult_distrib nat_power_power_left power_divide dest: prime_gt_1_nat) finally have sum2: \ . have sum4: "summable (\n. (norm (fds_nth f p / nat_power p s)) ^ Suc n)" if p: "prime p" for p proof - have "summable (\n. \ln (real p)\ * (norm (fds_nth f p / nat_power p s)) ^ Suc n)" using p abs_summable_on_Sigma_project2[OF sum2, of p] unfolding abs_summable_on_nat_iff' by (simp add: norm_power norm_mult norm_divide mult_ac del: power_Suc) thus ?thesis by (rule summable_mult_D) (insert p, auto dest: prime_gt_1_nat) qed have sums: "(\n. (fds_nth f p / nat_power p s) ^ Suc n) sums (1 / (1 - fds_nth f p / nat_power p s) - 1)" if p: "prime p" for p :: nat proof - from sum4[OF p] have "norm (fds_nth f p / nat_power p s) < 1" unfolding summable_Suc_iff by (simp add: summable_geometric_iff) from geometric_sums[OF this] show ?thesis by (subst sums_Suc_iff) auto qed have eq: "(\\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = -(of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))" if p: "prime p" for p proof - have "(\\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = (\\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (-ln (real p))" using sum4[of p] p by (subst infsetsum_cmult_left [symmetric]) (auto simp: abs_summable_on_nat_iff' norm_power simp del: power_Suc) - also have "(\\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) = + also have "(\\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) = (1 / (1 - fds_nth f p / nat_power p s) - 1)" using sum4[OF p] sums[OF p] by (subst infsetsum_nat') (auto simp: sums_iff abs_summable_on_nat_iff' norm_power simp del: power_Suc) finally show ?thesis by (simp add: mult_ac) qed have sum3: "(\x. \\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}" using sum2 by (rule abs_summable_on_Sigma_project1') auto - also have "?this \ (\p. -(of_real (ln (real p)) * + also have "?this \ (\p. -(of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1))) abs_summable_on {p. prime p}" by (intro abs_summable_on_cong eq) auto also have "\ \ ?th1" by (subst abs_summable_on_uminus_iff) auto finally show ?th1 . have "eval_fds h s = (\\<^sub>an. fds_nth h n / nat_power n s)" using * unfolding eval_fds_def by (subst infsetsum_nat') auto also have "\ = (\\<^sub>an \ {n. primepow n}. -fds_nth f n * mangoldt n / nat_power n s)" unfolding h_def using fds_nth_logderiv_completely_multiplicative[OF assms(2)] by (intro infsetsum_cong_neutral) (auto simp: fds_nth_fds mangoldt_def) also have "\ = (\\<^sub>a(p,k)\(?P \ UNIV). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s)" - using bij_betw_primepows unfolding case_prod_unfold + using bij_betw_primepows unfolding case_prod_unfold by (intro infsetsum_reindex_bij_betw [symmetric]) - also have "\ = (\\<^sub>a(p,k)\(?P \ UNIV). + also have "\ = (\\<^sub>a(p,k)\(?P \ UNIV). -((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))" by (intro infsetsum_cong) - (auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat + (auto simp: f.mult f.power mangoldt_def aprimedivisor_prime_power ln_realpow prime_gt_0_nat nat_power_power_left divide_simps simp del: power_Suc) - also have "\ = (\\<^sub>ap | prime p. \\<^sub>ak. + also have "\ = (\\<^sub>ap | prime p. \\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))" using sum2 by (subst infsetsum_Times) (auto simp: case_prod_unfold) also have "\ = (\\<^sub>ap | prime p. -(of_real (ln (real p)) * (1 / (1 - fds_nth f p / nat_power p s) - 1)))" using eq by (intro infsetsum_cong) auto finally show ?th2 by (subst (asm) infsetsum_uminus) -qed +qed lemma eval_fds_logderiv_zeta: assumes "Re s > 1" shows "(\p. of_real (ln (real p)) / (p powr s - 1)) abs_summable_on {p. prime p}" (is ?th1) and "deriv zeta s / zeta s = -(\\<^sub>ap | prime p. of_real (ln (real p)) / (p powr s - 1))" (is ?th2) proof - have *: "completely_multiplicative_function (fds_nth fds_zeta :: _ \ complex)" by standard auto note abscissa = le_less_trans[OF abs_conv_abscissa_completely_multiplicative_log_deriv[OF *]] have "(\p. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1)) abs_summable_on {p. prime p}" using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms by auto also have "?this \ (\p. ln (real p) / (p powr s - 1)) abs_summable_on {p. prime p}" using assms by (intro abs_summable_on_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat) finally show ?th1 . from assms have ev: "eventually (\z. z \ {z. Re z > 1}) (nhds s)" by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto have "deriv zeta s = deriv (eval_fds fds_zeta) s" by (intro deriv_cong_ev[OF eventually_mono[OF ev]]) (auto simp: eval_fds_zeta) also have "deriv (eval_fds fds_zeta) s / zeta s = eval_fds (fds_deriv fds_zeta / fds_zeta) s" using assms zeta_Re_gt_1_nonzero[of s] by (subst eval_fds_log_deriv) (auto simp: eval_fds_zeta eval_fds_deriv intro!: abscissa) also have "eval_fds (fds_deriv fds_zeta / fds_zeta) s = -(\\<^sub>ap | prime p. ln (real p) * (1 / (1 - fds_nth fds_zeta p / p powr s) - 1))" (is "_ = -?S") using eval_fds_logderiv_completely_multiplicative[OF *, of s] assms by auto also have "?S = (\\<^sub>ap | prime p. ln (real p) / (p powr s - 1))" using assms by (intro infsetsum_cong) (auto simp: fds_nth_zeta divide_simps dest: prime_gt_1_nat) finally show ?th2 . qed lemma sums_logderiv_zeta: assumes "Re s > 1" shows "(\p. if prime p then of_real (ln (real p)) / (of_nat p powr s - 1) else 0) sums -(deriv zeta s / zeta s)" (is "?f sums _") proof - note * = eval_fds_logderiv_zeta[OF assms] from sums_infsetsum_nat[OF *(1)] and *(2) show ?thesis by simp qed lemma abs_conv_abscissa_diff_le: "abs_conv_abscissa (f - g :: 'a :: dirichlet_series fds) \ max (abs_conv_abscissa f) (abs_conv_abscissa g)" using abs_conv_abscissa_add_le[of f "-g"] by auto lemma abs_conv_abscissa_diff_leI: - "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ abs_conv_abscissa g \ d \ + "abs_conv_abscissa (f :: 'a :: dirichlet_series fds) \ d \ abs_conv_abscissa g \ d \ abs_conv_abscissa (f - g) \ d" using abs_conv_abscissa_diff_le[of f g] by (auto simp: le_max_iff_disj) lemma range_add_nat: "range (\n. n + c) = {(c::nat)..}" proof safe fix x assume "x \ c" hence "x = x - c + c" by simp thus "x \ range (\n. n + c)" by blast qed auto lemma abs_summable_hurwitz_zeta: assumes "Re s > 1" "a + real b > 0" shows "(\n. 1 / (of_nat n + a) powr s) abs_summable_on {b..}" proof - from assms have "summable (\n. cmod (1 / (of_nat (n + b) + a) powr s))" using summable_hurwitz_zeta_real[of "Re s" "a + b"] by (auto simp: norm_divide powr_minus field_simps norm_powr_real_powr) hence "(\n. 1 / (of_nat (n + b) + a) powr s) abs_summable_on UNIV" by (auto simp: abs_summable_on_nat_iff' add_ac) also have "?this \ (\n. 1 / (of_nat n + a) powr s) abs_summable_on range (\n. n + b)" by (rule abs_summable_on_reindex_iff) auto also have "range (\n. n + b) = {b..}" by (rule range_add_nat) finally show ?thesis . qed lemma hurwitz_zeta_nat_conv_infsetsum: assumes "a > 0" and "Re s > 1" shows "hurwitz_zeta (real a) s = (\\<^sub>an. of_nat (n + a) powr -s)" "hurwitz_zeta (real a) s = (\\<^sub>an\{a..}. of_nat n powr -s)" proof - have "hurwitz_zeta (real a) s = (\n. of_nat (n + a) powr -s)" using assms by (subst hurwitz_zeta_conv_suminf) auto also have "\ = (\\<^sub>an. of_nat (n + a) powr -s)" using abs_summable_hurwitz_zeta[of s a 0] assms by (intro infsetsum_nat' [symmetric]) (auto simp: powr_minus field_simps) finally show "hurwitz_zeta (real a) s = (\\<^sub>an. of_nat (n + a) powr -s)" . also have "\ = (\\<^sub>an\range (\n. n + a). of_nat n powr -s)" by (rule infsetsum_reindex [symmetric]) auto also have "range (\n. n + a) = {a..}" by (rule range_add_nat) finally show "hurwitz_zeta (real a) s = (\\<^sub>an\{a..}. of_nat n powr -s)" . -qed +qed lemma continuous_on_pre_zeta [continuous_intros]: - assumes "continuous_on A f" "a > 0" + assumes "continuous_on A f" "a > 0" shows "continuous_on A (\x. pre_zeta a (f x))" proof - from assms have "continuous_on UNIV (pre_zeta a)" by (intro holomorphic_on_imp_continuous_on[OF holomorphic_pre_zeta]) auto from continuous_on_compose2[OF this assms(1)] show ?thesis by simp qed lemma continuous_pre_zeta [continuous_intros]: - assumes "continuous (at x within A) f" "a > 0" + assumes "continuous (at x within A) f" "a > 0" shows "continuous (at x within A) (\x. pre_zeta a (f x))" proof - have "continuous (at z) (pre_zeta a)" for z by (rule continuous_on_interior[of UNIV]) (insert assms, auto intro!: continuous_intros) from continuous_within_compose3[OF this assms(1)] show ?thesis . qed lemma pre_zeta_bound: assumes "0 < Re s" and a: "a > 0" shows "norm (pre_zeta a s) \ (1 + norm s / Re s) / 2 * a powr -Re s" proof - let ?f = "\x. - (s * (x + a) powr (-1-s))" let ?g' = "\x. norm s * (x + a) powr (-1-Re s)" let ?g = "\x. -norm s / Re s * (x + a) powr (-Re s)" define R where "R = EM_remainder 1 ?f 0" have [simp]: "-Re s - 1 = -1 - Re s" by (simp add: algebra_simps) have "\frac x - 1 / 2\ \ 1 / 2" for x :: real unfolding frac_def by linarith hence "\pbernpoly (Suc 0) x\ \ 1 / 2" for x by (simp add: pbernpoly_def bernpoly_def) moreover have "((\b. cmod s * (b + a) powr - Re s / Re s) \ 0) at_top" using \Re s > 0\ \a > 0\ by real_asymp ultimately have *: "\x. x \ real 0 \ norm (EM_remainder 1 ?f (int x)) \ (1 / 2) / fact 1 * (-?g (real x))" using \a > 0\ \Re s > 0\ by (intro norm_EM_remainder_le_strong_nat'[where g' = ?g' and Y = "{}"]) (auto intro!: continuous_intros derivative_eq_intros simp: field_simps norm_mult norm_powr_real_powr add_eq_0_iff) have R: "norm R \ norm s / (2 * Re s) * a powr -Re s" unfolding R_def using spec[OF *, of 0] by simp - + from assms have "pre_zeta a s = a powr -s / 2 + R" by (simp add: pre_zeta_def pre_zeta_aux_def R_def) also have "norm \ \ a powr -Re s / 2 + norm s / (2 * Re s) * a powr -Re s" using a by (intro order.trans[OF norm_triangle_ineq] add_mono R) (auto simp: norm_powr_real_powr) also have "\ = (1 + norm s / Re s) / 2 * a powr -Re s" by (simp add: field_simps) finally show ?thesis . qed lemma pre_zeta_bound': assumes "0 < Re s" and a: "a > 0" shows "norm (pre_zeta a s) \ norm s / (Re s * a powr Re s)" proof - from assms have "norm (pre_zeta a s) \ (1 + norm s / Re s) / 2 * a powr -Re s" by (intro pre_zeta_bound) auto also have "\ = (Re s + norm s) / 2 / (Re s * a powr Re s)" using assms by (auto simp: field_simps powr_minus) also have "Re s + norm s \ norm s + norm s" by (intro add_right_mono complex_Re_le_cmod) also have "(norm s + norm s) / 2 = norm s" by simp finally show "norm (pre_zeta a s) \ norm s / (Re s * a powr Re s)" using assms by (simp add: divide_right_mono) qed lemma summable_comparison_test_bigo: fixes f :: "nat \ real" assumes "summable (\n. norm (g n))" "f \ O(g)" shows "summable f" proof - from \f \ O(g)\ obtain C where C: "eventually (\x. norm (f x) \ C * norm (g x)) at_top" by (auto elim: landau_o.bigE) thus ?thesis by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult) qed lemma deriv_zeta_eq: assumes s: "s \ 1" shows "deriv zeta s = deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2" proof - from s have ev: "eventually (\z. z \ 1) (nhds s)" by (intro t1_space_nhds) have [derivative_intros]: "(pre_zeta 1 has_field_derivative deriv (pre_zeta 1) s) (at s)" by (intro holomorphic_derivI[of _ UNIV] holomorphic_intros) auto have "((\s. pre_zeta 1 s + 1 / (s - 1)) has_field_derivative (deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2)) (at s)" using s by (auto intro!: derivative_eq_intros simp: power2_eq_square) also have "?this \ (zeta has_field_derivative (deriv (pre_zeta 1) s - 1 / (s - 1)\<^sup>2)) (at s)" by (intro has_field_derivative_cong_ev eventually_mono[OF ev]) (auto simp: zeta_def hurwitz_zeta_def) finally show ?thesis by (rule DERIV_imp_deriv) qed lemma zeta_remove_zero: assumes "Re s \ 1" shows "(s - 1) * pre_zeta 1 s + 1 \ 0" proof (cases "s = 1") case False hence "(s - 1) * pre_zeta 1 s + 1 = (s - 1) * zeta s" by (simp add: zeta_def hurwitz_zeta_def divide_simps) also from False assms have "\ \ 0" using zeta_Re_ge_1_nonzero[of s] by auto finally show ?thesis . qed auto lemma eval_fds_deriv_zeta: assumes "Re s > 1" shows "eval_fds (fds_deriv fds_zeta) s = deriv zeta s" proof - have ev: "eventually (\z. z \ {z. Re z > 1}) (nhds s)" using assms by (intro eventually_nhds_in_open open_halfspace_Re_gt) auto from assms have "eval_fds (fds_deriv fds_zeta) s = deriv (eval_fds fds_zeta) s" by (subst eval_fds_deriv) auto also have "\ = deriv zeta s" by (intro deriv_cong_ev eventually_mono[OF ev]) (auto simp: eval_fds_zeta) finally show ?thesis . qed lemma length_sorted_list_of_set [simp]: "finite A \ length (sorted_list_of_set A) = card A" by (metis length_remdups_card_conv length_sort set_sorted_list_of_set sorted_list_of_set_sort_remdups) lemma le_nat_iff': "x \ nat y \ x = 0 \ y \ 0 \ int x \ y" by auto lemma sum_upto_plus1: assumes "x \ 0" shows "sum_upto f (x + 1) = sum_upto f x + f (Suc (nat \x\))" proof - have "sum_upto f (x + 1) = sum f {0<..Suc (nat \x\)}" using assms by (simp add: sum_upto_altdef nat_add_distrib) also have "{0<..Suc (nat \x\)} = insert (Suc (nat \x\)) {0<..nat \x\}" by auto also have "sum f \ = sum_upto f x + f (Suc (nat \x\))" by (subst sum.insert) (auto simp: sum_upto_altdef add_ac) finally show ?thesis . qed lemma sum_upto_minus1: assumes "x \ 1" shows "sum_upto f (x - 1) = (sum_upto f x - f (nat \x\) :: 'a :: ab_group_add)" using sum_upto_plus1[of "x - 1" f] assms by (simp add: algebra_simps nat_diff_distrib) lemma integral_smallo: fixes f g g' :: "real \ real" assumes "f \ o(g')" and "filterlim g at_top at_top" assumes "\a' x. a \ a' \ a' \ x \ f integrable_on {a'..x}" assumes deriv: "\x. x \ a \ (g has_field_derivative g' x) (at x)" assumes cont: "continuous_on {a..} g'" assumes nonneg: "\x. x \ a \ g' x \ 0" shows "(\x. integral {a..x} f) \ o(g)" proof (rule landau_o.smallI) fix c :: real assume c: "c > 0" note [continuous_intros] = continuous_on_subset[OF cont] define c' where "c' = c / 2" from c have c': "c' > 0" by (simp add: c'_def) from landau_o.smallD[OF assms(1) this] obtain b where b: "\x. x \ b \ norm (f x) \ c' * norm (g' x)" unfolding eventually_at_top_linorder by blast define b' where "b' = max a b" define D where "D = norm (integral {a..b'} f)" have "filterlim (\x. c' * g x) at_top at_top" using c' by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] assms) hence "eventually (\x. c' * g x \ D - c' * g b') at_top" by (auto simp: filterlim_at_top) thus "eventually (\x. norm (integral {a..x} f) \ c * norm (g x)) at_top" using eventually_ge_at_top[of b'] proof eventually_elim case (elim x) have b': "a \ b'" "b \ b'" by (auto simp: b'_def) from elim b' have integrable: "(\x. \g' x\) integrable_on {b'..x}" by (intro integrable_continuous_real continuous_intros) auto have "integral {a..x} f = integral {a..b'} f + integral {b'..x} f" using elim b' by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] assms) auto also have "norm \ \ D + norm (integral {b'..x} f)" unfolding D_def by (rule norm_triangle_ineq) also have "norm (integral {b'..x} f) \ integral {b'..x} (\x. c' * norm (g' x))" using b' elim assms c' integrable by (intro integral_norm_bound_integral b assms) auto also have "\ = c' * integral {b'..x} (\x. \g' x\)" by simp also have "integral {b'..x} (\x. \g' x\) = integral {b'..x} g'" using assms b' by (intro integral_cong) auto also have "(g' has_integral (g x - g b')) {b'..x}" using b' elim by (intro fundamental_theorem_of_calculus) (auto simp flip: has_field_derivative_iff_has_vector_derivative intro!: has_field_derivative_at_within[OF deriv]) hence "integral {b'..x} g' = g x - g b'" by (simp add: has_integral_iff) also have "D + c' * (g x - g b') \ c * g x" using elim by (simp add: field_simps c'_def) also have "\ \ c * norm (g x)" using c by (intro mult_left_mono) auto finally show ?case by simp qed qed lemma integral_bigo: fixes f g g' :: "real \ real" assumes "f \ O(g')" and "filterlim g at_top at_top" assumes "\a' x. a \ a' \ a' \ x \ f integrable_on {a'..x}" assumes deriv: "\x. x \ a \ (g has_field_derivative g' x) (at x within {a..})" assumes cont: "continuous_on {a..} g'" assumes nonneg: "\x. x \ a \ g' x \ 0" shows "(\x. integral {a..x} f) \ O(g)" proof - note [continuous_intros] = continuous_on_subset[OF cont] from landau_o.bigE[OF assms(1)] obtain c b where c: "c > 0" and b: "\x. x \ b \ norm (f x) \ c * norm (g' x)" unfolding eventually_at_top_linorder by metis define c' where "c' = c / 2" define b' where "b' = max a b" define D where "D = norm (integral {a..b'} f)" have "filterlim (\x. c * g x) at_top at_top" using c by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] assms) hence "eventually (\x. c * g x \ D - c * g b') at_top" by (auto simp: filterlim_at_top) hence "eventually (\x. norm (integral {a..x} f) \ 2 * c * norm (g x)) at_top" using eventually_ge_at_top[of b'] proof eventually_elim case (elim x) have b': "a \ b'" "b \ b'" by (auto simp: b'_def) from elim b' have integrable: "(\x. \g' x\) integrable_on {b'..x}" by (intro integrable_continuous_real continuous_intros) auto have "integral {a..x} f = integral {a..b'} f + integral {b'..x} f" using elim b' by (intro Henstock_Kurzweil_Integration.integral_combine [symmetric] assms) auto also have "norm \ \ D + norm (integral {b'..x} f)" unfolding D_def by (rule norm_triangle_ineq) also have "norm (integral {b'..x} f) \ integral {b'..x} (\x. c * norm (g' x))" using b' elim assms c integrable by (intro integral_norm_bound_integral b assms) auto also have "\ = c * integral {b'..x} (\x. \g' x\)" by simp also have "integral {b'..x} (\x. \g' x\) = integral {b'..x} g'" using assms b' by (intro integral_cong) auto also have "(g' has_integral (g x - g b')) {b'..x}" using b' elim by (intro fundamental_theorem_of_calculus) (auto simp flip: has_field_derivative_iff_has_vector_derivative intro!: DERIV_subset[OF deriv]) hence "integral {b'..x} g' = g x - g b'" by (simp add: has_integral_iff) also have "D + c * (g x - g b') \ 2 * c * g x" using elim by (simp add: field_simps c'_def) also have "\ \ 2 * c * norm (g x)" using c by (intro mult_left_mono) auto finally show ?case by simp qed thus ?thesis by (rule bigoI) qed lemma primepows_le_subset: assumes x: "x > 0" and l: "l > 0" shows "{(p, i). prime p \ l \ i \ real (p ^ i) \ x} \ {..nat \root l x\} \ {..nat \log 2 x\}" proof safe fix p i :: nat assume pi: "prime p" "i \ l" "real (p ^ i) \ x" have "real p ^ l \ real p ^ i" using pi x l by (intro power_increasing) (auto dest: prime_gt_0_nat) also have "\ \ x" using pi by simp finally have "root l (real p ^ l) \ root l x" using x pi l by (subst real_root_le_iff) auto also have "root l (real p ^ l) = real p" using pi l by (subst real_root_pos2) auto finally show "p \ nat \root l x\" using pi l x by (simp add: le_nat_iff' le_floor_iff) from pi have "2 ^ i \ real p ^ i" using l by (intro power_mono) (auto dest: prime_gt_1_nat) also have "\ \ x" using pi by simp finally show "i \ nat \log 2 x\" using pi x by (auto simp: le_nat_iff' le_floor_iff le_log_iff powr_realpow) qed lemma mangoldt_non_primepow: "\primepow n \ mangoldt n = 0" by (auto simp: mangoldt_def) lemma le_imp_bigo_real: assumes "c \ 0" "eventually (\x. f x \ c * (g x :: real)) F" "eventually (\x. 0 \ f x) F" shows "f \ O[F](g)" proof - have "eventually (\x. norm (f x) \ c * norm (g x)) F" using assms(2,3) proof eventually_elim case (elim x) have "norm (f x) \ c * g x" using elim by simp also have "\ \ c * norm (g x)" by (intro mult_left_mono assms) auto finally show ?case . qed thus ?thesis by (intro bigoI[of _ c]) auto qed (* TODO: unneeded. But why does real_asymp not work? *) lemma ln_minus_ln_floor_bigo: "(\x. ln x - ln (real (nat \x\))) \ O(\_. 1)" proof (intro le_imp_bigo_real[of 1] eventually_mono[OF eventually_ge_at_top[of 1]]) fix x :: real assume x: "x \ 1" from x have *: "x - real (nat \x\) \ 1" by linarith from x have "ln x - ln (real (nat \x\)) \ (x - real (nat \x\)) / real (nat \x\)" by (intro ln_diff_le) auto also have "\ \ 1 / 1" using x * by (intro frac_le) auto finally show "ln x - ln (real (nat \x\)) \ 1 * 1" by simp qed auto lemma cos_geD: assumes "cos x \ cos a" "0 \ a" "a \ pi" "-pi \ x" "x \ pi" shows "x \ {-a..a}" proof (cases "x \ 0") case True with assms show ?thesis by (subst (asm) cos_mono_le_eq) auto next case False with assms show ?thesis using cos_mono_le_eq[of a "-x"] by auto qed (* TODO: Could be generalised *) lemma path_image_part_circlepath_same_Re: assumes "0 \ b" "b \ pi" "a = -b" "r \ 0" shows "path_image (part_circlepath c r a b) = sphere c r \ {s. Re s \ Re c + r * cos a}" proof safe fix z assume "z \ path_image (part_circlepath c r a b)" with assms obtain t where t: "t \ {a..b}" "z = c + of_real r * cis t" by (auto simp: path_image_part_circlepath exp_eq_polar) from t and assms show "z \ sphere c r" by (auto simp: dist_norm norm_mult) from t and assms show "Re z \ Re c + r * cos a" using cos_monotone_0_pi_le[of t b] cos_monotone_minus_pi_0'[of a t] by (cases "t \ 0") (auto intro!: mult_left_mono) next fix z assume z: "z \ sphere c r" "Re z \ Re c + r * cos a" show "z \ path_image (part_circlepath c r a b)" proof (cases "r = 0") case False with assms have r: "r > 0" by simp with z have z_eq: "z = c + r * cis (Arg (z - c))" using Arg_eq[of "z - c"] by (auto simp: dist_norm exp_eq_polar norm_minus_commute) moreover from z(2) r assms have "cos b \ cos (Arg (z - c))" by (subst (asm) z_eq) auto with assms have "Arg (z - c) \ {-b..b}" using Arg_le_pi[of "z - c"] mpi_less_Arg[of "z - c"] by (intro cos_geD) auto ultimately show "z \ path_image (part_circlepath c r a b)" using assms by (subst path_image_part_circlepath) (auto simp: exp_eq_polar) qed (insert assms z, auto simp: path_image_part_circlepath) qed lemma part_circlepath_rotate_left: "part_circlepath c r (x + a) (x + b) = (\z. c + cis x * (z - c)) \ part_circlepath c r a b" by (simp add: part_circlepath_def exp_eq_polar fun_eq_iff linepath_translate_left linepath_translate_right cis_mult add_ac) lemma part_circlepath_rotate_right: "part_circlepath c r (a + x) (b + x) = (\z. c + cis x * (z - c)) \ part_circlepath c r a b" by (simp add: part_circlepath_def exp_eq_polar fun_eq_iff linepath_translate_left linepath_translate_right cis_mult add_ac) lemma path_image_semicircle_Re_ge: assumes "r \ 0" shows "path_image (part_circlepath c r (-pi/2) (pi/2)) = sphere c r \ {s. Re s \ Re c}" by (subst path_image_part_circlepath_same_Re) (simp_all add: assms) lemma sphere_rotate: "(\z. c + cis x * (z - c)) ` sphere c r = sphere c r" proof safe fix z assume z: "z \ sphere c r" hence "z = c + cis x * (c + cis (-x) * (z - c) - c)" "c + cis (-x) * (z - c) \ sphere c r" by (auto simp: dist_norm norm_mult norm_minus_commute cis_conv_exp exp_minus field_simps norm_divide) with z show "z \ (\z. c + cis x * (z - c)) ` sphere c r" by blast qed (auto simp: dist_norm norm_minus_commute norm_mult) lemma path_image_semicircle_Re_le: assumes "r \ 0" shows "path_image (part_circlepath c r (pi/2) (3/2*pi)) = sphere c r \ {s. Re s \ Re c}" proof - let ?f = "(\z. c + cis pi * (z - c))" have *: "part_circlepath c r (pi/2) (3/2*pi) = part_circlepath c r (pi + (-pi/2)) (pi + pi/2)" by simp have "path_image (part_circlepath c r (pi/2) (3/2*pi)) = ?f ` sphere c r \ ?f ` {s. Re c \ Re s}" unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms] by auto also have "?f ` sphere c r = sphere c r" by (rule sphere_rotate) also have "?f ` {s. Re c \ Re s} = {s. Re c \ Re s}" by (auto simp: image_iff intro!: exI[of _ "2 * c - x" for x]) finally show ?thesis . qed lemma path_image_semicircle_Im_ge: assumes "r \ 0" shows "path_image (part_circlepath c r 0 pi) = sphere c r \ {s. Im s \ Im c}" proof - let ?f = "(\z. c + cis (pi/2) * (z - c))" have *: "part_circlepath c r 0 pi = part_circlepath c r (pi / 2 + (-pi/2)) (pi / 2 + pi/2)" by simp have "path_image (part_circlepath c r 0 pi) = ?f ` sphere c r \ ?f ` {s. Re c \ Re s}" unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms] by auto also have "?f ` sphere c r = sphere c r" by (rule sphere_rotate) also have "?f ` {s. Re c \ Re s} = {s. Im c \ Im s}" by (auto simp: image_iff intro!: exI[of _ "c - \ * (x - c)" for x]) finally show ?thesis . qed lemma path_image_semicircle_Im_le: assumes "r \ 0" shows "path_image (part_circlepath c r pi (2 * pi)) = sphere c r \ {s. Im s \ Im c}" proof - let ?f = "(\z. c + cis (3*pi/2) * (z - c))" have *: "part_circlepath c r pi (2*pi) = part_circlepath c r (3*pi/2 + (-pi/2)) (3*pi/2 + pi/2)" by simp have "path_image (part_circlepath c r pi (2 * pi)) = ?f ` sphere c r \ ?f ` {s. Re c \ Re s}" unfolding * part_circlepath_rotate_left path_image_compose path_image_semicircle_Re_ge[OF assms] by auto also have "?f ` sphere c r = sphere c r" by (rule sphere_rotate) also have "cis (3 * pi / 2) = -\" using cis_mult[of pi "pi / 2"] by simp hence "?f ` {s. Re c \ Re s} = {s. Im c \ Im s}" by (auto simp: image_iff intro!: exI[of _ "c + \ * (x - c)" for x]) finally show ?thesis . qed lemma powr_numeral [simp]: "x \ 0 \ (x::real) powr numeral y = x ^ numeral y" using powr_numeral[of x y] by (cases "x = 0") auto lemma eval_fds_logderiv_zeta_real: assumes "x > (1 :: real)" shows "(\p. ln (real p) / (p powr x - 1)) abs_summable_on {p. prime p}" (is ?th1) and "deriv zeta (of_real x) / zeta (of_real x) = -of_real (\\<^sub>ap | prime p. ln (real p) / (p powr x - 1))" (is ?th2) proof - have "(\p. Re (of_real (ln (real p)) / (of_nat p powr of_real x - 1))) abs_summable_on {p. prime p}" using assms by (intro abs_summable_Re eval_fds_logderiv_zeta) auto also have "?this \ ?th1" by (intro abs_summable_on_cong) (auto simp: powr_Reals_eq) finally show ?th1 . - show ?th2 using assms + show ?th2 using assms by (subst eval_fds_logderiv_zeta) (auto simp: infsetsum_of_real [symmetric] powr_Reals_eq) qed lemma fixes a b c d :: real assumes ab: "d * a + b \ 1" and c: "c < -1" and d: "d > 0" defines "C \ - ((ln (d * a + b) - 1 / (c + 1)) * (d * a + b) powr (c + 1) / (d * (c + 1)))" shows set_integrable_ln_powr_at_top: "(\x. (ln (d * x + b) * ((d * x + b) powr c))) absolutely_integrable_on {a<..}" (is ?th1) and set_lebesgue_integral_ln_powr_at_top: "(\x\{a<..}. (ln (d * x + b) * ((d * x + b) powr c)) \lborel) = C" (is ?th2) and ln_powr_has_integral_at_top: "((\x. ln (d * x + b) * (d * x + b) powr c) has_integral C) {a<..}" (is ?th3) proof - define f where "f = (\x. ln (d * x + b) * (d * x + b) powr c)" define F where "F = (\x. (ln (d * x + b) - 1 / (c + 1)) * (d * x + b) powr (c + 1) / (d * (c + 1)))" have *: "(F has_field_derivative f x) (at x)" "isCont f x" "f x \ 0" if "x > a" for x proof - have "1 \ d * a + b" by fact also have "\ < d * x + b" using that assms - by (intro add_strict_right_mono mult_strict_left_mono) + by (intro add_strict_right_mono mult_strict_left_mono) finally have gt_1: "d * x + b > 1" . show "(F has_field_derivative f x) (at x)" "isCont f x" using ab c d gt_1 by (auto simp: F_def f_def divide_simps intro!: derivative_eq_intros continuous_intros) (auto simp: algebra_simps powr_add)? show "f x \ 0" using gt_1 by (auto simp: f_def) qed have limits: "((F \ real_of_ereal) \ F a) (at_right (ereal a))" "((F \ real_of_ereal) \ 0) (at_left \)" using c ab d unfolding ereal_tendsto_simps1 F_def by (real_asymp; simp add: field_simps)+ have 1: "set_integrable lborel (einterval a \) f" using ab c limits by (intro interval_integral_FTC_nonneg) (auto intro!: * AE_I2) thus 2: "f absolutely_integrable_on {a<..}" by (auto simp: set_integrable_def integrable_completion) have "(LBINT x=ereal a..\. f x) = 0 - F a" using ab c limits by (intro interval_integral_FTC_nonneg) (auto intro!: *) thus 3: ?th2 by (simp add: interval_integral_to_infinity_eq F_def f_def C_def) show ?th3 using set_borel_integral_eq_integral[OF 1] 3 by (simp add: has_integral_iff f_def C_def) qed lemma ln_fact_conv_sum_upto: "ln (fact n) = sum_upto ln n" by (induction n) (auto simp: sum_upto_plus1 add.commute[of 1] ln_mult) lemma sum_upto_ln_conv_ln_fact: "sum_upto ln x = ln (fact (nat \x\))" by (simp add: ln_fact_conv_sum_upto sum_upto_altdef) lemma real_of_nat_div: "real (a div b) = real_of_int \real a / real b\" by (subst floor_divide_of_nat_eq) auto lemma integral_subset_negligible: fixes f :: "'a :: euclidean_space \ 'b :: banach" assumes "S \ T" "negligible (T - S)" shows "integral S f = integral T f" proof - have "integral T f = integral T (\x. if x \ S then f x else 0)" by (rule integral_spike[of "T - S"]) (use assms in auto) also have "\ = integral (S \ T) f" by (subst integral_restrict_Int) auto also have "S \ T = S" using assms by auto finally show ?thesis .. qed lemma integrable_on_cong [cong]: assumes "\x. x \ A \ f x = g x" "A = B" shows "f integrable_on A \ g integrable_on B" using has_integral_cong[of A f g, OF assms(1)] assms(2) by (auto simp: integrable_on_def) lemma measurable_sum_upto [measurable]: fixes f :: "'a \ nat \ real" assumes [measurable]: "\y. (\t. f t y) \ M \\<^sub>M borel" assumes [measurable]: "x \ M \\<^sub>M borel" shows "(\t. sum_upto (f t) (x t)) \ M \\<^sub>M borel" proof - have meas: "(\t. set_lebesgue_integral lborel {y. y \ 0 \ y - real (nat \x t\) \ 0} (\y. f t (nat \y\))) \ M \\<^sub>M borel" (is "?f \ _") unfolding set_lebesgue_integral_def by measurable also have "?f = (\t. sum_upto (f t) (x t))" proof fix t :: 'a show "?f t = sum_upto (f t) (x t)" proof (cases "x t < 1") case True hence "{y. y \ 0 \ y - real (nat \x t\) \ 0} = {0}" by auto thus ?thesis using True by (simp add: set_integral_at_point sum_upto_altdef) next case False define n where "n = nat \x t\" from False have "n > 0" by (auto simp: n_def) have *: "((\x. f t (nat \x\)) has_integral sum (f t) {0<..n}) {real 0..real n}" using \n > 0\ by (intro nat_sum_has_integral_ceiling) auto have **: "(\x. f t (nat \x\)) absolutely_integrable_on {real 0..real n}" proof (rule absolutely_integrable_absolutely_integrable_ubound) show "(\_. MAX n\{0..n}. \f t n\) absolutely_integrable_on {real 0..real n}" using \n > 0\ by (subst absolutely_integrable_on_iff_nonneg) (auto simp: Max_ge_iff intro!: exI[of _ "f t 0"]) show "(\x. f t (nat \x\)) integrable_on {real 0..real n}" using * by (simp add: has_integral_iff) next fix y :: real assume y: "y \ {real 0..real n}" have "f t (nat \y\) \ \f t (nat \y\)\" by simp also have "\ \ (MAX n\{0..n}. \f t n\)" using y by (intro Max.coboundedI) auto finally show "f t (nat \y\) \ (MAX n\{0..n}. \f t n\)" . qed have "sum (f t) {0<..n} = (\x\{real 0..real n}. f t (nat \x\) \lebesgue)" using has_integral_set_lebesgue[OF **] * by (simp add: has_integral_iff) also have "\ = (\x\{real 0..real n}. f t (nat \x\) \lborel)" unfolding set_lebesgue_integral_def by (subst integral_completion) auto also have "{real 0..real n} = {y. 0 \ y \ y - real (nat \x t\) \ 0}" by (auto simp: n_def) also have "sum (f t) {0<..n} = sum_upto (f t) (x t)" by (simp add: sum_upto_altdef n_def) finally show ?thesis .. qed qed finally show ?thesis . qed -end \ No newline at end of file +end