[STATEMENT]
lemma zeta_partial_sum_le':
  fixes x :: real and m :: nat
  assumes x: "x > 0" and m: "m > 0"
  shows   "(\<Sum>n=1..m. real n powr (x - 1)) \<le> m powr x * (1 / x + 1 / m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
proof (cases "x > 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
 2. \<not> 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 1 < x

goal (2 subgoals):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
 2. \<not> 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < x
0 < m
\<not> 1 < x
[PROOF STEP]
have "(\<Sum>n=1..m. real n powr (x - 1)) \<le> m powr x / x"
[PROOF STATE]
proof (prove)
using this:
0 < x
0 < m
\<not> 1 < x

goal (1 subgoal):
 1. (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
by (intro zeta_partial_sum_le) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x / x

goal (2 subgoals):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
 2. \<not> 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x / x

goal (2 subgoals):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
 2. \<not> 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
have "\<dots> \<le> m powr x * (1 / x + 1 / m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real m powr x / x \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x
0 < m

goal (1 subgoal):
 1. real m powr x / x \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
real m powr x / x \<le> real m powr x * (1 / x + 1 / real m)

goal (2 subgoals):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
 2. \<not> 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)

goal (1 subgoal):
 1. (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
1 < x

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
have "(\<Sum>n\<in>{1..m}. n powr (x - 1)) = (\<Sum>n\<in>insert m {0..<m}. n powr (x - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n = 1..m. real n powr (x - 1)) = (\<Sum>n\<in>insert m {0..<m}. real n powr (x - 1))
[PROOF STEP]
by (intro sum.mono_neutral_left) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 1..m. real n powr (x - 1)) = (\<Sum>n\<in>insert m {0..<m}. real n powr (x - 1))

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 1..m. real n powr (x - 1)) = (\<Sum>n\<in>insert m {0..<m}. real n powr (x - 1))

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
have "\<dots> = m powr (x - 1) + (\<Sum>n\<in>{0..<m}. n powr (x - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n\<in>insert m {0..<m}. real n powr (x - 1)) = real m powr (x - 1) + (\<Sum>n = 0..<m. real n powr (x - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>n\<in>insert m {0..<m}. real n powr (x - 1)) = real m powr (x - 1) + (\<Sum>n = 0..<m. real n powr (x - 1))

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n\<in>insert m {0..<m}. real n powr (x - 1)) = real m powr (x - 1) + (\<Sum>n = 0..<m. real n powr (x - 1))

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
have "(\<Sum>n\<in>{0..<m}. n powr (x - 1)) \<le> real m powr x / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n = 0..<m. real n powr (x - 1)) \<le> real m powr x / x
[PROOF STEP]
proof (rule has_integral_le)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (?f has_integral (\<Sum>n = 0..<m. real n powr (x - 1))) ?S
 2. (?g has_integral real m powr x / x) ?S
 3. \<And>x. x \<in> ?S \<Longrightarrow> ?f x \<le> ?g x
[PROOF STEP]
show "((\<lambda>t. (nat \<lfloor>t\<rfloor>) powr (x - 1)) has_integral (\<Sum>n\<in>{0..<m}. n powr (x - 1))) {real 0..m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. real (nat \<lfloor>t\<rfloor>) powr (x - 1)) has_integral (\<Sum>n = 0..<m. real n powr (x - 1))) {real 0..real m}
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
0 < m

goal (1 subgoal):
 1. ((\<lambda>t. real (nat \<lfloor>t\<rfloor>) powr (x - 1)) has_integral (\<Sum>n = 0..<m. real n powr (x - 1))) {real 0..real m}
[PROOF STEP]
by (intro nat_sum_has_integral_floor) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>t. real (nat \<lfloor>t\<rfloor>) powr (x - 1)) has_integral (\<Sum>n = 0..<m. real n powr (x - 1))) {real 0..real m}

goal (2 subgoals):
 1. (?g has_integral real m powr x / x) {real 0..real m}
 2. \<And>xa. xa \<in> {real 0..real m} \<Longrightarrow> real (nat \<lfloor>xa\<rfloor>) powr (x - 1) \<le> ?g xa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (?g has_integral real m powr x / x) {real 0..real m}
 2. \<And>xa. xa \<in> {real 0..real m} \<Longrightarrow> real (nat \<lfloor>xa\<rfloor>) powr (x - 1) \<le> ?g xa
[PROOF STEP]
show "((\<lambda>t. t powr (x - 1)) has_integral (real m powr x / x)) {real 0..real m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x) {real 0..real m}
[PROOF STEP]
using has_integral_powr_from_0[of "x - 1"] x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>- 1 < x - 1; 0 \<le> ?c\<rbrakk> \<Longrightarrow> ((\<lambda>xa. xa powr (x - 1)) has_integral ?c powr (x - 1 + 1) / (x - 1 + 1)) {0..?c}
0 < x

goal (1 subgoal):
 1. ((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x) {real 0..real m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>t. t powr (x - 1)) has_integral real m powr x / x) {real 0..real m}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {real 0..real m} \<Longrightarrow> real (nat \<lfloor>xa\<rfloor>) powr (x - 1) \<le> xa powr (x - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {real 0..real m} \<Longrightarrow> real (nat \<lfloor>xa\<rfloor>) powr (x - 1) \<le> xa powr (x - 1)
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {real 0..real m} \<Longrightarrow> real (nat \<lfloor>xa\<rfloor>) powr (x - 1) \<le> xa powr (x - 1)
[PROOF STEP]
assume "t \<in> {real 0..real m}"
[PROOF STATE]
proof (state)
this:
t \<in> {real 0..real m}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {real 0..real m} \<Longrightarrow> real (nat \<lfloor>xa\<rfloor>) powr (x - 1) \<le> xa powr (x - 1)
[PROOF STEP]
with \<open>x > 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 < x
t \<in> {real 0..real m}
[PROOF STEP]
show "real (nat \<lfloor>t\<rfloor>) powr (x - 1) \<le> t powr (x - 1)"
[PROOF STATE]
proof (prove)
using this:
1 < x
t \<in> {real 0..real m}

goal (1 subgoal):
 1. real (nat \<lfloor>t\<rfloor>) powr (x - 1) \<le> t powr (x - 1)
[PROOF STEP]
by (cases "t = 0") (auto intro: powr_mono2)
[PROOF STATE]
proof (state)
this:
real (nat \<lfloor>t\<rfloor>) powr (x - 1) \<le> t powr (x - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 0..<m. real n powr (x - 1)) \<le> real m powr x / x

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 0..<m. real n powr (x - 1)) \<le> real m powr x / x

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
have "m powr (x - 1) + m powr x / x = m powr x * (1 / x + 1 / m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real m powr (x - 1) + real m powr x / x = real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
using m x
[PROOF STATE]
proof (prove)
using this:
0 < m
0 < x

