[STATEMENT]
lemma Lp_bounded_bounded_support:
  assumes [measurable]: "f \<in> borel_measurable M"
      and "AE x in M. \<bar>f x\<bar> \<le> C"
          "emeasure M {x \<in> space M. f x \<noteq> 0} \<noteq> \<infinity>"
  shows "f \<in> space\<^sub>N(\<LL> p M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
proof (cases rule: Lp_cases[of p])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 2. p = 0 \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 3. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
p = 0

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 2. p = 0 \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 3. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 0

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
using L_zero_space assms
[PROOF STATE]
proof (prove)
using this:
p = 0
space\<^sub>N (\<LL> 0 ?M) = borel_measurable ?M
zero_space\<^sub>N (\<LL> 0 ?M) = borel_measurable ?M
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C
emeasure M {x \<in> space M. f x \<noteq> 0} \<noteq> \<infinity>

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M)

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
p = \<infinity>

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
 2. p = \<infinity> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = \<infinity>

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
using L_infinity_space assms
[PROOF STATE]
proof (prove)
using this:
p = \<infinity>
space\<^sub>N (\<LL> \<infinity> ?M) = {f \<in> borel_measurable ?M. \<exists>C. AE x in ?M. \<bar>f x\<bar> \<le> C}
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C
emeasure M {x \<in> space M. f x \<noteq> 0} \<noteq> \<infinity>

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
case (real_pos p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2
0 < p

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
have *: "integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
[PROOF STEP]
apply (rule integrableI_bounded_set[of "{x \<in> space M. f x \<noteq> 0}" _ _ "C powr p2"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {x \<in> space M. f x \<noteq> 0} \<in> sets M
 2. (\<lambda>x. \<bar>f x\<bar> powr p2) \<in> borel_measurable M
 3. emeasure M {x \<in> space M. f x \<noteq> 0} < \<infinity>
 4. AE x\<in>{x \<in> space M. f x \<noteq> 0} in M. norm (\<bar>f x\<bar> powr p2) \<le> C powr p2
 5. AE x in M. x \<notin> {x \<in> space M. f x \<noteq> 0} \<longrightarrow> \<bar>f x\<bar> powr p2 = 0
[PROOF STEP]
using assms powr_mono2[OF less_imp_le[OF \<open>p2 > 0\<close>]]
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C
emeasure M {x \<in> space M. f x \<noteq> 0} \<noteq> \<infinity>
\<lbrakk>0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x powr p2 \<le> ?y powr p2

goal (5 subgoals):
 1. {x \<in> space M. f x \<noteq> 0} \<in> sets M
 2. (\<lambda>x. \<bar>f x\<bar> powr p2) \<in> borel_measurable M
 3. emeasure M {x \<in> space M. f x \<noteq> 0} < \<infinity>
 4. AE x\<in>{x \<in> space M. f x \<noteq> 0} in M. norm (\<bar>f x\<bar> powr p2) \<le> C powr p2
 5. AE x in M. x \<notin> {x \<in> space M. f x \<noteq> 0} \<longrightarrow> \<bar>f x\<bar> powr p2 = 0
[PROOF STEP]
by (auto simp add: top.not_eq_extremum)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)

goal (1 subgoal):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
apply (rule Lp_I[OF \<open>p2 > 0\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f \<in> borel_measurable M
 2. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)

goal (2 subgoals):
 1. f \<in> borel_measurable M
 2. integrable M (\<lambda>x. \<bar>f x\<bar> powr p2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> p M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_AE_limit':
  assumes "g \<in> borel_measurable M"
          "\<And>n. f n \<in> space\<^sub>N (\<LL> p M)"
          "AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
          "(\<lambda>n. Norm (\<LL> p M) (f n)) \<longlonglongrightarrow> l"
  shows "g \<in> space\<^sub>N (\<LL> p M)"
        "Norm (\<LL> p M) g \<le> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> p M) &&& Norm (\<LL> p M) g \<le> l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
have "l \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> l
[PROOF STEP]
by (rule LIMSEQ_le_const[OF \<open>(\<lambda>n. Norm (\<LL> p M) (f n)) \<longlonglongrightarrow> l\<close>], auto)
[PROOF STATE]
proof (state)
this:
0 \<le> l

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
have "(\<lambda>n. eNorm (\<LL> p M) (f n)) \<longlonglongrightarrow> ennreal l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. eNorm (\<LL> p M) (f n)) \<longlonglongrightarrow> ennreal l
[PROOF STEP]
unfolding eNorm_Norm[OF \<open>\<And>n. f n \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ennreal (Norm (\<LL> p M) (f n))) \<longlonglongrightarrow> ennreal l
[PROOF STEP]
using \<open>(\<lambda>n. Norm (\<LL> p M) (f n)) \<longlonglongrightarrow> l\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. Norm (\<LL> p M) (f n)) \<longlonglongrightarrow> l

goal (1 subgoal):
 1. (\<lambda>n. ennreal (Norm (\<LL> p M) (f n))) \<longlonglongrightarrow> ennreal l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. eNorm (\<LL> p M) (f n)) \<longlonglongrightarrow> ennreal l

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. eNorm (\<LL> p M) (f n)) \<longlonglongrightarrow> ennreal l
[PROOF STEP]
have *: "ennreal l = liminf (\<lambda>n. eNorm (\<LL> p M) (f n))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. eNorm (\<LL> p M) (f n)) \<longlonglongrightarrow> ennreal l

goal (1 subgoal):
 1. ennreal l = liminf (\<lambda>n. eNorm (\<LL> p M) (f n))
[PROOF STEP]
using lim_imp_Liminf[symmetric] trivial_limit_sequentially
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. eNorm (\<LL> p M) (f n)) \<longlonglongrightarrow> ennreal l
\<lbrakk>?F \<noteq> \<bottom>; (?f \<longlongrightarrow> ?t) ?F\<rbrakk> \<Longrightarrow> ?t = Liminf ?F ?f
sequentially \<noteq> \<bottom>

goal (1 subgoal):
 1. ennreal l = liminf (\<lambda>n. eNorm (\<LL> p M) (f n))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ennreal l = liminf (\<lambda>n. eNorm (\<LL> p M) (f n))

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
have "eNorm (\<LL> p M) g \<le> ennreal l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) g \<le> ennreal l
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) g \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (f n))
[PROOF STEP]
apply (rule Lp_AE_limit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g \<in> borel_measurable M
 2. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in> borel_measurable M
f ?n \<in> space\<^sub>N (\<LL> p M)
AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
(\<lambda>n. Norm (\<LL> p M) (f n)) \<longlonglongrightarrow> l

goal (2 subgoals):
 1. g \<in> borel_measurable M
 2. AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) g \<le> ennreal l

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) g \<le> ennreal l
[PROOF STEP]
have "eNorm (\<LL> p M) g < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g \<le> ennreal l

goal (1 subgoal):
 1. eNorm (\<LL> p M) g < \<infinity>