goal (1 subgoal):
 1. real m powr (x - 1) + real m powr x / x = real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
by (simp add: powr_diff field_simps)
[PROOF STATE]
proof (state)
this:
real m powr (x - 1) + real m powr x / x = real m powr x * (1 / x + 1 / real m)

goal (1 subgoal):
 1. 1 < x \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> real m powr (x - 1) + xa \<le> real m powr (x - 1) + y) \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> real m powr (x - 1) + xa \<le> real m powr (x - 1) + y) \<Longrightarrow> (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)

goal (1 subgoal):
 1. (\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>n = 1..m. real n powr (x - 1)) \<le> real m powr x * (1 / x + 1 / real m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma natfun_bigo_1E:
  assumes "(f :: nat \<Rightarrow> _) \<in> O(\<lambda>_. 1)"
  obtains C where "C \<ge> lb" "\<And>n. norm (f n) \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>lb \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>C. \<lbrakk>lb \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f \<in> O(\<lambda>_. 1::'a)
[PROOF STEP]
obtain C N where "\<forall>n\<ge>N. norm (f n) \<le> C"
[PROOF STATE]
proof (prove)
using this:
f \<in> O(\<lambda>_. 1::'a)

goal (1 subgoal):
 1. (\<And>N C. \<forall>n\<ge>N. norm (f n) \<le> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: landau_o.bigE simp: eventually_at_top_linorder)
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. norm (f n) \<le> C

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>lb \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence *: "norm (f n) \<le> Max ({C, lb} \<union> (norm ` f ` {..<N}))" for n
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. norm (f n) \<le> C

goal (1 subgoal):
 1. norm (f n) \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
[PROOF STEP]
by (cases "n \<ge> N") (subst Max_ge_iff; force simp: image_iff)+
[PROOF STATE]
proof (state)
this:
norm (f ?n) \<le> Max ({C, lb} \<union> norm ` f ` {..<N})

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>lb \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm (f ?n) \<le> Max ({C, lb} \<union> norm ` f ` {..<N})

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>lb \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "Max ({C, lb} \<union> (norm ` f ` {..<N})) \<ge> lb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lb \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
[PROOF STEP]
by (intro Max.coboundedI) auto
[PROOF STATE]
proof (state)
this:
lb \<le> Max ({C, lb} \<union> norm ` f ` {..<N})

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>lb \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm (f ?n) \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
lb \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (f ?n) \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
lb \<le> Max ({C, lb} \<union> norm ` f ` {..<N})

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
norm (f ?n) \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
lb \<le> Max ({C, lb} \<union> norm ` f ` {..<N})
\<lbrakk>lb \<le> ?C; \<And>n. norm (f n) \<le> ?C\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma natfun_bigo_iff_Bseq: "f \<in> O(\<lambda>_. 1) \<longleftrightarrow> Bseq f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> O(\<lambda>_. 1::'a)) = Bseq f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
 2. Bseq f \<Longrightarrow> f \<in> O(\<lambda>_. 1::'a)
[PROOF STEP]
assume "Bseq f"
[PROOF STATE]
proof (state)
this:
Bseq f

goal (2 subgoals):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
 2. Bseq f \<Longrightarrow> f \<in> O(\<lambda>_. 1::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bseq f
[PROOF STEP]
obtain C where "C > 0" "\<And>n. norm (f n) \<le> C"
[PROOF STATE]
proof (prove)
using this:
Bseq f

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>0 < C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Bseq_def)
[PROOF STATE]
proof (state)
this:
0 < C
norm (f ?n) \<le> C

goal (2 subgoals):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
 2. Bseq f \<Longrightarrow> f \<in> O(\<lambda>_. 1::'a)
[PROOF STEP]
thus "f \<in> O(\<lambda>_. 1)"
[PROOF STATE]
proof (prove)
using this:
0 < C
norm (f ?n) \<le> C

goal (1 subgoal):
 1. f \<in> O(\<lambda>_. 1::'a)
[PROOF STEP]
by (intro bigoI[of _ C]) auto
[PROOF STATE]
proof (state)
this:
f \<in> O(\<lambda>_. 1::'a)

goal (1 subgoal):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
[PROOF STEP]
assume "f \<in> O(\<lambda>_. 1)"
[PROOF STATE]
proof (state)
this:
f \<in> O(\<lambda>_. 1::'a)

goal (1 subgoal):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
[PROOF STEP]
from natfun_bigo_1E[OF this, where lb = 1]
[PROOF STATE]
proof (chain)
picking this:
(\<And>C. \<lbrakk>1 \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain C where "C \<ge> 1" "\<And>n. norm (f n) \<le> C"
[PROOF STATE]
proof (prove)
using this:
(\<And>C. \<lbrakk>1 \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>1 \<le> C; \<And>n. norm (f n) \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> C
norm (f ?n) \<le> C

goal (1 subgoal):
 1. f \<in> O(\<lambda>_. 1::'a) \<Longrightarrow> Bseq f
[PROOF STEP]
thus "Bseq f"
[PROOF STATE]
proof (prove)
using this:
1 \<le> C
norm (f ?n) \<le> C

goal (1 subgoal):
 1. Bseq f
[PROOF STEP]
by (auto simp: Bseq_def intro!: exI[of _ C])
[PROOF STATE]
proof (state)
this:
Bseq f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enn_decreasing_sum_le_set_nn_integral:
  fixes f :: "real \<Rightarrow> ennreal"
  assumes decreasing: "\<And>x y. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> f y \<le> f x"
  shows "(\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
have "(\<Sum>n. (f (Suc n))) =
          (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. (f (Suc n)) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (Suc n))\<partial>lborel)
[PROOF STEP]
by (subst nn_integral_cmult_indicator) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. f (real (Suc n))) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (Suc n))\<partial>lborel)

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. f (real (Suc n))) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (Suc n))\<partial>lborel)

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
have "nat \<lceil>x\<rceil> = Suc n" if "x \<in> {real n<..real (Suc n)}" for x n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>x\<rceil> = Suc n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> {real n<..real (Suc n)}

goal (1 subgoal):
 1. nat \<lceil>x\<rceil> = Suc n
[PROOF STEP]
by (auto simp: nat_eq_iff ceiling_eq_iff)
[PROOF STATE]
proof (state)
this:
?x \<in> {real ?n<..real (Suc ?n)} \<Longrightarrow> nat \<lceil>?x\<rceil> = Suc ?n

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
hence "(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. (f (Suc n)) \<partial>lborel) =
          (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. (f (real (nat \<lceil>x\<rceil>))) \<partial>lborel)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {real ?n<..real (Suc ?n)} \<Longrightarrow> nat \<lceil>?x\<rceil> = Suc ?n

goal (1 subgoal):
 1. (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (Suc n))\<partial>lborel) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (nat \<lceil>x\<rceil>))\<partial>lborel)
[PROOF STEP]
by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (Suc n))\<partial>lborel) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (nat \<lceil>x\<rceil>))\<partial>lborel)

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (Suc n))\<partial>lborel) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (nat \<lceil>x\<rceil>))\<partial>lborel)

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). (f (nat \<lceil>x::real\<rceil>)) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (nat \<lceil>x\<rceil>))\<partial>lborel) = \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). f (real (nat \<lceil>x\<rceil>))\<partial>lborel
[PROOF STEP]
by (subst nn_integral_disjoint_family)
       (auto simp: disjoint_family_on_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (nat \<lceil>x\<rceil>))\<partial>lborel) = \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). f (real (nat \<lceil>x\<rceil>))\<partial>lborel

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. f (real (nat \<lceil>x\<rceil>))\<partial>lborel) = \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). f (real (nat \<lceil>x\<rceil>))\<partial>lborel

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
have "\<dots> \<le> (\<integral>\<^sup>+x\<in>{0..}. (f x) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). f (real (nat \<lceil>x\<rceil>))\<partial>lborel \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
by (intro nn_integral_mono) (auto simp: indicator_def intro!: decreasing)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). f (real (nat \<lceil>x\<rceil>))\<partial>lborel \<le> set_nn_integral lborel {0..} f

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>n. f (real (Suc n))) \<le> set_nn_integral lborel {0..} f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nn_integral_has_integral_lebesgue:
  fixes f :: "'a::euclidean_space \<Rightarrow> real"
  assumes nonneg: "\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
  shows "integral\<^sup>N lborel (\<lambda>x. indicator \<Omega> x * f x) = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
from I
[PROOF STATE]
proof (chain)
picking this:
(f has_integral I) \<Omega>
[PROOF STEP]
have "(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> lebesgue \<rightarrow>\<^sub>M borel"
[PROOF STATE]
proof (prove)
using this:
(f has_integral I) \<Omega>

goal (1 subgoal):
 1. (\<lambda>x. indicat_real \<Omega> x *\<^sub>R f x) \<in> borel_measurable lebesgue
[PROOF STEP]
by (rule has_integral_implies_lebesgue_measurable)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. indicat_real \<Omega> x *\<^sub>R f x) \<in> borel_measurable lebesgue

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. indicat_real \<Omega> x *\<^sub>R f x) \<in> borel_measurable lebesgue
[PROOF STEP]
obtain f' :: "'a \<Rightarrow> real"
    where [measurable]: "f' \<in> borel \<rightarrow>\<^sub>M borel" and eq: "AE x in lborel. indicator \<Omega> x * f x = f' x"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. indicat_real \<Omega> x *\<^sub>R f x) \<in> borel_measurable lebesgue

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> borel_measurable borel; AE x in lborel. indicat_real \<Omega> x * f x = f' x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: completion_ex_borel_measurable_real)
[PROOF STATE]
proof (state)
this:
f' \<in> borel_measurable borel
AE x in lborel. indicat_real \<Omega> x * f x = f' x

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
from I
[PROOF STATE]
proof (chain)
picking this:
(f has_integral I) \<Omega>
[PROOF STEP]
have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV"
[PROOF STATE]
proof (prove)
using this:
(f has_integral I) \<Omega>

goal (1 subgoal):
 1. ((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV
[PROOF STEP]
using nonneg
[PROOF STATE]
proof (prove)
using this:
(f has_integral I) \<Omega>
?x \<in> \<Omega> \<Longrightarrow> 0 \<le> f ?x

goal (1 subgoal):
 1. ((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV
[PROOF STEP]
by (simp add: indicator_def of_bool_def if_distrib[of "\<lambda>x. x * f y" for y] cong: if_cong)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
have "((\<lambda>x. abs (indicator \<Omega> x * f x)) has_integral I) UNIV \<longleftrightarrow> ((\<lambda>x. abs (f' x)) has_integral I) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV = ((\<lambda>x. \<bar>f' x\<bar>) has_integral I) UNIV
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
AE x in lborel. indicat_real \<Omega> x * f x = f' x

goal (1 subgoal):
 1. ((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV = ((\<lambda>x. \<bar>f' x\<bar>) has_integral I) UNIV
[PROOF STEP]
by (intro has_integral_AE) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) has_integral I) UNIV = ((\<lambda>x. \<bar>f' x\<bar>) has_integral I) UNIV

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<bar>f' x\<bar>) has_integral I) UNIV
[PROOF STEP]
have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = I"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<bar>f' x\<bar>) has_integral I) UNIV

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = ennreal I
[PROOF STEP]
by (rule nn_integral_has_integral_lborel[rotated 2]) auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = ennreal I

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = ennreal I

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = integral\<^sup>N lborel (\<lambda>x. abs (indicator \<Omega> x * f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = \<integral>\<^sup>+ x. ennreal \<bar>indicat_real \<Omega> x * f x\<bar> \<partial>lborel
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
AE x in lborel. indicat_real \<Omega> x * f x = f' x

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = \<integral>\<^sup>+ x. ennreal \<bar>indicat_real \<Omega> x * f x\<bar> \<partial>lborel
[PROOF STEP]
by (intro nn_integral_cong_AE) auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = \<integral>\<^sup>+ x. ennreal \<bar>indicat_real \<Omega> x * f x\<bar> \<partial>lborel

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal \<bar>f' x\<bar> \<partial>lborel = \<integral>\<^sup>+ x. ennreal \<bar>indicat_real \<Omega> x * f x\<bar> \<partial>lborel

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
have "(\<lambda>x. abs (indicator \<Omega> x * f x)) = (\<lambda>x. indicator \<Omega> x * f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) = (\<lambda>x. indicat_real \<Omega> x * f x)
[PROOF STEP]
using nonneg
[PROOF STATE]
proof (prove)
using this:
?x \<in> \<Omega> \<Longrightarrow> 0 \<le> f ?x

goal (1 subgoal):
 1. (\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) = (\<lambda>x. indicat_real \<Omega> x * f x)
[PROOF STEP]
by (auto simp: indicator_def fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<bar>indicat_real \<Omega> x * f x\<bar>) = (\<lambda>x. indicat_real \<Omega> x * f x)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (indicat_real \<Omega> x * f x) \<partial>lborel = ennreal I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decreasing_sum_le_integral:
  fixes f :: "real \<Rightarrow> real"
  assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
  assumes decreasing: "\<And>x y. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> f y \<le> f x"
  assumes integral: "(f has_integral I) {0..}"
  shows   "summable (\<lambda>i. f (real (Suc i)))" and "suminf (\<lambda>i. f (real (Suc i))) \<le> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>i. f (real (Suc i))) &&& (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have [simp]: "I \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> I
[PROOF STEP]
by (intro has_integral_nonneg[OF integral] nonneg) auto
[PROOF STATE]
proof (state)
this:
0 \<le> I

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have "(\<Sum>n. ennreal (f (Suc n))) =
          (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (Suc n)) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. ennreal (f (real (Suc n)))) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (Suc n)))\<partial>lborel)
[PROOF STEP]
by (subst nn_integral_cmult_indicator) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ennreal (f (real (Suc n)))) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (Suc n)))\<partial>lborel)

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ennreal (f (real (Suc n)))) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (Suc n)))\<partial>lborel)

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have "nat \<lceil>x\<rceil> = Suc n" if "x \<in> {real n<..real (Suc n)}" for x n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>x\<rceil> = Suc n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> {real n<..real (Suc n)}