[PROOF STEP]
using le_less_trans
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g \<le> ennreal l
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. eNorm (\<LL> p M) g < \<infinity>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) g < \<infinity>

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) g < \<infinity>
[PROOF STEP]
show "g \<in> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g < \<infinity>

goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
using spaceN_iff
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g < \<infinity>
(?x \<in> space\<^sub>N ?N) = (eNorm ?N ?x < \<infinity>)

goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
show "Norm (\<LL> p M) g \<le> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
using \<open>eNorm (\<LL> p M) g \<le> ennreal l\<close> ennreal_le_iff[OF \<open>l \<ge> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g \<le> ennreal l
(ennreal ?x \<le> ennreal l) = (?x \<le> l)

goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
unfolding eNorm_Norm[OF \<open>g \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
ennreal (Norm (\<LL> p M) g) \<le> ennreal l
(ennreal ?x \<le> ennreal l) = (?x \<le> l)

goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) g \<le> l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Lp_AE_limit'':
  assumes "g \<in> borel_measurable M"
          "\<And>n. f n \<in> space\<^sub>N (\<LL> p M)"
          "AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
          "\<And>n. Norm (\<LL> p M) (f n) \<le> C"
  shows "g \<in> space\<^sub>N (\<LL> p M)"
        "Norm (\<LL> p M) g \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> p M) &&& Norm (\<LL> p M) g \<le> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
have "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
by (rule order_trans[OF Norm_nonneg[of "\<LL> p M" "f 0"] \<open>Norm (\<LL> p M) (f 0) \<le> C\<close>])
[PROOF STATE]
proof (state)
this:
0 \<le> C

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
have *: "liminf (\<lambda>n. ennreal C) = ennreal C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liminf (\<lambda>n. ennreal C) = ennreal C
[PROOF STEP]
using Liminf_const trivial_limit_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
?F \<noteq> \<bottom> \<Longrightarrow> Liminf ?F (\<lambda>x. ?c) = ?c
at_top \<noteq> \<bottom>

goal (1 subgoal):
 1. liminf (\<lambda>n. ennreal C) = ennreal C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
liminf (\<lambda>n. ennreal C) = ennreal C

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
have "eNorm (\<LL> p M) (f n) \<le> ennreal C" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (\<LL> p M) (f n) \<le> ennreal C
[PROOF STEP]
unfolding eNorm_Norm[OF \<open>f n \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (Norm (\<LL> p M) (f n)) \<le> ennreal C
[PROOF STEP]
using \<open>Norm (\<LL> p M) (f n) \<le> C\<close>
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> p M) (f n) \<le> C

goal (1 subgoal):
 1. ennreal (Norm (\<LL> p M) (f n)) \<le> ennreal C
[PROOF STEP]
by (auto simp add: ennreal_leI)
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) (f ?n) \<le> ennreal C

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) (f ?n) \<le> ennreal C
[PROOF STEP]
have "liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) (f ?n) \<le> ennreal C

goal (1 subgoal):
 1. liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C
[PROOF STEP]
using Liminf_mono[of "(\<lambda>n. eNorm (\<LL> p M) (f n))" "\<lambda>_. C" sequentially] *
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) (f ?n) \<le> ennreal C
\<forall>\<^sub>F x in sequentially. eNorm (\<LL> p M) (f x) \<le> ennreal C \<Longrightarrow> liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> liminf (\<lambda>x. ennreal C)
liminf (\<lambda>n. ennreal C) = ennreal C

goal (1 subgoal):
 1. liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C
[PROOF STEP]
have "eNorm (\<LL> p M) g \<le> ennreal C"
[PROOF STATE]
proof (prove)
using this:
liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C

goal (1 subgoal):
 1. eNorm (\<LL> p M) g \<le> ennreal C
[PROOF STEP]
using
    Lp_AE_limit[OF \<open>g \<in> borel_measurable M\<close> \<open>AE x in M. (\<lambda>n. f n x) \<longlonglongrightarrow> g x\<close>, of p]
[PROOF STATE]
proof (prove)
using this:
liminf (\<lambda>n. eNorm (\<LL> p M) (f n)) \<le> ennreal C
eNorm (\<LL> p M) g \<le> liminf (\<lambda>n. eNorm (\<LL> p M) (f n))

goal (1 subgoal):
 1. eNorm (\<LL> p M) g \<le> ennreal C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) g \<le> ennreal C

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) g \<le> ennreal C
[PROOF STEP]
have "eNorm (\<LL> p M) g < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g \<le> ennreal C

goal (1 subgoal):
 1. eNorm (\<LL> p M) g < \<infinity>
[PROOF STEP]
using le_less_trans
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g \<le> ennreal C
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. eNorm (\<LL> p M) g < \<infinity>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> p M) g < \<infinity>

goal (2 subgoals):
 1. g \<in> space\<^sub>N (\<LL> p M)
 2. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> p M) g < \<infinity>
[PROOF STEP]
show "g \<in> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g < \<infinity>

goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
using spaceN_iff
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g < \<infinity>
(?x \<in> space\<^sub>N ?N) = (eNorm ?N ?x < \<infinity>)

goal (1 subgoal):
 1. g \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
show "Norm (\<LL> p M) g \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
using \<open>eNorm (\<LL> p M) g \<le> ennreal C\<close> ennreal_le_iff[OF \<open>C \<ge> 0\<close>]
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> p M) g \<le> ennreal C
(ennreal ?x \<le> ennreal C) = (?x \<le> C)

goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
unfolding eNorm_Norm[OF \<open>g \<in> space\<^sub>N (\<LL> p M)\<close>]
[PROOF STATE]
proof (prove)
using this:
ennreal (Norm (\<LL> p M) g) \<le> ennreal C
(ennreal ?x \<le> ennreal C) = (?x \<le> C)

goal (1 subgoal):
 1. Norm (\<LL> p M) g \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> p M) g \<le> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Lp_complete:
  "complete\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete\<^sub>N (\<LL> p M)
[PROOF STEP]
proof (cases rule: Lp_cases[of p])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 2. p = 0 \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 3. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
case zero
[PROOF STATE]
proof (state)
this:
p = 0