goal (1 subgoal):
 1. nat \<lceil>x\<rceil> = Suc n
[PROOF STEP]
by (auto simp: nat_eq_iff ceiling_eq_iff)
[PROOF STATE]
proof (state)
this:
?x \<in> {real ?n<..real (Suc ?n)} \<Longrightarrow> nat \<lceil>?x\<rceil> = Suc ?n

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
hence "(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (Suc n)) \<partial>lborel) =
          (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>))) \<partial>lborel)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {real ?n<..real (Suc ?n)} \<Longrightarrow> nat \<lceil>?x\<rceil> = Suc ?n

goal (1 subgoal):
 1. (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (Suc n)))\<partial>lborel) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel)
[PROOF STEP]
by (intro suminf_cong nn_integral_cong) (auto simp: indicator_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (Suc n)))\<partial>lborel) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel)

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (Suc n)))\<partial>lborel) = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel)

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (nat \<lceil>x::real\<rceil>)) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel) = \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel
[PROOF STEP]
by (subst nn_integral_disjoint_family)
       (auto simp: disjoint_family_on_def intro!: measurable_completion)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel) = \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<integral>\<^sup>+x\<in>{real n<..real (Suc n)}. ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel) = \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have "\<dots> \<le> (\<integral>\<^sup>+x\<in>{0..}. ennreal (f x) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel \<le> \<integral>\<^sup>+x\<in>{0..}. ennreal (f x)\<partial>lborel
[PROOF STEP]
by (intro nn_integral_mono) (auto simp: indicator_def nonneg intro!: decreasing)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel \<le> \<integral>\<^sup>+x\<in>{0..}. ennreal (f x)\<partial>lborel

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>(\<Union>i. {real i<..real (Suc i)}). ennreal (f (real (nat \<lceil>x\<rceil>)))\<partial>lborel \<le> \<integral>\<^sup>+x\<in>{0..}. ennreal (f x)\<partial>lborel

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>{0..}. ennreal (f x)\<partial>lborel = \<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel
[PROOF STEP]
by (intro nn_integral_cong) (auto simp: indicator_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>{0..}. ennreal (f x)\<partial>lborel = \<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>{0..}. ennreal (f x)\<partial>lborel = \<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
have "\<dots> = ennreal I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
using nn_integral_has_integral_lebesgue[OF nonneg integral]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> {0..} \<Longrightarrow> 0 \<le> x) \<Longrightarrow> \<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel = ennreal I

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel = ennreal I
[PROOF STEP]
by (auto simp: nonneg)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (indicat_real {0..} x * f x) \<partial>lborel = ennreal I

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I
[PROOF STEP]
have *: "(\<Sum>n. ennreal (f (Suc n))) \<le> ennreal I"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I

goal (1 subgoal):
 1. (\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I

goal (2 subgoals):
 1. summable (\<lambda>i. f (real (Suc i)))
 2. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I
[PROOF STEP]
show summable: "summable (\<lambda>i. f (real (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I

goal (1 subgoal):
 1. summable (\<lambda>i. f (real (Suc i)))
[PROOF STEP]
by (intro summable_suminf_not_top) (auto simp: top_unique intro: nonneg)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>i. f (real (Suc i)))

goal (1 subgoal):
 1. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
note *
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I

goal (1 subgoal):
 1. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ennreal (f (real (Suc n)))) \<le> ennreal I

goal (1 subgoal):
 1. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
from summable
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>i. f (real (Suc i)))
[PROOF STEP]
have "(\<Sum>n. ennreal (f (Suc n))) = ennreal (\<Sum>n. f (Suc n))"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>i. f (real (Suc i)))

goal (1 subgoal):
 1. (\<Sum>n. ennreal (f (real (Suc n)))) = ennreal (\<Sum>n. f (real (Suc n)))
[PROOF STEP]
by (subst suminf_ennreal2) (auto simp: o_def nonneg)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. ennreal (f (real (Suc n)))) = ennreal (\<Sum>n. f (real (Suc n)))

goal (1 subgoal):
 1. (\<Sum>i. f (real (Suc i))) \<le> I
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (\<Sum>n. f (real (Suc n))) \<le> ennreal I
[PROOF STEP]
show "(\<Sum>n. f (real (Suc n))) \<le> I"
[PROOF STATE]
proof (prove)
using this:
ennreal (\<Sum>n. f (real (Suc n))) \<le> ennreal I

goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> I
[PROOF STEP]
by (subst (asm) ennreal_le_iff) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. f (real (Suc n))) \<le> I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma decreasing_sum_le_integral':
  fixes f :: "real \<Rightarrow> real"
  assumes "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
  assumes "\<And>x y. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> f y \<le> f x"
  assumes "(f has_integral I) {0..}"
  shows   "summable (\<lambda>i. f (real i))" and "suminf (\<lambda>i. f (real i)) \<le> f 0 + I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>i. f (real i)) &&& (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>i. f (real i))
 2. (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
have "summable ((\<lambda>i. f (real (Suc i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>i. f (real (Suc i)))
[PROOF STEP]
using decreasing_sum_le_integral[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> x; \<And>x y. \<lbrakk>0 \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> 0 \<le> x; \<And>x y. \<lbrakk>0 \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> summable (\<lambda>i. f (real (Suc i)))
\<lbrakk>\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> x; \<And>x y. \<lbrakk>0 \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> 0 \<le> x; \<And>x y. \<lbrakk>0 \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> x \<le> y\<rbrakk> \<Longrightarrow> (\<Sum>i. f (real (Suc i))) \<le> I

goal (1 subgoal):
 1. summable (\<lambda>i. f (real (Suc i)))
[PROOF STEP]
by (simp add: o_def)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>i. f (real (Suc i)))

goal (2 subgoals):
 1. summable (\<lambda>i. f (real i))
 2. (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
thus *: "summable (\<lambda>i. f (real i))"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>i. f (real (Suc i)))

goal (1 subgoal):
 1. summable (\<lambda>i. f (real i))
[PROOF STEP]
by (subst (asm) summable_Suc_iff)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>i. f (real i))

goal (1 subgoal):
 1. (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
have "(\<Sum>n. f (real (Suc n))) \<le> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. f (real (Suc n))) \<le> I
[PROOF STEP]
by (intro decreasing_sum_le_integral assms)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. f (real (Suc n))) \<le> I

goal (1 subgoal):
 1. (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
thus "suminf (\<lambda>i. f (real i)) \<le> f 0 + I"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. f (real (Suc n))) \<le> I

goal (1 subgoal):
 1. (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. f (real (Suc n))) \<le> I
summable (\<lambda>i. f (real i))

goal (1 subgoal):
 1. (\<Sum>i. f (real i)) \<le> f 0 + I
[PROOF STEP]
by (subst (asm) suminf_split_head) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i. f (real i)) \<le> f 0 + I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma norm_suminf_le:
  assumes "\<And>n. norm (f n :: 'a :: banach) \<le> g n" "summable g"
  shows   "norm (suminf f) \<le> suminf g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
have *: "summable (\<lambda>n. norm (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. norm (f n))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
norm (f ?n) \<le> g ?n
summable g

goal (1 subgoal):
 1. summable (\<lambda>n. norm (f n))
[PROOF STEP]
by (intro summable_norm summable_comparison_test[OF _ assms(2)] exI[of _ 0]) auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. norm (f n))

goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
hence "norm (suminf f) \<le> (\<Sum>n. norm (f n))"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. norm (f n))

goal (1 subgoal):
 1. norm (suminf f) \<le> (\<Sum>n. norm (f n))
[PROOF STEP]
by (intro summable_norm) auto
[PROOF STATE]
proof (state)
this:
norm (suminf f) \<le> (\<Sum>n. norm (f n))

goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (suminf f) \<le> (\<Sum>n. norm (f n))

goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
have "\<dots> \<le> suminf g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. norm (f n)) \<le> suminf g
[PROOF STEP]
by (intro suminf_le * assms allI)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. norm (f n)) \<le> suminf g

goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (suminf f) \<le> suminf g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (suminf f) \<le> suminf g

goal (1 subgoal):
 1. norm (suminf f) \<le> suminf g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm (suminf f) \<le> suminf g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_nat_powr_neq_1_complex [simp]:
  assumes "n > 1" "Re s \<noteq> 0"
  shows   "of_nat n powr s \<noteq> (1::complex)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n powr s \<noteq> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_nat n powr s \<noteq> 1
[PROOF STEP]
have "norm (of_nat n powr s) = real n powr Re s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (of_nat n powr s) = real n powr Re s
[PROOF STEP]
by (simp add: norm_powr_real_powr)
[PROOF STATE]
proof (state)
this:
cmod (of_nat n powr s) = real n powr Re s

goal (1 subgoal):
 1. of_nat n powr s \<noteq> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (of_nat n powr s) = real n powr Re s

goal (1 subgoal):
 1. of_nat n powr s \<noteq> 1
[PROOF STEP]
have "\<dots> \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n powr Re s \<noteq> 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < n
Re s \<noteq> 0

goal (1 subgoal):
 1. real n powr Re s \<noteq> 1
[PROOF STEP]
by (auto simp: powr_def)
[PROOF STATE]
proof (state)
this:
real n powr Re s \<noteq> 1

goal (1 subgoal):
 1. of_nat n powr s \<noteq> 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (of_nat n powr s) \<noteq> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (of_nat n powr s) \<noteq> 1

goal (1 subgoal):
 1. of_nat n powr s \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat n powr s \<noteq> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_summable_on_uminus_iff:
  "(\<lambda>x. -f x) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. - f x) abs_summable_on A) = (f abs_summable_on A)
[PROOF STEP]
using abs_summable_on_uminus[of f A] abs_summable_on_uminus[of "\<lambda>x. -f x" A]
[PROOF STATE]
proof (prove)
using this:
f abs_summable_on A \<Longrightarrow> (\<lambda>x. - f x) abs_summable_on A
(\<lambda>x. - f x) abs_summable_on A \<Longrightarrow> (\<lambda>x. - (- f x)) abs_summable_on A

goal (1 subgoal):
 1. ((\<lambda>x. - f x) abs_summable_on A) = (f abs_summable_on A)
[PROOF STEP]
by auto


[STATEMENT]
lemma abs_summable_on_cmult_right_iff:
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_field, second_countable_topology}"
  assumes "c \<noteq> 0"
  shows   "(\<lambda>x. c * f x) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. c * f x) abs_summable_on A) = (f abs_summable_on A)
[PROOF STEP]
using assms abs_summable_on_cmult_right[of c f A]
        abs_summable_on_cmult_right[of "inverse c" "\<lambda>x. c * f x" A]