goal (3 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 2. p = 0 \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 3. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete\<^sub>N (\<LL> p M)
[PROOF STEP]
proof (rule complete\<^sub>N_I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>cauchy_in\<^sub>N (\<LL> p M) u; \<forall>n. u n \<in> space\<^sub>N (\<LL> p M)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>cauchy_in\<^sub>N (\<LL> p M) u; \<forall>n. u n \<in> space\<^sub>N (\<LL> p M)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x
[PROOF STEP]
assume "\<forall>(n::nat). u n \<in> space\<^sub>N (\<LL> p M)"
[PROOF STATE]
proof (state)
this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>cauchy_in\<^sub>N (\<LL> p M) u; \<forall>n. u n \<in> space\<^sub>N (\<LL> p M)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
have "tendsto_in\<^sub>N (\<LL> p M) u 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. tendsto_in\<^sub>N (\<LL> p M) u 0
[PROOF STEP]
unfolding tendsto_in\<^sub>N_def Norm_def \<open>p = 0\<close> L_zero(1) L_zero_space
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> borel_measurable M

goal (1 subgoal):
 1. (\<lambda>n. enn2real (if u n - 0 \<in> borel_measurable M then 0 else \<infinity>)) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tendsto_in\<^sub>N (\<LL> p M) u 0

goal (1 subgoal):
 1. \<And>u. \<lbrakk>cauchy_in\<^sub>N (\<LL> p M) u; \<forall>n. u n \<in> space\<^sub>N (\<LL> p M)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tendsto_in\<^sub>N (\<LL> p M) u 0
[PROOF STEP]
show "\<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x"
[PROOF STATE]
proof (prove)
using this:
tendsto_in\<^sub>N (\<LL> p M) u 0

goal (1 subgoal):
 1. \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) u x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
complete\<^sub>N (\<LL> p M)

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 2. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 2. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
case (real_pos p2)
[PROOF STATE]
proof (state)
this:
p = ennreal p2
0 < p2
0 < p

goal (2 subgoals):
 1. \<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
 2. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete\<^sub>N (\<LL> p M)
[PROOF STEP]
proof (rule complete\<^sub>N_I'[of "\<lambda>n. (1/2)^n * (1/(defect (\<LL> p M))^(Suc n))"], unfold \<open>p = ennreal p2\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
show "0 < (1/2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
[PROOF STEP]
using defect_ge_1[of "\<LL> (ennreal p2) M"]
[PROOF STATE]
proof (prove)
using this:
1 \<le> defect (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. 0 < (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
0 < (1 / 2) ^ ?n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc ?n)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
assume "\<forall>(n::nat). u n \<in> space\<^sub>N (\<LL> p2 M)" "\<forall>n. Norm (\<LL> p2 M) (u n) \<le> (1/2)^n * (1/(defect (\<LL> p2 M))^(Suc n))"
[PROOF STATE]
proof (state)
this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M)
\<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M)
\<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
[PROOF STEP]
have H: "\<And>n. u n \<in> space\<^sub>N (\<LL> p2 M)"
                 "\<And>n. Norm (\<LL> p2 M) (u n) \<le> (1/2) ^ n * (1/(defect (\<LL> p2 M))^(Suc n))"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M)
\<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)

goal (1 subgoal):
 1. (\<And>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M)) &&& (\<And>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n))
[PROOF STEP]
unfolding \<open>p = ennreal p2\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M)
\<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)

goal (1 subgoal):
 1. (\<And>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M)) &&& (\<And>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u ?n \<in> space\<^sub>N (\<LL> (ennreal p2) M)
Norm (\<LL> (ennreal p2) M) (u ?n) \<le> (1 / 2) ^ ?n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc ?n)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have [measurable]: "u n \<in> borel_measurable M" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n \<in> borel_measurable M
[PROOF STEP]
using Lp_measurable[OF H(1)]
[PROOF STATE]
proof (prove)
using this:
u ?n1 \<in> borel_measurable M

goal (1 subgoal):
 1. u n \<in> borel_measurable M
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
u ?n \<in> borel_measurable M

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
define w where "w = (\<lambda>N x. (\<Sum>n\<in>{..<N}. \<bar>u n x\<bar>))"
[PROOF STATE]
proof (state)
this:
w = (\<lambda>N x. \<Sum>n<N. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have w2: "w = (\<lambda>N. sum (\<lambda>n x. \<bar>u n x\<bar>) {..<N})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = (\<lambda>N. \<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>))
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N x. \<Sum>n<N. \<bar>u n x\<bar>) = (\<lambda>N. \<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>))
[PROOF STEP]
apply (rule ext)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N x. (\<Sum>n<N. \<bar>u n x\<bar>) = (\<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>)) x
[PROOF STEP]
by (metis (mono_tags, lifting) sum.cong fun_sum_apply)
[PROOF STATE]
proof (state)
this:
w = (\<lambda>N. \<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>))

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "incseq (\<lambda>N. w N x)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incseq (\<lambda>N. w N x)
[PROOF STEP]
unfolding w2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incseq (\<lambda>N. (\<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>)) x)
[PROOF STEP]
by (rule incseq_SucI, auto)
[PROOF STATE]
proof (state)
this:
incseq (\<lambda>N. w N ?x)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
incseq (\<lambda>N. w N ?x)
[PROOF STEP]
have wN_inc: "AE x in M. incseq (\<lambda>N. w N x)"
[PROOF STATE]
proof (prove)
using this:
incseq (\<lambda>N. w N ?x)

goal (1 subgoal):
 1. AE x in M. incseq (\<lambda>N. w N x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in M. incseq (\<lambda>N. w N x)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have abs_u_space: "(\<lambda>x. \<bar>u n x\<bar>) \<in> space\<^sub>N (\<LL> p2 M)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<bar>u n x\<bar>) \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
by (rule Lp_Banach_lattice[OF \<open>u n \<in> space\<^sub>N (\<LL> p2 M)\<close>])
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<bar>u ?n x\<bar>) \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. \<bar>u ?n x\<bar>) \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
have wN_space: "w N \<in> space\<^sub>N (\<LL> p2 M)" for N
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<bar>u ?n x\<bar>) \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. w N \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
unfolding w2
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<bar>u ?n x\<bar>) \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. (\<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>)) \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
using H(1)
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<bar>u ?n x\<bar>) \<in> space\<^sub>N (\<LL> (ennreal p2) M)
u ?n \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. (\<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>)) \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?N \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have abs_u_Norm: "Norm (\<LL> p2 M) (\<lambda>x. \<bar>u n x\<bar>) \<le> (1/2) ^ n * (1/(defect (\<LL> p2 M))^(Suc n))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
[PROOF STEP]
using Lp_Banach_lattice(2)[OF \<open>u n \<in> space\<^sub>N (\<LL> p2 M)\<close>] H(2)
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>) = Norm (\<LL> (ennreal p2) M) (u n)
Norm (\<LL> (ennreal p2) M) (u ?n) \<le> (1 / 2) ^ ?n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc ?n)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u ?n x\<bar>) \<le> (1 / 2) ^ ?n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc ?n)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have wN_Norm: "Norm (\<LL> p2 M) (w N) \<le> 2" for N
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
have *: "(defect (\<LL> p2 M))^(Suc n) \<ge> 0" "(defect (\<LL> p2 M))^(Suc n) > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> defect (\<LL> (ennreal p2) M) ^ Suc n &&& 0 < defect (\<LL> (ennreal p2) M) ^ Suc n
[PROOF STEP]
using defect_ge_1[of "\<LL> p2 M"]
[PROOF STATE]
proof (prove)
using this:
1 \<le> defect (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. 0 \<le> defect (\<LL> (ennreal p2) M) ^ Suc n &&& 0 < defect (\<LL> (ennreal p2) M) ^ Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> defect (\<LL> (ennreal p2) M) ^ Suc ?n
0 < defect (\<LL> (ennreal p2) M) ^ Suc ?n

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
have "Norm (\<LL> p2 M) (w N) \<le> (\<Sum>n<N. (defect (\<LL> p2 M))^(Suc n) * Norm (\<LL> p2 M) (\<lambda>x. \<bar>u n x\<bar>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>))
[PROOF STEP]
unfolding w2 lessThan_Suc_atMost[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (\<Sum>n<N. (\<lambda>x. \<bar>u n x\<bar>)) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>))
[PROOF STEP]
by (rule Norm_sum, simp add: abs_u_space)
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) (w N) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>))

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) (w N) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>))

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
have "... \<le> (\<Sum>n<N. (defect (\<LL> p2 M))^(Suc n) * ((1/2) ^ n * (1/(defect (\<LL> p2 M))^(Suc n))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>)) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)))
[PROOF STEP]
apply (rule sum_mono, rule mult_left_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. n \<in> {..<N} \<Longrightarrow> Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
 2. \<And>n. n \<in> {..<N} \<Longrightarrow> 0 \<le> defect (\<LL> (ennreal p2) M) ^ Suc n
[PROOF STEP]
using abs_u_Norm *
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u ?n x\<bar>) \<le> (1 / 2) ^ ?n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc ?n)
0 \<le> defect (\<LL> (ennreal p2) M) ^ Suc ?n
0 < defect (\<LL> (ennreal p2) M) ^ Suc ?n