[PROOF STATE]
proof (prove)
using this:
c \<noteq> (0::'b)
(c \<noteq> (0::'b) \<Longrightarrow> f abs_summable_on A) \<Longrightarrow> (\<lambda>x. c * f x) abs_summable_on A
(inverse c \<noteq> (0::'b) \<Longrightarrow> (\<lambda>x. c * f x) abs_summable_on A) \<Longrightarrow> (\<lambda>x. inverse c * (c * f x)) abs_summable_on A

goal (1 subgoal):
 1. ((\<lambda>x. c * f x) abs_summable_on A) = (f abs_summable_on A)
[PROOF STEP]
by (auto simp: field_simps)


[STATEMENT]
lemma abs_summable_on_cmult_left_iff:
  fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_field, second_countable_topology}"
  assumes "c \<noteq> 0"
  shows   "(\<lambda>x. f x * c) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f x * c) abs_summable_on A) = (f abs_summable_on A)
[PROOF STEP]
using assms abs_summable_on_cmult_left[of c f A]
        abs_summable_on_cmult_left[of "inverse c" "\<lambda>x. f x * c" A]
[PROOF STATE]
proof (prove)
using this:
c \<noteq> (0::'b)
(c \<noteq> (0::'b) \<Longrightarrow> f abs_summable_on A) \<Longrightarrow> (\<lambda>x. f x * c) abs_summable_on A
(inverse c \<noteq> (0::'b) \<Longrightarrow> (\<lambda>x. f x * c) abs_summable_on A) \<Longrightarrow> (\<lambda>x. f x * c * inverse c) abs_summable_on A

goal (1 subgoal):
 1. ((\<lambda>x. f x * c) abs_summable_on A) = (f abs_summable_on A)
[PROOF STEP]
by (auto simp: field_simps)


[STATEMENT]
lemma fds_logderiv_completely_multiplicative:
  fixes f :: "'a :: {real_normed_field} fds"
  assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 \<noteq> 0"
  shows   "fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
have "fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f
[PROOF STEP]
using completely_multiplicative_fds_deriv[of "fds_nth f"] assms
[PROOF STATE]
proof (prove)
using this:
completely_multiplicative_function (fds_nth f) \<Longrightarrow> fds_deriv (fds (fds_nth f)) = - fds (\<lambda>n. fds_nth f n * mangoldt n) * fds (fds_nth f)
completely_multiplicative_function (fds_nth f)
fds_nth f 1 \<noteq> (0::'a)

goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f

goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f

goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
have "\<dots> = - fds (\<lambda>n. fds_nth f n * mangoldt n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
completely_multiplicative_function (fds_nth f)
fds_nth f 1 \<noteq> (0::'a)

goal (1 subgoal):
 1. - fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
by (simp add: divide_fds_def fds_right_inverse)
[PROOF STATE]
proof (state)
this:
- fds (\<lambda>n. fds_nth f n * mangoldt n) * f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)

goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)

goal (1 subgoal):
 1. fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fds_deriv f / f = - fds (\<lambda>n. fds_nth f n * mangoldt n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_nth_logderiv_completely_multiplicative:
  fixes f :: "'a :: {real_normed_field} fds"
  assumes "completely_multiplicative_function (fds_nth f)" "fds_nth f 1 \<noteq> 0"
  shows   "fds_nth (fds_deriv f / f) n = -fds_nth f n * mangoldt n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_nth (fds_deriv f / f) n = - fds_nth f n * mangoldt n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
completely_multiplicative_function (fds_nth f)
fds_nth f 1 \<noteq> (0::'a)

goal (1 subgoal):
 1. fds_nth (fds_deriv f / f) n = - fds_nth f n * mangoldt n
[PROOF STEP]
by (subst fds_logderiv_completely_multiplicative) (simp_all add: fds_nth_fds')


[STATEMENT]
lemma eval_fds_logderiv_completely_multiplicative:
  fixes s :: "'a :: dirichlet_series" and l :: 'a and f :: "'a fds"
  defines "h \<equiv> fds_deriv f / f"
  assumes "completely_multiplicative_function (fds_nth f)" and [simp]: "fds_nth f 1 \<noteq> 0"
  assumes "s \<bullet> 1 > abs_conv_abscissa f"
  shows  "(\<lambda>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 = -(\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) *
                            (1 / (1 - fds_nth f p / nat_power p s) - 1))" (is ?th2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p} &&& eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
let ?P = "{p::nat. prime p}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
interpret f: completely_multiplicative_function "fds_nth f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth f)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "fds_abs_converges h s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges h s
[PROOF STEP]
using abs_conv_abscissa_completely_multiplicative_log_deriv[OF assms(2)] assms
[PROOF STATE]
proof (prove)
using this:
fds_nth f 1 \<noteq> (0::'a) \<Longrightarrow> abs_conv_abscissa (fds_deriv f / f) \<le> abs_conv_abscissa f
h \<equiv> fds_deriv f / f
completely_multiplicative_function (fds_nth f)
fds_nth f 1 \<noteq> (0::'a)
abs_conv_abscissa f < ereal (s \<bullet> (1::'a))

goal (1 subgoal):
 1. fds_abs_converges h s
[PROOF STEP]
by (intro fds_abs_converges) auto
[PROOF STATE]
proof (state)
this:
fds_abs_converges h s

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
hence *: "(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV"
[PROOF STATE]
proof (prove)
using this:
fds_abs_converges h s

goal (1 subgoal):
 1. (\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV
[PROOF STEP]
by (auto simp: h_def fds_abs_converges_altdef')
[PROOF STATE]
proof (state)
this:
(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
note *
[PROOF STATE]
proof (state)
this:
(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV \<longleftrightarrow>
          (\<lambda>x. -fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV) = ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow)
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>n. fds_nth (fds_deriv f / f) n / nat_power n s) abs_summable_on UNIV) = ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow)
[PROOF STEP]
using fds_nth_logderiv_completely_multiplicative[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
fds_nth f 1 \<noteq> (0::'a) \<Longrightarrow> fds_nth (fds_deriv f / f) ?n = - fds_nth f ?n * mangoldt ?n

goal (1 subgoal):
 1. ((\<lambda>n. fds_nth (fds_deriv f / f) n / nat_power n s) abs_summable_on UNIV) = ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow)
[PROOF STEP]
by (intro abs_summable_on_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV) = ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow)

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow
[PROOF STEP]
have sum1: "(\<lambda>x. -fds_nth f x * mangoldt x / nat_power x s)
                      abs_summable_on Collect primepow"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow

goal (1 subgoal):
 1. (\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow
[PROOF STEP]
by (rule abs_summable_on_subset) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "?this \<longleftrightarrow> (\<lambda>(p,k). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) /
                                nat_power (p ^ Suc k) s) abs_summable_on (?P \<times> UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow) = ((\<lambda>(p, k). - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on {p. prime p} \<times> UNIV)
[PROOF STEP]
using bij_betw_primepows
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>(p, k). p ^ Suc k) (Collect prime \<times> UNIV) (Collect primepow)

goal (1 subgoal):
 1. ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow) = ((\<lambda>(p, k). - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on {p. prime p} \<times> UNIV)
[PROOF STEP]
unfolding case_prod_unfold
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>p. fst p ^ Suc (snd p)) (Collect prime \<times> UNIV) (Collect primepow)

goal (1 subgoal):
 1. ((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow) = ((\<lambda>p. - fds_nth f (fst p ^ Suc (snd p)) * mangoldt (fst p ^ Suc (snd p)) / nat_power (fst p ^ Suc (snd p)) s) abs_summable_on {p. prime p} \<times> UNIV)
[PROOF STEP]
by (intro abs_summable_on_reindex_bij_betw [symmetric])
[PROOF STATE]
proof (state)
this:
((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow) = ((\<lambda>(p, k). - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on {p. prime p} \<times> UNIV)

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. - fds_nth f x * mangoldt x / nat_power x s) abs_summable_on Collect primepow) = ((\<lambda>(p, k). - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on {p. prime p} \<times> UNIV)

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<lambda>(p,k). -((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p))))
                abs_summable_on (?P \<times> UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>(p, k). - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on {p. prime p} \<times> UNIV) = ((\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV)
[PROOF STEP]
unfolding case_prod_unfold
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>p. - fds_nth f (fst p ^ Suc (snd p)) * mangoldt (fst p ^ Suc (snd p)) / nat_power (fst p ^ Suc (snd p)) s) abs_summable_on {p. prime p} \<times> UNIV) = ((\<lambda>p. - ((fds_nth f (fst p) / nat_power (fst p) s) ^ Suc (snd p) * of_real (ln (real (fst p))))) abs_summable_on {p. prime p} \<times> UNIV)
[PROOF STEP]
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)
[PROOF STATE]
proof (state)
this:
((\<lambda>(p, k). - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) abs_summable_on {p. prime p} \<times> UNIV) = ((\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV)

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV
[PROOF STEP]
have sum2: \<dots>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV

goal (1 subgoal):
 1. (\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have sum4: "summable (\<lambda>n. (norm (fds_nth f p / nat_power p s)) ^ Suc n)" if p: "prime p" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
have "summable (\<lambda>n. \<bar>ln (real p)\<bar> * (norm (fds_nth f p / nat_power p s)) ^ Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>ln (real p)\<bar> * norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
using p abs_summable_on_Sigma_project2[OF sum2, of p]
[PROOF STATE]
proof (prove)
using this:
prime p
p \<in> {p. prime p} \<Longrightarrow> (\<lambda>y. case (p, y) of (p, k) \<Rightarrow> - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on UNIV

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>ln (real p)\<bar> * norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
unfolding abs_summable_on_nat_iff'
[PROOF STATE]
proof (prove)
using this:
prime p
p \<in> {p. prime p} \<Longrightarrow> summable (\<lambda>n. norm (case (p, n) of (p, k) \<Rightarrow> - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))))

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>ln (real p)\<bar> * norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
by (simp add: norm_power norm_mult norm_divide mult_ac del: power_Suc)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>ln (real p)\<bar> * norm (fds_nth f p / nat_power p s) ^ Suc n)

goal (1 subgoal):
 1. summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>ln (real p)\<bar> * norm (fds_nth f p / nat_power p s) ^ Suc n)

goal (1 subgoal):
 1. summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
by (rule summable_mult_D) (insert p, auto dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime ?p \<Longrightarrow> summable (\<lambda>n. norm (fds_nth f ?p / nat_power ?p s) ^ Suc n)

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have sums: "(\<lambda>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 STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (fds_nth f p / nat_power p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (fds_nth f p / nat_power p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))
[PROOF STEP]
from sum4[OF p]
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
[PROOF STEP]
have "norm (fds_nth f p / nat_power p s) < 1"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)

goal (1 subgoal):
 1. norm (fds_nth f p / nat_power p s) < 1
[PROOF STEP]
unfolding summable_Suc_iff
[PROOF STATE]
proof (prove)
using this:
summable ((^) (norm (fds_nth f p / nat_power p s)))

goal (1 subgoal):
 1. norm (fds_nth f p / nat_power p s) < 1
[PROOF STEP]
by (simp add: summable_geometric_iff)
[PROOF STATE]
proof (state)
this:
norm (fds_nth f p / nat_power p s) < 1

goal (1 subgoal):
 1. (\<lambda>n. (fds_nth f p / nat_power p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))
[PROOF STEP]
from geometric_sums[OF this]
[PROOF STATE]
proof (chain)
picking this:
(^) (fds_nth f p / nat_power p s) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(^) (fds_nth f p / nat_power p s) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s))

goal (1 subgoal):
 1. (\<lambda>n. (fds_nth f p / nat_power p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))
[PROOF STEP]
by (subst sums_Suc_iff) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (fds_nth f p / nat_power p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime ?p \<Longrightarrow> (\<lambda>n. (fds_nth f ?p / nat_power ?p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f ?p / nat_power ?p s) - (1::'a))

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have eq: "(\<Sum>\<^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 STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "(\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) =
             (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (-ln (real p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (- ln (real p))
[PROOF STEP]
using sum4[of p] p
[PROOF STATE]
proof (prove)
using this:
prime p \<Longrightarrow> summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
prime p

goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (- ln (real p))
[PROOF STEP]
by (subst infsetsum_cmult_left [symmetric])
         (auto simp: abs_summable_on_nat_iff' norm_power simp del: power_Suc)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (- ln (real p))

goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) * of_real (- ln (real p))

goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "(\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) =
                 (1 / (1 - fds_nth f p / nat_power p s) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) = (1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)
[PROOF STEP]
using sum4[OF p] sums[OF p]
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. norm (fds_nth f p / nat_power p s) ^ Suc n)
(\<lambda>n. (fds_nth f p / nat_power p s) ^ Suc n) sums ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))

goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) = (1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)
[PROOF STEP]
by (subst infsetsum_nat')
         (auto simp: sums_iff abs_summable_on_nat_iff' norm_power simp del: power_Suc)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>ak. (fds_nth f p / nat_power p s) ^ Suc k) = (1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)

goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)) * of_real (- ln (real p))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)) * of_real (- ln (real p))

goal (1 subgoal):
 1. (\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) = - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prime ?p \<Longrightarrow> (\<Sum>\<^sub>ak. - ((fds_nth f ?p / nat_power ?p s) ^ Suc k * of_real (ln (real ?p)))) = - (of_real (ln (real ?p)) * ((1::'a) / ((1::'a) - fds_nth f ?p / nat_power ?p s) - (1::'a)))

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have sum3: "(\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x))))
                 abs_summable_on {p. prime p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}
[PROOF STEP]
using sum2
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}
[PROOF STEP]
by (rule abs_summable_on_Sigma_project1') auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "?this \<longleftrightarrow> (\<lambda>p. -(of_real (ln (real p)) *
                (1 / (1 - fds_nth f p / nat_power p s) - 1))) abs_summable_on {p. prime p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}) = ((\<lambda>p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))) abs_summable_on {p. prime p})
[PROOF STEP]
by (intro abs_summable_on_cong eq) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}) = ((\<lambda>p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))) abs_summable_on {p. prime p})

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>\<^sub>ay. - ((fds_nth f x / nat_power x s) ^ Suc y * of_real (ln (real x)))) abs_summable_on {p. prime p}) = ((\<lambda>p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))) abs_summable_on {p. prime p})

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?th1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))) abs_summable_on {p. prime p}) = ((\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p})
[PROOF STEP]
by (subst abs_summable_on_uminus_iff) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))) abs_summable_on {p. prime p}) = ((\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p})

goal (2 subgoals):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
 2. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
[PROOF STEP]
show ?th1
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}

goal (1 subgoal):
 1. (\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))) abs_summable_on {p. prime p}

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "eval_fds h s = (\<Sum>\<^sub>an. fds_nth h n / nat_power n s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fds h s = (\<Sum>\<^sub>an. fds_nth h n / nat_power n s)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV

goal (1 subgoal):
 1. eval_fds h s = (\<Sum>\<^sub>an. fds_nth h n / nat_power n s)
[PROOF STEP]
unfolding eval_fds_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. fds_nth h n / nat_power n s) abs_summable_on UNIV

goal (1 subgoal):
 1. (\<Sum>n. fds_nth h n / nat_power n s) = (\<Sum>\<^sub>an. fds_nth h n / nat_power n s)
[PROOF STEP]
by (subst infsetsum_nat') auto
[PROOF STATE]
proof (state)
this:
eval_fds h s = (\<Sum>\<^sub>an. fds_nth h n / nat_power n s)

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_fds h s = (\<Sum>\<^sub>an. fds_nth h n / nat_power n s)

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>an \<in> {n. primepow n}. -fds_nth f n * mangoldt n / nat_power n s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>an. fds_nth h n / nat_power n s) = (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s)
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>an. fds_nth (fds_deriv f / f) n / nat_power n s) = (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s)
[PROOF STEP]
using fds_nth_logderiv_completely_multiplicative[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
fds_nth f 1 \<noteq> (0::'a) \<Longrightarrow> fds_nth (fds_deriv f / f) ?n = - fds_nth f ?n * mangoldt ?n

goal (1 subgoal):
 1. (\<Sum>\<^sub>an. fds_nth (fds_deriv f / f) n / nat_power n s) = (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s)
[PROOF STEP]
by (intro infsetsum_cong_neutral) (auto simp: fds_nth_fds mangoldt_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>an. fds_nth h n / nat_power n s) = (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s)

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>an. fds_nth h n / nat_power n s) = (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s)

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>a(p,k)\<in>(?P \<times> UNIV). -fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) /
                                            nat_power (p ^ Suc k) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s)