goal (2 subgoals):
 1. \<And>n. n \<in> {..<N} \<Longrightarrow> Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)
 2. \<And>n. n \<in> {..<N} \<Longrightarrow> 0 \<le> defect (\<LL> (ennreal p2) M) ^ Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>)) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)))

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * Norm (\<LL> (ennreal p2) M) (\<lambda>x. \<bar>u n x\<bar>)) \<le> (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)))

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
have "... = (\<Sum>n<N. (1/2) ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n))) = sum ((^) (1 / 2)) {..<N}
[PROOF STEP]
using *(2) defect_ge_1[of "\<LL> p2 M"]
[PROOF STATE]
proof (prove)
using this:
0 < defect (\<LL> (ennreal p2) M) ^ Suc ?n
1 \<le> defect (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. (\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n))) = sum ((^) (1 / 2)) {..<N}
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n))) = sum ((^) (1 / 2)) {..<N}

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n<N. defect (\<LL> (ennreal p2) M) ^ Suc n * ((1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n))) = sum ((^) (1 / 2)) {..<N}

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
have "... \<le> (\<Sum>n. (1/2) ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) (1 / 2)) {..<N} \<le> (\<Sum>n. (1 / 2) ^ n)
[PROOF STEP]
unfolding lessThan_Suc_atMost[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) (1 / 2)) {..<N} \<le> (\<Sum>n. (1 / 2) ^ n)
[PROOF STEP]
by (rule sum_le_suminf, rule summable_geometric[of "1/2"], auto)
[PROOF STATE]
proof (state)
this:
sum ((^) (1 / 2)) {..<N} \<le> (\<Sum>n. (1 / 2) ^ n)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((^) (1 / 2)) {..<N} \<le> (\<Sum>n. (1 / 2) ^ n)

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
have "... = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. (1 / 2) ^ n) = 2
[PROOF STEP]
using suminf_geometric[of "1/2"]
[PROOF STATE]
proof (prove)
using this:
norm ((1::?'b1) / (2::?'b1)) < 1 \<Longrightarrow> (\<Sum>n. ((1::?'b1) / (2::?'b1)) ^ n) = (1::?'b1) / ((1::?'b1) - (1::?'b1) / (2::?'b1))

goal (1 subgoal):
 1. (\<Sum>n. (1 / 2) ^ n) = 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. (1 / 2) ^ n) = 2

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Norm (\<LL> (ennreal p2) M) (w N) \<le> 2

goal (1 subgoal):
 1. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) (w N) \<le> 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Norm (\<LL> (ennreal p2) M) (w ?N) \<le> 2

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "AE x in M. convergent (\<lambda>N. w N x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. convergent (\<lambda>N. w N x)
[PROOF STEP]
apply (rule Lp_monotone_limit[OF \<open>p > 0\<close>, of _ _ 2], unfold \<open>p = ennreal p2\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. AE x in M. incseq (\<lambda>N. w N x)
 2. \<And>N. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
 3. \<And>N. w N \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
using wN_inc wN_Norm wN_space
[PROOF STATE]
proof (prove)
using this:
AE x in M. incseq (\<lambda>N. w N x)
Norm (\<LL> (ennreal p2) M) (w ?N) \<le> 2
w ?N \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (3 subgoals):
 1. AE x in M. incseq (\<lambda>N. w N x)
 2. \<And>N. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
 3. \<And>N. w N \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. convergent (\<lambda>N. w N x)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
define m where "m = (\<lambda>x. lim (\<lambda>N. w N x))"
[PROOF STATE]
proof (state)
this:
m = (\<lambda>x. lim (\<lambda>N. w N x))

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have m_space: "m \<in> space\<^sub>N (\<LL> p2 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
unfolding m_def \<open>p = ennreal p2\<close>[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. lim (\<lambda>N. w N x)) \<in> space\<^sub>N (\<LL> p M)
[PROOF STEP]
apply (rule Lp_monotone_limit[OF \<open>p > 0\<close>, of _ _ 2], unfold \<open>p = ennreal p2\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. AE x in M. incseq (\<lambda>N. w N x)
 2. \<And>N. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
 3. \<And>N. w N \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
using wN_inc wN_Norm wN_space
[PROOF STATE]
proof (prove)
using this:
AE x in M. incseq (\<lambda>N. w N x)
Norm (\<LL> (ennreal p2) M) (w ?N) \<le> 2
w ?N \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (3 subgoals):
 1. AE x in M. incseq (\<lambda>N. w N x)
 2. \<And>N. Norm (\<LL> (ennreal p2) M) (w N) \<le> 2
 3. \<And>N. w N \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
define v where "v = (\<lambda>x. (\<Sum>n. u n x))"
[PROOF STATE]
proof (state)
this:
v = (\<lambda>x. \<Sum>n. u n x)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have v_meas: "v \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> borel_measurable M
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n. u n x) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> borel_measurable M

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have u_meas: "\<And>n. (sum u {0..<n}) \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. sum u {0..<n} \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum u {0..<?n} \<in> borel_measurable M

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sum u {0..<?n} \<in> borel_measurable M

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
assume "convergent (\<lambda>N. w N x)"
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>N. w N x)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergent (\<lambda>N. w N x)
[PROOF STEP]
have S: "summable (\<lambda>n. \<bar>u n x\<bar>)"
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>N. w N x)

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>u n x\<bar>)
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>N. \<Sum>n<N. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>u n x\<bar>)
[PROOF STEP]
using summable_iff_convergent
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>N. \<Sum>n<N. \<bar>u n x\<bar>)
summable ?f = convergent (\<lambda>n. sum ?f {..<n})

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>u n x\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. \<bar>u n x\<bar>)
[PROOF STEP]
have "m x = (\<Sum>n. \<bar>u n x\<bar>)"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. m x = (\<Sum>n. \<bar>u n x\<bar>)
[PROOF STEP]
unfolding m_def w_def
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. lim (\<lambda>N. \<Sum>n<N. \<bar>u n x\<bar>) = (\<Sum>n. \<bar>u n x\<bar>)
[PROOF STEP]
by (metis suminf_eq_lim)
[PROOF STATE]
proof (state)
this:
m x = (\<Sum>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "summable (\<lambda>n. u n x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. u n x)
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. summable (\<lambda>n. u n x)
[PROOF STEP]
by (rule summable_rabs_cancel)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. u n x)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. u n x)
[PROOF STEP]
have *: "(\<lambda>n. (sum u {..<n}) x) \<longlonglongrightarrow> v x"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. u n x)