[PROOF STEP]
using bij_betw_primepows
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>(p, k). p ^ Suc k) (Collect prime \<times> UNIV) (Collect primepow)

goal (1 subgoal):
 1. (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s)
[PROOF STEP]
unfolding case_prod_unfold
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>p. fst p ^ Suc (snd p)) (Collect prime \<times> UNIV) (Collect primepow)

goal (1 subgoal):
 1. (\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s) = (\<Sum>\<^sub>ap\<in>{p. prime p} \<times> UNIV. - fds_nth f (fst p ^ Suc (snd p)) * mangoldt (fst p ^ Suc (snd p)) / nat_power (fst p ^ Suc (snd p)) s)
[PROOF STEP]
by (intro infsetsum_reindex_bij_betw [symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s)

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>an | primepow n. - fds_nth f n * mangoldt n / nat_power n s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s)

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>a(p,k)\<in>(?P \<times> UNIV).
                     -((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))
[PROOF STEP]
by (intro infsetsum_cong)
       (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)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - fds_nth f (p ^ Suc k) * mangoldt (p ^ Suc k) / nat_power (p ^ Suc k) s) = (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak.
                    - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))
[PROOF STEP]
using sum2
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(p, k). - ((fds_nth f p / nat_power p s) ^ Suc k * of_real (ln (real p)))) abs_summable_on {p. prime p} \<times> UNIV

goal (1 subgoal):
 1. (\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))
[PROOF STEP]
by (subst infsetsum_Times) (auto simp: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>a(p, k)\<in>{p. prime p} \<times> UNIV. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p)))

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
have "\<dots> = (\<Sum>\<^sub>ap | prime p. -(of_real (ln (real p)) *
                    (1 / (1 - fds_nth f p / nat_power p s) - 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))))
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
prime ?p \<Longrightarrow> (\<Sum>\<^sub>ak. - ((fds_nth f ?p / nat_power ?p s) ^ Suc k * of_real (ln (real ?p)))) = - (of_real (ln (real ?p)) * ((1::'a) / ((1::'a) - fds_nth f ?p / nat_power ?p s) - (1::'a)))

goal (1 subgoal):
 1. (\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))))
[PROOF STEP]
by (intro infsetsum_cong) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>ap | prime p. \<Sum>\<^sub>ak. - ((fds_nth f p / nat_power p s) ^ Suc k) * of_real (ln (real p))) = (\<Sum>\<^sub>ap | prime p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))))

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval_fds h s = (\<Sum>\<^sub>ap | prime p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))))
[PROOF STEP]
show ?th2
[PROOF STATE]
proof (prove)
using this:
eval_fds h s = (\<Sum>\<^sub>ap | prime p. - (of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a))))

goal (1 subgoal):
 1. eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))
[PROOF STEP]
by (subst (asm) infsetsum_uminus)
[PROOF STATE]
proof (state)
this:
eval_fds h s = - (\<Sum>\<^sub>ap | prime p. of_real (ln (real p)) * ((1::'a) / ((1::'a) - fds_nth f p / nat_power p s) - (1::'a)))

goal:
No subgoals!
[PROOF STEP]
qed