goal (1 subgoal):
 1. (\<lambda>n. sum u {..<n} x) \<longlonglongrightarrow> v x
[PROOF STEP]
unfolding v_def fun_sum_apply
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. u n x)

goal (1 subgoal):
 1. (\<lambda>n. \<Sum>i<n. u i x) \<longlonglongrightarrow> (\<Sum>n. u n x)
[PROOF STEP]
by (metis convergent_LIMSEQ_iff suminf_eq_lim summable_iff_convergent)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. sum u {..<n} x) \<longlonglongrightarrow> v x

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "\<bar>(sum u {..<n}) x\<bar> \<le> m x" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
have "\<bar>(sum u {..<n}) x\<bar> \<le> (\<Sum>i\<in>{..<n}. \<bar>u i x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> (\<Sum>i<n. \<bar>u i x\<bar>)
[PROOF STEP]
unfolding fun_sum_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<Sum>i<n. u i x\<bar> \<le> (\<Sum>i<n. \<bar>u i x\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>sum u {..<n} x\<bar> \<le> (\<Sum>i<n. \<bar>u i x\<bar>)

goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>sum u {..<n} x\<bar> \<le> (\<Sum>i<n. \<bar>u i x\<bar>)

goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
have "... \<le> (\<Sum>i. \<bar>u i x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. \<bar>u i x\<bar>) \<le> (\<Sum>i. \<bar>u i x\<bar>)
[PROOF STEP]
apply (rule sum_le_suminf)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. summable (\<lambda>i. \<bar>u i x\<bar>)
 2. finite {..<n}
 3. \<And>na. na \<in> - {..<n} \<Longrightarrow> 0 \<le> \<bar>u na x\<bar>
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (3 subgoals):
 1. summable (\<lambda>i. \<bar>u i x\<bar>)
 2. finite {..<n}
 3. \<And>na. na \<in> - {..<n} \<Longrightarrow> 0 \<le> \<bar>u na x\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<bar>u i x\<bar>) \<le> (\<Sum>i. \<bar>u i x\<bar>)

goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>sum u {..<n} x\<bar> \<le> (\<Sum>i. \<bar>u i x\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>sum u {..<n} x\<bar> \<le> (\<Sum>i. \<bar>u i x\<bar>)

goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
using \<open>m x = (\<Sum>n. \<bar>u n x\<bar>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>sum u {..<n} x\<bar> \<le> (\<Sum>i. \<bar>u i x\<bar>)
m x = (\<Sum>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. \<bar>sum u {..<n} x\<bar> \<le> m x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>sum u {..<n} x\<bar> \<le> m x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>sum u {..<?n} x\<bar> \<le> m x

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>sum u {..<?n} x\<bar> \<le> m x
[PROOF STEP]
have "(\<forall>n. \<bar>(sum u {0..<n}) x\<bar> \<le> m x) \<and> (\<lambda>n. (sum u {0..<n}) x) \<longlonglongrightarrow> v x"
[PROOF STATE]
proof (prove)
using this:
\<bar>sum u {..<?n} x\<bar> \<le> m x

goal (1 subgoal):
 1. (\<forall>n. \<bar>sum u {0..<n} x\<bar> \<le> m x) \<and> (\<lambda>n. sum u {0..<n} x) \<longlonglongrightarrow> v x
[PROOF STEP]
unfolding atLeast0LessThan
[PROOF STATE]
proof (prove)
using this:
\<bar>sum u {..<?n} x\<bar> \<le> m x

goal (1 subgoal):
 1. (\<forall>n. \<bar>sum u {..<n} x\<bar> \<le> m x) \<and> (\<lambda>n. sum u {..<n} x) \<longlonglongrightarrow> v x
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<bar>sum u {..<?n} x\<bar> \<le> m x
(\<lambda>n. sum u {..<n} x) \<longlonglongrightarrow> v x

goal (1 subgoal):
 1. (\<forall>n. \<bar>sum u {..<n} x\<bar> \<le> m x) \<and> (\<lambda>n. sum u {..<n} x) \<longlonglongrightarrow> v x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>n. \<bar>sum u {0..<n} x\<bar> \<le> m x) \<and> (\<lambda>n. sum u {0..<n} x) \<longlonglongrightarrow> v x

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>N. w N ?x2) \<Longrightarrow> (\<forall>n. \<bar>sum u {0..<n} ?x2\<bar> \<le> m ?x2) \<and> (\<lambda>n. sum u {0..<n} ?x2) \<longlonglongrightarrow> v ?x2

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergent (\<lambda>N. w N ?x2) \<Longrightarrow> (\<forall>n. \<bar>sum u {0..<n} ?x2\<bar> \<le> m ?x2) \<and> (\<lambda>n. sum u {0..<n} ?x2) \<longlonglongrightarrow> v ?x2
[PROOF STEP]
have m_bound: "\<And>n. AE x in M. \<bar>(sum u {0..<n}) x\<bar> \<le> m x"
          and u_conv: "AE x in M. (\<lambda>n. (sum u {0..<n}) x) \<longlonglongrightarrow> v x"
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>N. w N ?x2) \<Longrightarrow> (\<forall>n. \<bar>sum u {0..<n} ?x2\<bar> \<le> m ?x2) \<and> (\<lambda>n. sum u {0..<n} ?x2) \<longlonglongrightarrow> v ?x2

goal (1 subgoal):
 1. (\<And>n. AE x in M. \<bar>sum u {0..<n} x\<bar> \<le> m x) &&& AE x in M. (\<lambda>n. sum u {0..<n} x) \<longlonglongrightarrow> v x
[PROOF STEP]
using \<open>AE x in M. convergent (\<lambda>N. w N x)\<close>
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>N. w N ?x2) \<Longrightarrow> (\<forall>n. \<bar>sum u {0..<n} ?x2\<bar> \<le> m ?x2) \<and> (\<lambda>n. sum u {0..<n} ?x2) \<longlonglongrightarrow> v ?x2
AE x in M. convergent (\<lambda>N. w N x)

goal (1 subgoal):
 1. (\<And>n. AE x in M. \<bar>sum u {0..<n} x\<bar> \<le> m x) &&& AE x in M. (\<lambda>n. sum u {0..<n} x) \<longlonglongrightarrow> v x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>sum u {0..<?n} x\<bar> \<le> m x
AE x in M. (\<lambda>n. sum u {0..<n} x) \<longlonglongrightarrow> v x

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "tendsto_in\<^sub>N (\<LL> p2 M) (\<lambda>n. sum u {0..<n}) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v
[PROOF STEP]
by (rule Lp_domination_limit[OF v_meas u_meas m_space u_conv m_bound])
[PROOF STATE]
proof (state)
this:
tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "v \<in> space\<^sub>N (\<LL> p2 M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
by (rule Lp_domination_limit[OF v_meas u_meas m_space u_conv m_bound])
[PROOF STATE]
proof (state)
this:
v \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> (ennreal p2) M); \<forall>n. Norm (\<LL> (ennreal p2) M) (u n) \<le> (1 / 2) ^ n * (1 / defect (\<LL> (ennreal p2) M) ^ Suc n)\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v
v \<in> space\<^sub>N (\<LL> (ennreal p2) M)
[PROOF STEP]
show "\<exists>v \<in> space\<^sub>N (\<LL> p2 M). tendsto_in\<^sub>N (\<LL> p2 M) (\<lambda>n. sum u {0..<n}) v"
[PROOF STATE]
proof (prove)
using this:
tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v
v \<in> space\<^sub>N (\<LL> (ennreal p2) M)

goal (1 subgoal):
 1. \<exists>v\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v\<in>space\<^sub>N (\<LL> (ennreal p2) M). tendsto_in\<^sub>N (\<LL> (ennreal p2) M) (\<lambda>n. sum u {0..<n}) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
complete\<^sub>N (\<LL> p M)

goal (1 subgoal):
 1. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
case PInf
[PROOF STATE]
proof (state)
this:
p = \<infinity>

goal (1 subgoal):
 1. p = \<infinity> \<Longrightarrow> complete\<^sub>N (\<LL> p M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete\<^sub>N (\<LL> p M)
[PROOF STEP]
proof (rule complete\<^sub>N_I'[of "\<lambda>n. (1/2)^n"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
assume "\<forall>(n::nat). u n \<in> space\<^sub>N (\<LL> p M)" "\<forall>n. Norm (\<LL> p M) (u n) \<le> (1/2) ^ n"
[PROOF STATE]
proof (state)
this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)
\<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)
\<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n
[PROOF STEP]
have H: "\<And>n. u n \<in> space\<^sub>N (\<LL> \<infinity> M)" "\<And>n. Norm (\<LL> \<infinity> M) (u n) \<le> (1/2) ^ n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)
\<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n

goal (1 subgoal):
 1. (\<And>n. u n \<in> space\<^sub>N (\<LL> \<infinity> M)) &&& (\<And>n. Norm (\<LL> \<infinity> M) (u n) \<le> (1 / 2) ^ n)
[PROOF STEP]
using PInf
[PROOF STATE]
proof (prove)
using this:
\<forall>n. u n \<in> space\<^sub>N (\<LL> p M)
\<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n
p = \<infinity>

goal (1 subgoal):
 1. (\<And>n. u n \<in> space\<^sub>N (\<LL> \<infinity> M)) &&& (\<And>n. Norm (\<LL> \<infinity> M) (u n) \<le> (1 / 2) ^ n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u ?n \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) (u ?n) \<le> (1 / 2) ^ ?n

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have [measurable]: "u n \<in> borel_measurable M" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u n \<in> borel_measurable M
[PROOF STEP]
using Lp_measurable[OF H(1)]
[PROOF STATE]
proof (prove)
using this:
u ?n1 \<in> borel_measurable M

goal (1 subgoal):
 1. u n \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u ?n \<in> borel_measurable M

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
define v where "v = (\<lambda>x. \<Sum>n. u n x)"
[PROOF STATE]
proof (state)
this:
v = (\<lambda>x. \<Sum>n. u n x)

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have [measurable]: "v \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> borel_measurable M
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n. u n x) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> borel_measurable M

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
define w where "w = (\<lambda>N x. (\<Sum>n\<in>{0..<N}. u n x))"
[PROOF STATE]
proof (state)
this:
w = (\<lambda>N x. \<Sum>n = 0..<N. u n x)

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have [measurable]: "w N \<in> borel_measurable M" for N
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w N \<in> borel_measurable M
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n = 0..<N. u n x) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?N \<in> borel_measurable M

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "AE x in M. \<bar>u n x\<bar> \<le> (1/2)^n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
[PROOF STEP]
using L_infinity_AE_bound[OF H(1), of n] H(2)[of n]
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>u n x\<bar> \<le> Norm (\<LL> \<infinity> M) (u n)
Norm (\<LL> \<infinity> M) (u n) \<le> (1 / 2) ^ n

goal (1 subgoal):
 1. AE x in M. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>u ?n x\<bar> \<le> (1 / 2) ^ ?n

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<bar>u ?n x\<bar> \<le> (1 / 2) ^ ?n
[PROOF STEP]
have "AE x in M. \<forall>n. \<bar>u n x\<bar> \<le> (1/2)^n"
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>u ?n x\<bar> \<le> (1 / 2) ^ ?n

goal (1 subgoal):
 1. AE x in M. \<forall>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
[PROOF STEP]
by (subst AE_all_countable, auto)
[PROOF STATE]
proof (state)
this:
AE x in M. \<forall>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. \<forall>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "\<bar>w N x - v x\<bar> \<le> (1/2)^N * 2" if "\<forall>n. \<bar>u n x\<bar> \<le> (1/2)^n" for N x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have *: "\<And>n. \<bar>u n x\<bar> \<le> (1/2)^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n

goal (1 subgoal):
 1. \<And>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>u ?n x\<bar> \<le> (1 / 2) ^ ?n

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have **: "summable (\<lambda>n. \<bar>u n x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>u n x\<bar>)
[PROOF STEP]
apply (rule summable_norm_cancel, rule summable_comparison_test'[OF summable_geometric[of "1/2"]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. norm (1 / 2) < 1
 2. \<And>n. ?N2 \<le> n \<Longrightarrow> norm (norm \<bar>u n x\<bar>) \<le> (1 / 2) ^ n
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<bar>u ?n x\<bar> \<le> (1 / 2) ^ ?n

goal (2 subgoals):
 1. norm (1 / 2) < 1
 2. \<And>n. ?N2 \<le> n \<Longrightarrow> norm (norm \<bar>u n x\<bar>) \<le> (1 / 2) ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have "\<bar>w N x - v x\<bar> = \<bar>(\<Sum>n. u (n + N) x)\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> = \<bar>\<Sum>n. u (n + N) x\<bar>
[PROOF STEP]
unfolding v_def w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>(\<Sum>n = 0..<N. u n x) - (\<Sum>n. u n x)\<bar> = \<bar>\<Sum>n. u (n + N) x\<bar>
[PROOF STEP]
apply (subst suminf_split_initial_segment[OF summable_rabs_cancel[OF \<open>summable (\<lambda>n. \<bar>u n x\<bar>)\<close>], of "N"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>(\<Sum>n = 0..<N. u n x) - ((\<Sum>n. u (n + N) x) + (\<Sum>i<N. u i x))\<bar> = \<bar>\<Sum>n. u (n + N) x\<bar>
[PROOF STEP]
by (simp add: lessThan_atLeast0)
[PROOF STATE]
proof (state)
this:
\<bar>w N x - v x\<bar> = \<bar>\<Sum>n. u (n + N) x\<bar>

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>w N x - v x\<bar> = \<bar>\<Sum>n. u (n + N) x\<bar>

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have "... \<le> (\<Sum>n. \<bar>u (n + N) x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<Sum>n. u (n + N) x\<bar> \<le> (\<Sum>n. \<bar>u (n + N) x\<bar>)
[PROOF STEP]
apply (rule summable_rabs, subst summable_iff_shift)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>a. \<bar>u a x\<bar>)
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. summable (\<lambda>a. \<bar>u a x\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>n. u (n + N) x\<bar> \<le> (\<Sum>n. \<bar>u (n + N) x\<bar>)

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>n. u (n + N) x\<bar> \<le> (\<Sum>n. \<bar>u (n + N) x\<bar>)

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have "... \<le> (\<Sum>n. (1/2)^(n + N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. \<bar>u (n + N) x\<bar>) \<le> (\<Sum>n. (1 / 2) ^ (n + N))
[PROOF STEP]
proof (rule suminf_le)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<bar>u (n + N) x\<bar> \<le> (1 / 2) ^ (n + N)
 2. summable (\<lambda>n. \<bar>u (n + N) x\<bar>)
 3. summable (\<lambda>n. (1 / 2) ^ (n + N))
[PROOF STEP]
show "\<And>n. \<bar>u (n + N) x\<bar> \<le> (1/2) ^ (n + N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<bar>u (n + N) x\<bar> \<le> (1 / 2) ^ (n + N)
[PROOF STEP]
using *[of "_ + N"]
[PROOF STATE]
proof (prove)
using this:
\<bar>u (?uu3 + N) x\<bar> \<le> (1 / 2) ^ (?uu3 + N)

goal (1 subgoal):
 1. \<And>n. \<bar>u (n + N) x\<bar> \<le> (1 / 2) ^ (n + N)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>u (?n + N) x\<bar> \<le> (1 / 2) ^ (?n + N)

goal (2 subgoals):
 1. summable (\<lambda>n. \<bar>u (n + N) x\<bar>)
 2. summable (\<lambda>n. (1 / 2) ^ (n + N))
[PROOF STEP]
show "summable (\<lambda>n. \<bar>u (n + N) x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>u (n + N) x\<bar>)
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. \<bar>u n x\<bar>)

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>u (n + N) x\<bar>)
[PROOF STEP]
by (subst summable_iff_shift) simp
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>u (n + N) x\<bar>)

goal (1 subgoal):
 1. summable (\<lambda>n. (1 / 2) ^ (n + N))
[PROOF STEP]
show "summable (\<lambda>n. (1/2::real) ^ (n + N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. (1 / 2) ^ (n + N))
[PROOF STEP]
using summable_geometric [of "1/2"]
[PROOF STATE]
proof (prove)
using this:
norm ((1::?'b1) / (2::?'b1)) < 1 \<Longrightarrow> summable ((^) ((1::?'b1) / (2::?'b1)))

goal (1 subgoal):
 1. summable (\<lambda>n. (1 / 2) ^ (n + N))
[PROOF STEP]
by (subst summable_iff_shift) simp
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. (1 / 2) ^ (n + N))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<bar>u (n + N) x\<bar>) \<le> (\<Sum>n. (1 / 2) ^ (n + N))

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<bar>u (n + N) x\<bar>) \<le> (\<Sum>n. (1 / 2) ^ (n + N))

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have "... = (1/2)^N * (\<Sum>n. (1/2)^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. (1 / 2) ^ (n + N)) = (1 / 2) ^ N * (\<Sum>n. (1 / 2) ^ n)
[PROOF STEP]
by (subst power_add, subst suminf_mult2[symmetric], auto simp add: summable_geometric[of "1/2"])
[PROOF STATE]
proof (state)
this:
(\<Sum>n. (1 / 2) ^ (n + N)) = (1 / 2) ^ N * (\<Sum>n. (1 / 2) ^ n)

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. (1 / 2) ^ (n + N)) = (1 / 2) ^ N * (\<Sum>n. (1 / 2) ^ n)

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
have "... = (1/2)^N * 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / 2) ^ N * (\<Sum>n. (1 / 2) ^ n) = (1 / 2) ^ N * 2
[PROOF STEP]
by (subst suminf_geometric, auto)
[PROOF STATE]
proof (state)
this:
(1 / 2) ^ N * (\<Sum>n. (1 / 2) ^ n) = (1 / 2) ^ N * 2

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2

goal (1 subgoal):
 1. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. \<bar>u n ?x\<bar> \<le> (1 / 2) ^ n \<Longrightarrow> \<bar>w ?N ?x - v ?x\<bar> \<le> (1 / 2) ^ ?N * 2

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<forall>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
\<forall>n. \<bar>u n ?x\<bar> \<le> (1 / 2) ^ n \<Longrightarrow> \<bar>w ?N ?x - v ?x\<bar> \<le> (1 / 2) ^ ?N * 2
[PROOF STEP]
have *: "AE x in M. \<bar>w N x - v x\<bar> \<le> (1/2)^N * 2" for N
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<forall>n. \<bar>u n x\<bar> \<le> (1 / 2) ^ n
\<forall>n. \<bar>u n ?x\<bar> \<le> (1 / 2) ^ n \<Longrightarrow> \<bar>w ?N ?x - v ?x\<bar> \<le> (1 / 2) ^ ?N * 2

goal (1 subgoal):
 1. AE x in M. \<bar>w N x - v x\<bar> \<le> (1 / 2) ^ N * 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>w ?N x - v x\<bar> \<le> (1 / 2) ^ ?N * 2

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have **: "w N - v \<in> space\<^sub>N (\<LL> \<infinity> M)" "Norm (\<LL> \<infinity> M) (w N - v) \<le> (1/2)^N * 2" for N
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w N - v \<in> space\<^sub>N (\<LL> \<infinity> M) &&& Norm (\<LL> \<infinity> M) (w N - v) \<le> (1 / 2) ^ N * 2
[PROOF STEP]
unfolding fun_diff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. w N x - v x) \<in> space\<^sub>N (\<LL> \<infinity> M) &&& Norm (\<LL> \<infinity> M) (\<lambda>x. w N x - v x) \<le> (1 / 2) ^ N * 2
[PROOF STEP]
using L_infinity_I[OF _ *]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<lambda>x. w ?N2 x - v x) \<in> borel_measurable M; 0 \<le> (1 / 2) ^ ?N2 * 2\<rbrakk> \<Longrightarrow> (\<lambda>x. w ?N2 x - v x) \<in> space\<^sub>N (\<LL> \<infinity> M)
\<lbrakk>(\<lambda>x. w ?N2 x - v x) \<in> borel_measurable M; 0 \<le> (1 / 2) ^ ?N2 * 2\<rbrakk> \<Longrightarrow> Norm (\<LL> \<infinity> M) (\<lambda>x. w ?N2 x - v x) \<le> (1 / 2) ^ ?N2 * 2

goal (1 subgoal):
 1. (\<lambda>x. w N x - v x) \<in> space\<^sub>N (\<LL> \<infinity> M) &&& Norm (\<LL> \<infinity> M) (\<lambda>x. w N x - v x) \<le> (1 / 2) ^ N * 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w ?N - v \<in> space\<^sub>N (\<LL> \<infinity> M)
Norm (\<LL> \<infinity> M) (w ?N - v) \<le> (1 / 2) ^ ?N * 2

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have l: "(\<lambda>N. ((1/2)^N) * (2::real)) \<longlonglongrightarrow> 0 * 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>N. (1 / 2) ^ N * 2) \<longlonglongrightarrow> 0 * 2
[PROOF STEP]
by (rule tendsto_mult, auto simp add: LIMSEQ_realpow_zero[of "1/2"])
[PROOF STATE]
proof (state)
this:
(\<lambda>N. (1 / 2) ^ N * 2) \<longlonglongrightarrow> 0 * 2

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "tendsto_in\<^sub>N (\<LL> \<infinity> M) w v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tendsto_in\<^sub>N (\<LL> \<infinity> M) w v
[PROOF STEP]
unfolding tendsto_in\<^sub>N_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. Norm (\<LL> \<infinity> M) (w n - v)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule tendsto_sandwich[of "\<lambda>_. 0" _ _ "\<lambda>n. (1/2)^n * 2"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> Norm (\<LL> \<infinity> M) (w n - v)
 2. \<forall>\<^sub>F n in sequentially. Norm (\<LL> \<infinity> M) (w n - v) \<le> (1 / 2) ^ n * 2
 3. (\<lambda>_. 0) \<longlonglongrightarrow> 0
 4. (\<lambda>n. (1 / 2) ^ n * 2) \<longlonglongrightarrow> 0
[PROOF STEP]
using l **(2)
[PROOF STATE]
proof (prove)
using this:
(\<lambda>N. (1 / 2) ^ N * 2) \<longlonglongrightarrow> 0 * 2
Norm (\<LL> \<infinity> M) (w ?N - v) \<le> (1 / 2) ^ ?N * 2

goal (4 subgoals):
 1. \<forall>\<^sub>F n in sequentially. 0 \<le> Norm (\<LL> \<infinity> M) (w n - v)
 2. \<forall>\<^sub>F n in sequentially. Norm (\<LL> \<infinity> M) (w n - v) \<le> (1 / 2) ^ n * 2
 3. (\<lambda>_. 0) \<longlonglongrightarrow> 0
 4. (\<lambda>n. (1 / 2) ^ n * 2) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tendsto_in\<^sub>N (\<LL> \<infinity> M) w v

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
have "v = - (w 0 - v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = - (w 0 - v)
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = - ((\<lambda>x. \<Sum>n = 0..<0. u n x) - v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = - (w 0 - v)

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = - (w 0 - v)
[PROOF STEP]
have "v \<in> space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (prove)
using this:
v = - (w 0 - v)

goal (1 subgoal):
 1. v \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
using **(1)[of 0] spaceN_add spaceN_diff
[PROOF STATE]
proof (prove)
using this:
v = - (w 0 - v)
w 0 - v \<in> space\<^sub>N (\<LL> \<infinity> M)
\<lbrakk>?x \<in> space\<^sub>N ?N; ?y \<in> space\<^sub>N ?N\<rbrakk> \<Longrightarrow> ?x + ?y \<in> space\<^sub>N ?N
\<lbrakk>?x \<in> space\<^sub>N ?N; ?y \<in> space\<^sub>N ?N\<rbrakk> \<Longrightarrow> ?x - ?y \<in> space\<^sub>N ?N

goal (1 subgoal):
 1. v \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
v \<in> space\<^sub>N (\<LL> \<infinity> M)

goal (2 subgoals):
 1. \<And>n. 0 < (1 / 2) ^ n
 2. \<And>u. \<lbrakk>\<forall>n. u n \<in> space\<^sub>N (\<LL> p M); \<forall>n. Norm (\<LL> p M) (u n) \<le> (1 / 2) ^ n\<rbrakk> \<Longrightarrow> \<exists>x\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
show "\<exists>v \<in> space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) v"
[PROOF STATE]
proof (prove)
using this:
v \<in> space\<^sub>N (\<LL> \<infinity> M)

goal (1 subgoal):
 1. \<exists>v\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) v
[PROOF STEP]
using \<open>tendsto_in\<^sub>N (\<LL> \<infinity> M) w v\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> space\<^sub>N (\<LL> \<infinity> M)
tendsto_in\<^sub>N (\<LL> \<infinity> M) w v

goal (1 subgoal):
 1. \<exists>v\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) v
[PROOF STEP]
unfolding \<open>p = \<infinity>\<close> w_def fun_sum_apply[symmetric]
[PROOF STATE]
proof (prove)
using this:
v \<in> space\<^sub>N (\<LL> \<infinity> M)
tendsto_in\<^sub>N (\<LL> \<infinity> M) (\<lambda>N. sum u {0..<N}) v

goal (1 subgoal):
 1. \<exists>v\<in>space\<^sub>N (\<LL> \<infinity> M). tendsto_in\<^sub>N (\<LL> \<infinity> M) (\<lambda>n. sum u {0..<n}) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v\<in>space\<^sub>N (\<LL> p M). tendsto_in\<^sub>N (\<LL> p M) (\<lambda>n. sum u {0..<n}) v

goal (1 subgoal):
 1. \<And>n. 0 < (1 / 2) ^ n
[PROOF STEP]
qed (simp)
[PROOF STATE]
proof (state)
this:
complete\<^sub>N (\<LL> p M)

goal:
No subgoals!
[PROOF STEP]
qed