[STATEMENT]
lemma ell2_norm_triangle:
  assumes "has_ell2_norm x" and "has_ell2_norm y"
  shows "has_ell2_norm (\<lambda>i. x i + y i)" and "ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm (\<lambda>i. x i + y i) &&& ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. x i + y i)
 2. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have triangle: "L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F"
    (is "?lhs\<le>?rhs")
    if "finite F" for F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
have "?lhs \<le> L2_set (\<lambda>i. (cmod o x) i + (cmod o y) i) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (\<lambda>i. (cmod \<circ> x) i + (cmod \<circ> y) i) F
[PROOF STEP]
proof (rule L2_set_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> F \<Longrightarrow> (cmod \<circ> (\<lambda>i. x i + y i)) i \<le> (cmod \<circ> x) i + (cmod \<circ> y) i
 2. \<And>i. i \<in> F \<Longrightarrow> 0 \<le> (cmod \<circ> (\<lambda>i. x i + y i)) i
[PROOF STEP]
show "(cmod \<circ> (\<lambda>i. x i + y i)) i \<le> (cmod \<circ> x) i + (cmod \<circ> y) i"
        if "i \<in> F"
        for i :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod \<circ> (\<lambda>i. x i + y i)) i \<le> (cmod \<circ> x) i + (cmod \<circ> y) i
[PROOF STEP]
using that norm_triangle_ineq
[PROOF STATE]
proof (prove)
using this:
i \<in> F
norm (?x + ?y) \<le> norm ?x + norm ?y

goal (1 subgoal):
 1. (cmod \<circ> (\<lambda>i. x i + y i)) i \<le> (cmod \<circ> x) i + (cmod \<circ> y) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in> F \<Longrightarrow> (cmod \<circ> (\<lambda>i. x i + y i)) ?i \<le> (cmod \<circ> x) ?i + (cmod \<circ> y) ?i

goal (1 subgoal):
 1. \<And>i. i \<in> F \<Longrightarrow> 0 \<le> (cmod \<circ> (\<lambda>i. x i + y i)) i
[PROOF STEP]
show "0 \<le> (cmod \<circ> (\<lambda>i. x i + y i)) i"
        if "i \<in> F"
        for i :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (cmod \<circ> (\<lambda>i. x i + y i)) i
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<in> F

goal (1 subgoal):
 1. 0 \<le> (cmod \<circ> (\<lambda>i. x i + y i)) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?i \<in> F \<Longrightarrow> 0 \<le> (cmod \<circ> (\<lambda>i. x i + y i)) ?i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (\<lambda>i. (cmod \<circ> x) i + (cmod \<circ> y) i) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (\<lambda>i. (cmod \<circ> x) i + (cmod \<circ> y) i) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
have "\<dots> \<le> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (\<lambda>i. (cmod \<circ> x) i + (cmod \<circ> y) i) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
by (rule L2_set_triangle_ineq)
[PROOF STATE]
proof (state)
this:
L2_set (\<lambda>i. (cmod \<circ> x) i + (cmod \<circ> y) i) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ?F \<le> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. x i + y i)
 2. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
obtain Mx My where Mx: "Mx \<ge> L2_set (cmod o x) F" and My: "My \<ge> L2_set (cmod o y) F"
    if "finite F" for F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Mx My. \<lbrakk>\<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> x) F \<le> Mx; \<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> y) F \<le> My\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x
has_ell2_norm y

goal (1 subgoal):
 1. (\<And>Mx My. \<lbrakk>\<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> x) F \<le> Mx; \<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> y) F \<le> My\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding has_ell2_norm_L2_set bdd_above_def
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>x\<in>L2_set (cmod \<circ> x) ` Collect finite. x \<le> M
\<exists>M. \<forall>x\<in>L2_set (cmod \<circ> y) ` Collect finite. x \<le> M

goal (1 subgoal):
 1. (\<And>Mx My. \<lbrakk>\<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> x) F \<le> Mx; \<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> y) F \<le> My\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F \<le> Mx
finite ?F \<Longrightarrow> L2_set (cmod \<circ> y) ?F \<le> My

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. x i + y i)
 2. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
hence MxMy: "Mx + My \<ge> L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F" if "finite F" for F
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F \<le> Mx
finite ?F \<Longrightarrow> L2_set (cmod \<circ> y) ?F \<le> My

goal (1 subgoal):
 1. L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F \<le> Mx + My
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F \<le> Mx
finite ?F \<Longrightarrow> L2_set (cmod \<circ> y) ?F \<le> My
finite F

goal (1 subgoal):
 1. L2_set (cmod \<circ> x) F + L2_set (cmod \<circ> y) F \<le> Mx + My
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F \<le> Mx + My

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. x i + y i)
 2. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
hence bdd_plus: "bdd_above ((\<lambda>xa. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa) ` Collect finite)"
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F \<le> Mx + My

goal (1 subgoal):
 1. bdd_above ((\<lambda>xa. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa) ` Collect finite)
[PROOF STEP]
unfolding bdd_above_def
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F \<le> Mx + My

goal (1 subgoal):
 1. \<exists>M. \<forall>x\<in>(\<lambda>xa. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa) ` Collect finite. x \<le> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>xa. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa) ` Collect finite)

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. x i + y i)
 2. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
from MxMy
[PROOF STATE]
proof (chain)
picking this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F \<le> Mx + My
[PROOF STEP]
have MxMy': "Mx + My \<ge> L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F" if "finite F" for F
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F \<le> Mx + My

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> Mx + My
[PROOF STEP]
using triangle that
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F \<le> Mx + My
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ?F \<le> L2_set (cmod \<circ> x) ?F + L2_set (cmod \<circ> y) ?F
finite F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. x i + y i)) F \<le> Mx + My
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ?F \<le> Mx + My

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. x i + y i)
 2. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
thus has: "has_ell2_norm (\<lambda>i. x i + y i)"
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ?F \<le> Mx + My

goal (1 subgoal):
 1. has_ell2_norm (\<lambda>i. x i + y i)
[PROOF STEP]
unfolding has_ell2_norm_L2_set bdd_above_def
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ?F \<le> Mx + My

goal (1 subgoal):
 1. \<exists>M. \<forall>x\<in>L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite. x \<le> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
has_ell2_norm (\<lambda>i. x i + y i)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have SUP_plus: "(SUP x\<in>A. f x + g x) \<le> (SUP x\<in>A. f x) + (SUP x\<in>A. g x)"
    if notempty: "A\<noteq>{}" and bddf: "bdd_above (f`A)"and bddg: "bdd_above (g`A)"
    for f g :: "'a set \<Rightarrow> real" and A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
have xleq: "x \<le> (SUP x\<in>A. f x) + (SUP x\<in>A. g x)" if x: "x \<in> (\<lambda>x. f x + g x) ` A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
obtain a where aA: "a:A" and ax: "x = f a + g a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x = f a + g a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>x. f x + g x) ` A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x = f a + g a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
x = f a + g a

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
have fa: "f a \<le> (SUP x\<in>A. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<le> \<Squnion> (f ` A)
[PROOF STEP]
by (simp add: bddf aA cSUP_upper)
[PROOF STATE]
proof (state)
this:
f a \<le> \<Squnion> (f ` A)

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f a \<le> \<Squnion> (f ` A)

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
have "g a \<le> (SUP x\<in>A. g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g a \<le> \<Squnion> (g ` A)
[PROOF STEP]
by (simp add: bddg aA cSUP_upper)
[PROOF STATE]
proof (state)
this:
g a \<le> \<Squnion> (g ` A)

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f a \<le> \<Squnion> (f ` A)
g a \<le> \<Squnion> (g ` A)
[PROOF STEP]
have "f a + g a \<le> (SUP x\<in>A. f x) + (SUP x\<in>A. g x)"
[PROOF STATE]
proof (prove)
using this:
f a \<le> \<Squnion> (f ` A)
g a \<le> \<Squnion> (g ` A)

goal (1 subgoal):
 1. f a + g a \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f a + g a \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
with ax
[PROOF STATE]
proof (chain)
picking this:
x = f a + g a
f a + g a \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = f a + g a
f a + g a \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> (\<lambda>x. f x + g x) ` A \<Longrightarrow> ?x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
have "(\<lambda>x. f x + g x) ` A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x + g x) ` A \<noteq> {}
[PROOF STEP]
using notempty
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. (\<lambda>x. f x + g x) ` A \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) ` A \<noteq> {}

goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x + g x) ` A \<noteq> {}

goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
have "x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)"
      if "x \<in> (\<lambda>x. f x + g x) ` A"
      for x :: real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>x. f x + g x) ` A

goal (1 subgoal):
 1. x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
by (simp add: xleq)
[PROOF STATE]
proof (state)
this:
?x \<in> (\<lambda>x. f x + g x) ` A \<Longrightarrow> ?x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x + g x) ` A \<noteq> {}
?x \<in> (\<lambda>x. f x + g x) ` A \<Longrightarrow> ?x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x + g x) ` A \<noteq> {}
?x \<in> (\<lambda>x. f x + g x) ` A \<Longrightarrow> ?x \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal (1 subgoal):
 1. (\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)
[PROOF STEP]
by (meson bdd_above_def cSup_le_iff)
[PROOF STATE]
proof (state)
this:
(\<Squnion>x\<in>A. f x + g x) \<le> \<Squnion> (f ` A) + \<Squnion> (g ` A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A \<noteq> {}; bdd_above (?f ` ?A); bdd_above (?g ` ?A)\<rbrakk> \<Longrightarrow> (\<Squnion>x\<in>?A. ?f x + ?g x) \<le> \<Squnion> (?f ` ?A) + \<Squnion> (?g ` ?A)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have a2: "bdd_above (L2_set (cmod \<circ> x) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
by (meson assms(1) has_ell2_norm_L2_set)
[PROOF STATE]
proof (state)
this:
bdd_above (L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have a3: "bdd_above (L2_set (cmod \<circ> y) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> y) ` Collect finite)
[PROOF STEP]
by (meson assms(2) has_ell2_norm_L2_set)
[PROOF STATE]
proof (state)
this:
bdd_above (L2_set (cmod \<circ> y) ` Collect finite)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have a1: "Collect finite \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect finite \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Collect finite \<noteq> {}

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have a4: "\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite)
    \<le> (SUP xa\<in>Collect finite.
           L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> (\<Squnion>xa\<in>Collect finite. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa)
[PROOF STEP]
by (metis (mono_tags, lifting) a1 bdd_plus cSUP_mono mem_Collect_eq triangle)
[PROOF STATE]
proof (state)
this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> (\<Squnion>xa\<in>Collect finite. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
have "\<forall>r. \<Squnion> (L2_set (cmod \<circ> (\<lambda>a. x a + y a)) ` Collect finite) \<le> r \<or> \<not> (SUP A\<in>Collect finite. L2_set (cmod \<circ> x) A + L2_set (cmod \<circ> y) A) \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. \<Squnion> (L2_set (cmod \<circ> (\<lambda>a. x a + y a)) ` Collect finite) \<le> r \<or> \<not> (\<Squnion>A\<in>Collect finite. L2_set (cmod \<circ> x) A + L2_set (cmod \<circ> y) A) \<le> r
[PROOF STEP]
using a4
[PROOF STATE]
proof (prove)
using this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> (\<Squnion>xa\<in>Collect finite. L2_set (cmod \<circ> x) xa + L2_set (cmod \<circ> y) xa)

goal (1 subgoal):
 1. \<forall>r. \<Squnion> (L2_set (cmod \<circ> (\<lambda>a. x a + y a)) ` Collect finite) \<le> r \<or> \<not> (\<Squnion>A\<in>Collect finite. L2_set (cmod \<circ> x) A + L2_set (cmod \<circ> y) A) \<le> r
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<forall>r. \<Squnion> (L2_set (cmod \<circ> (\<lambda>a. x a + y a)) ` Collect finite) \<le> r \<or> \<not> (\<Squnion>A\<in>Collect finite. L2_set (cmod \<circ> x) A + L2_set (cmod \<circ> y) A) \<le> r

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
hence "\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite)
    \<le> \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite) +
       \<Squnion> (L2_set (cmod \<circ> y) ` Collect finite)"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. \<Squnion> (L2_set (cmod \<circ> (\<lambda>a. x a + y a)) ` Collect finite) \<le> r \<or> \<not> (\<Squnion>A\<in>Collect finite. L2_set (cmod \<circ> x) A + L2_set (cmod \<circ> y) A) \<le> r

goal (1 subgoal):
 1. \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite) + \<Squnion> (L2_set (cmod \<circ> y) ` Collect finite)
[PROOF STEP]
by (metis (no_types) SUP_plus a1 a2 a3)
[PROOF STATE]
proof (state)
this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite) + \<Squnion> (L2_set (cmod \<circ> y) ` Collect finite)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
hence "\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> ell2_norm x + ell2_norm y"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite) + \<Squnion> (L2_set (cmod \<circ> y) ` Collect finite)

goal (1 subgoal):
 1. \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
by (simp add: assms(1) assms(2) ell2_norm_L2_set)
[PROOF STATE]
proof (state)
this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> ell2_norm x + ell2_norm y

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
thus "ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y"
[PROOF STATE]
proof (prove)
using this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. x i + y i)) ` Collect finite) \<le> ell2_norm x + ell2_norm y

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y
[PROOF STEP]
by (simp add: ell2_norm_L2_set has)
[PROOF STATE]
proof (state)
this:
ell2_norm (\<lambda>i. x i + y i) \<le> ell2_norm x + ell2_norm y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ell2_norm_uminus:
  assumes "has_ell2_norm x"
  shows \<open>has_ell2_norm (\<lambda>i. - x i)\<close> and \<open>ell2_norm (\<lambda>i. - x i) = ell2_norm x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm (\<lambda>i. - x i) &&& ell2_norm (\<lambda>i. - x i) = ell2_norm x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x

goal (1 subgoal):
 1. has_ell2_norm (\<lambda>i. - x i) &&& ell2_norm (\<lambda>i. - x i) = ell2_norm x
[PROOF STEP]
by (auto simp: has_ell2_norm_def ell2_norm_def)


[STATEMENT]
lemma norm_point_bound_ell2: "norm (Rep_ell2 x i) \<le> norm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (Rep_ell2 x i) \<le> norm x
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. has_ell2_norm x \<Longrightarrow> cmod (x i) \<le> ell2_norm x
[PROOF STEP]
by (simp add: ell2_norm_point_bound)


[STATEMENT]
lemma ell2_norm_finite_support:
  assumes \<open>finite S\<close> \<open>\<And> i. i \<notin> S \<Longrightarrow> Rep_ell2 x i = 0\<close>
  shows \<open>norm x = sqrt ((sum (\<lambda>i. (cmod (Rep_ell2 x i))\<^sup>2)) S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
proof (insert assms(2), transfer fixing: S)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
fix x :: \<open>'a \<Rightarrow> complex\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
assume zero: \<open>\<And>i. i \<notin> S \<Longrightarrow> x i = 0\<close>
[PROOF STATE]
proof (state)
this:
?i \<notin> S \<Longrightarrow> x ?i = 0

goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
have \<open>ell2_norm x = sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)
[PROOF STEP]
by (auto simp: ell2_norm_def)
[PROOF STATE]
proof (state)
this:
ell2_norm x = sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ell2_norm x = sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
have \<open>\<dots> = sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
apply (subst infsum_cong_neutral[where g=\<open>\<lambda>i. (cmod (x i))\<^sup>2\<close> and S=UNIV and T=S])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> S - UNIV \<Longrightarrow> (cmod (x x))\<^sup>2 = 0
 2. \<And>x. x \<in> UNIV - S \<Longrightarrow> (cmod (x x))\<^sup>2 = 0
 3. \<And>x. x \<in> UNIV \<inter> S \<Longrightarrow> (cmod (x x))\<^sup>2 = (cmod (x x))\<^sup>2
 4. sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2) = sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
using zero
[PROOF STATE]
proof (prove)
using this:
?i \<notin> S \<Longrightarrow> x ?i = 0

goal (4 subgoals):
 1. \<And>x. x \<in> S - UNIV \<Longrightarrow> (cmod (x x))\<^sup>2 = 0
 2. \<And>x. x \<in> UNIV - S \<Longrightarrow> (cmod (x x))\<^sup>2 = 0
 3. \<And>x. x \<in> UNIV \<inter> S \<Longrightarrow> (cmod (x x))\<^sup>2 = (cmod (x x))\<^sup>2
 4. sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2) = sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
have \<open>\<dots> = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2) = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
using \<open>finite S\<close>
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2) = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>\<^sub>\<infinity>i\<in>S. (cmod (x i))\<^sup>2) = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>has_ell2_norm x; \<And>i. i \<notin> S \<Longrightarrow> x i = 0\<rbrakk> \<Longrightarrow> ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
show \<open>ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
using this:
ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)

goal (1 subgoal):
 1. ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
ell2_norm x = sqrt (\<Sum>i\<in>S. (cmod (x i))\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_ell2_transfer[transfer_rule]:
  includes lifting_syntax
  shows \<open>(((=) ===> pcr_ell2 (=)) ===> rel_set (=) ===> pcr_ell2 (=))
          (\<lambda>f X x. sum (\<lambda>y. f y x) X) sum\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> pcr_ell2 (=)) ===> rel_set (=) ===> pcr_ell2 (=)) (\<lambda>f X x. \<Sum>y\<in>X. f y x) sum
[PROOF STEP]
proof (intro rel_funI, rename_tac f f' X X')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f f' X X'. \<lbrakk>((=) ===> pcr_ell2 (=)) f f'; rel_set (=) X X'\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
fix f and f' :: \<open>'a \<Rightarrow> 'b ell2\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f f' X X'. \<lbrakk>((=) ===> pcr_ell2 (=)) f f'; rel_set (=) X X'\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
assume [transfer_rule]: \<open>((=) ===> pcr_ell2 (=)) f f'\<close>
[PROOF STATE]
proof (state)
this:
((=) ===> pcr_ell2 (=)) f f'

goal (1 subgoal):
 1. \<And>f f' X X'. \<lbrakk>((=) ===> pcr_ell2 (=)) f f'; rel_set (=) X X'\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
fix X X' :: \<open>'a set\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f f' X X'. \<lbrakk>((=) ===> pcr_ell2 (=)) f f'; rel_set (=) X X'\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
assume \<open>rel_set (=) X X'\<close>
[PROOF STATE]
proof (state)
this:
rel_set (=) X X'

goal (1 subgoal):
 1. \<And>f f' X X'. \<lbrakk>((=) ===> pcr_ell2 (=)) f f'; rel_set (=) X X'\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_set (=) X X'
[PROOF STEP]
have [simp]: \<open>X' = X\<close>
[PROOF STATE]
proof (prove)
using this:
rel_set (=) X X'

goal (1 subgoal):
 1. X' = X
[PROOF STEP]
by (simp add: rel_set_eq)
[PROOF STATE]
proof (state)
this:
X' = X

goal (1 subgoal):
 1. \<And>f f' X X'. \<lbrakk>((=) ===> pcr_ell2 (=)) f f'; rel_set (=) X X'\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
show \<open>pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')
[PROOF STEP]
unfolding \<open>X' = X\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X)
[PROOF STEP]
proof (induction X rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. infinite A \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>A. f y x) (sum f' A)
 2. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
case (infinite X)
[PROOF STATE]
proof (state)
this:
infinite X

goal (3 subgoals):
 1. \<And>A. infinite A \<Longrightarrow> pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>A. f y x) (sum f' A)
 2. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X)
[PROOF STEP]
apply (simp add: infinite)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>x. 0) 0
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X)

goal (2 subgoals):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})
[PROOF STEP]
apply (simp add: empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>x. 0) 0
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>{}. f y x) (sum f' {})

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
note [transfer_rule] = insert.IH
[PROOF STATE]
proof (state)
this:
pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>F. f y x) (sum f' F)\<rbrakk> \<Longrightarrow> pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))
[PROOF STEP]
apply (simp add: insert)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcr_ell2 (=) (\<lambda>xa. f x xa + (\<Sum>y\<in>F. f y xa)) (f' x + sum f' F)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
pcr_ell2 (=) (\<lambda>xa. \<Sum>y\<in>insert x F. f y xa) (sum f' (insert x F))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pcr_ell2 (=) (\<lambda>x. \<Sum>y\<in>X. f y x) (sum f' X')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ell2_pointwise_ortho:
  assumes \<open>\<And> i. Rep_ell2 x i = 0 \<or> Rep_ell2 y i = 0\<close>
  shows \<open>is_orthogonal x y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_orthogonal x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Rep_ell2 x ?i = 0 \<or> Rep_ell2 y ?i = 0

goal (1 subgoal):
 1. is_orthogonal x y
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>has_ell2_norm x; has_ell2_norm y; \<And>i. x i = 0 \<or> y i = 0\<rbrakk> \<Longrightarrow> (\<Sum>\<^sub>\<infinity>i. cnj (x i) * y i) = 0
[PROOF STEP]
by (simp add: infsum_0)


[STATEMENT]
lemma trunc_ell2_empty[simp]: \<open>trunc_ell2 {} x = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 {} x = 0
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. has_ell2_norm x \<Longrightarrow> (\<lambda>i. if i \<in> {} then x i else 0) = (\<lambda>_. 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma trunc_ell2_UNIV[simp]: \<open>trunc_ell2 UNIV \<psi> = \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 UNIV \<psi> = \<psi>
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> (\<lambda>i. if i \<in> UNIV then \<psi> i else 0) = \<psi>
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_id_minus_trunc_ell2:
  \<open>(norm (x - trunc_ell2 S x))^2 = (norm x)^2 - (norm (trunc_ell2 S x))^2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2
[PROOF STEP]
have \<open>Rep_ell2 (trunc_ell2 S x) i = 0 \<or> Rep_ell2 (x - trunc_ell2 S x) i = 0\<close> for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_ell2 (trunc_ell2 S x) i = 0 \<or> Rep_ell2 (x - trunc_ell2 S x) i = 0
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S x i. has_ell2_norm x \<Longrightarrow> (if i \<in> S then x i else 0) = 0 \<or> x i - (if i \<in> S then x i else 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Rep_ell2 (trunc_ell2 S x) ?i = 0 \<or> Rep_ell2 (x - trunc_ell2 S x) ?i = 0

goal (1 subgoal):
 1. (norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2
[PROOF STEP]
hence \<open>((trunc_ell2 S x) \<bullet>\<^sub>C (x - trunc_ell2 S x)) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
Rep_ell2 (trunc_ell2 S x) ?i = 0 \<or> Rep_ell2 (x - trunc_ell2 S x) ?i = 0

goal (1 subgoal):
 1. is_orthogonal (trunc_ell2 S x) (x - trunc_ell2 S x)
[PROOF STEP]
using ell2_pointwise_ortho
[PROOF STATE]
proof (prove)
using this:
Rep_ell2 (trunc_ell2 S x) ?i = 0 \<or> Rep_ell2 (x - trunc_ell2 S x) ?i = 0
(\<And>i. Rep_ell2 ?x i = 0 \<or> Rep_ell2 ?y i = 0) \<Longrightarrow> is_orthogonal ?x ?y

goal (1 subgoal):
 1. is_orthogonal (trunc_ell2 S x) (x - trunc_ell2 S x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_orthogonal (trunc_ell2 S x) (x - trunc_ell2 S x)

goal (1 subgoal):
 1. (norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2
[PROOF STEP]
hence \<open>(norm x)^2 = (norm (trunc_ell2 S x))^2 + (norm (x - trunc_ell2 S x))^2\<close>
[PROOF STATE]
proof (prove)
using this:
is_orthogonal (trunc_ell2 S x) (x - trunc_ell2 S x)

goal (1 subgoal):
 1. (norm x)\<^sup>2 = (norm (trunc_ell2 S x))\<^sup>2 + (norm (x - trunc_ell2 S x))\<^sup>2
[PROOF STEP]
using pythagorean_theorem
[PROOF STATE]
proof (prove)
using this:
is_orthogonal (trunc_ell2 S x) (x - trunc_ell2 S x)
is_orthogonal ?x ?y \<Longrightarrow> (norm (?x + ?y))\<^sup>2 = (norm ?x)\<^sup>2 + (norm ?y)\<^sup>2

goal (1 subgoal):
 1. (norm x)\<^sup>2 = (norm (trunc_ell2 S x))\<^sup>2 + (norm (x - trunc_ell2 S x))\<^sup>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(norm x)\<^sup>2 = (norm (trunc_ell2 S x))\<^sup>2 + (norm (x - trunc_ell2 S x))\<^sup>2

goal (1 subgoal):
 1. (norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(norm x)\<^sup>2 = (norm (trunc_ell2 S x))\<^sup>2 + (norm (x - trunc_ell2 S x))\<^sup>2

goal (1 subgoal):
 1. (norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(norm (x - trunc_ell2 S x))\<^sup>2 = (norm x)\<^sup>2 - (norm (trunc_ell2 S x))\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma norm_trunc_ell2_finite:
  \<open>finite S \<Longrightarrow> (norm (trunc_ell2 S x)) = sqrt ((sum (\<lambda>i. (cmod (Rep_ell2 x i))\<^sup>2)) S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
assume \<open>finite S\<close>
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
have \<open>\<And> i. i \<notin> S \<Longrightarrow> Rep_ell2 ((trunc_ell2 S x)) i = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<notin> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) i = 0
[PROOF STEP]
by (simp add: trunc_ell2.rep_eq)
[PROOF STATE]
proof (state)
this:
?i \<notin> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = 0

goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite S
?i \<notin> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = 0
[PROOF STEP]
have \<open>(norm (trunc_ell2 S x)) = sqrt ((sum (\<lambda>i. (cmod (Rep_ell2 ((trunc_ell2 S x)) i))\<^sup>2)) S)\<close>
[PROOF STATE]
proof (prove)
using this:
finite S
?i \<notin> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = 0

goal (1 subgoal):
 1. norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 (trunc_ell2 S x) i))\<^sup>2)
[PROOF STEP]
using ell2_norm_finite_support
[PROOF STATE]
proof (prove)
using this:
finite S
?i \<notin> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = 0
\<lbrakk>finite ?S; \<And>i. i \<notin> ?S \<Longrightarrow> Rep_ell2 ?x i = 0\<rbrakk> \<Longrightarrow> norm ?x = sqrt (\<Sum>i\<in>?S. (cmod (Rep_ell2 ?x i))\<^sup>2)

goal (1 subgoal):
 1. norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 (trunc_ell2 S x) i))\<^sup>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 (trunc_ell2 S x) i))\<^sup>2)

goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 (trunc_ell2 S x) i))\<^sup>2)

goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
have \<open>\<And> i. i \<in> S \<Longrightarrow> Rep_ell2 ((trunc_ell2 S x)) i = Rep_ell2 x i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) i = Rep_ell2 x i
[PROOF STEP]
by (simp add: trunc_ell2.rep_eq)
[PROOF STATE]
proof (state)
this:
?i \<in> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = Rep_ell2 x ?i

goal (1 subgoal):
 1. finite S \<Longrightarrow> norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 (trunc_ell2 S x) i))\<^sup>2)
?i \<in> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = Rep_ell2 x ?i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 (trunc_ell2 S x) i))\<^sup>2)
?i \<in> S \<Longrightarrow> Rep_ell2 (trunc_ell2 S x) ?i = Rep_ell2 x ?i

goal (1 subgoal):
 1. norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 S x) = sqrt (\<Sum>i\<in>S. (cmod (Rep_ell2 x i))\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trunc_ell2_lim_at_UNIV:
  \<open>((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
define f where \<open>f i = (cmod (Rep_ell2 \<psi> i))\<^sup>2\<close> for i
[PROOF STATE]
proof (state)
this:
f ?i = (cmod (Rep_ell2 \<psi> ?i))\<^sup>2

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have has: \<open>has_ell2_norm (Rep_ell2 \<psi>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm (Rep_ell2 \<psi>)
[PROOF STEP]
using Rep_ell2
[PROOF STATE]
proof (prove)
using this:
Rep_ell2 ?x \<in> {x. has_ell2_norm x}

goal (1 subgoal):
 1. has_ell2_norm (Rep_ell2 \<psi>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
has_ell2_norm (Rep_ell2 \<psi>)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
has_ell2_norm (Rep_ell2 \<psi>)
[PROOF STEP]
have summable: "f abs_summable_on UNIV"
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm (Rep_ell2 \<psi>)

goal (1 subgoal):
 1. f abs_summable_on UNIV
[PROOF STEP]
by (smt (verit, del_insts) f_def has_ell2_norm_def norm_ge_zero norm_power real_norm_def summable_on_cong)
[PROOF STATE]
proof (state)
this:
f abs_summable_on UNIV

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>norm \<psi> = (ell2_norm (Rep_ell2 \<psi>))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm \<psi> = ell2_norm (Rep_ell2 \<psi>)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> ell2_norm \<psi> = ell2_norm \<psi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm \<psi> = ell2_norm (Rep_ell2 \<psi>)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm \<psi> = ell2_norm (Rep_ell2 \<psi>)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>\<dots> = sqrt (infsum f UNIV)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm (Rep_ell2 \<psi>) = sqrt (infsum f UNIV)
[PROOF STEP]
by (simp add: ell2_norm_def f_def[symmetric])
[PROOF STATE]
proof (state)
this:
ell2_norm (Rep_ell2 \<psi>) = sqrt (infsum f UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm \<psi> = sqrt (infsum f UNIV)
[PROOF STEP]
have norm\<psi>: \<open>norm \<psi> = sqrt (infsum f UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
norm \<psi> = sqrt (infsum f UNIV)

goal (1 subgoal):
 1. norm \<psi> = sqrt (infsum f UNIV)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
norm \<psi> = sqrt (infsum f UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have norm_trunc: \<open>norm (trunc_ell2 S \<psi>) = sqrt (sum f S)\<close> if \<open>finite S\<close> for S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (trunc_ell2 S \<psi>) = sqrt (sum f S)
[PROOF STEP]
using f_def that norm_trunc_ell2_finite
[PROOF STATE]
proof (prove)
using this:
f ?i = (cmod (Rep_ell2 \<psi> ?i))\<^sup>2
finite S
finite ?S \<Longrightarrow> norm (trunc_ell2 ?S ?x) = sqrt (\<Sum>i\<in>?S. (cmod (Rep_ell2 ?x i))\<^sup>2)

goal (1 subgoal):
 1. norm (trunc_ell2 S \<psi>) = sqrt (sum f S)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
finite ?S \<Longrightarrow> norm (trunc_ell2 ?S \<psi>) = sqrt (sum f ?S)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>(sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)
[PROOF STEP]
using f_def[abs_def] infsum_tendsto local.summable
[PROOF STATE]
proof (prove)
using this:
f \<equiv> \<lambda>i. (cmod (Rep_ell2 \<psi> i))\<^sup>2
?f summable_on ?S \<Longrightarrow> (sum ?f \<longlongrightarrow> infsum ?f ?S) (finite_subsets_at_top ?S)
f abs_summable_on UNIV

goal (1 subgoal):
 1. (sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
(sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)
[PROOF STEP]
using tendsto_real_sqrt
[PROOF STATE]
proof (prove)
using this:
(sum f \<longlongrightarrow> infsum f UNIV) (finite_subsets_at_top UNIV)
(?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ((\<lambda>x. sqrt (?f x)) \<longlongrightarrow> sqrt ?x) ?F

goal (1 subgoal):
 1. ((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. norm (trunc_ell2 S \<psi>)) \<longlongrightarrow> norm \<psi>) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. norm (trunc_ell2 S \<psi>)) \<longlongrightarrow> norm \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
apply (subst tendsto_cong[where g=\<open>\<lambda>S. sqrt (sum f S)\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV) \<Longrightarrow> \<forall>\<^sub>F x in finite_subsets_at_top UNIV. norm (trunc_ell2 x \<psi>) = sqrt (sum f x)
 2. ((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> sqrt (infsum f UNIV)) (finite_subsets_at_top UNIV) \<Longrightarrow> ((\<lambda>S. sqrt (sum f S)) \<longlongrightarrow> norm \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
by (auto simp add: eventually_finite_subsets_at_top_weakI norm_trunc norm\<psi>)
[PROOF STATE]
proof (state)
this:
((\<lambda>S. norm (trunc_ell2 S \<psi>)) \<longlongrightarrow> norm \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. norm (trunc_ell2 S \<psi>)) \<longlongrightarrow> norm \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> (norm \<psi>)\<^sup>2) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. norm (trunc_ell2 S \<psi>)) \<longlongrightarrow> norm \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> (norm \<psi>)\<^sup>2) (finite_subsets_at_top UNIV)
[PROOF STEP]
by (simp add: tendsto_power)
[PROOF STATE]
proof (state)
this:
((\<lambda>S. (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> (norm \<psi>)\<^sup>2) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> (norm \<psi>)\<^sup>2) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> (norm \<psi>)\<^sup>2) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
apply (rule tendsto_diff[where a=\<open>(norm \<psi>)^2\<close> and b=\<open>(norm \<psi>)^2\<close>, simplified, rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (norm \<psi>)\<^sup>2) \<longlongrightarrow> (norm \<psi>)\<^sup>2) (finite_subsets_at_top UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. (norm (\<psi> - trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. (norm (\<psi> - trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
unfolding norm_id_minus_trunc_ell2
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. (norm \<psi>)\<^sup>2 - (norm (trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>S. (norm (\<psi> - trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. (norm (\<psi> - trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. norm (\<psi> - trunc_ell2 S \<psi>)) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. (norm (\<psi> - trunc_ell2 S \<psi>))\<^sup>2) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. norm (\<psi> - trunc_ell2 S \<psi>)) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>S. norm (\<psi> - trunc_ell2 S \<psi>)) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. norm (\<psi> - trunc_ell2 S \<psi>)) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. \<psi> - trunc_ell2 S \<psi>) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. norm (\<psi> - trunc_ell2 S \<psi>)) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. \<psi> - trunc_ell2 S \<psi>) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
by (rule tendsto_norm_zero_cancel)
[PROOF STATE]
proof (state)
this:
((\<lambda>S. \<psi> - trunc_ell2 S \<psi>) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. \<psi> - trunc_ell2 S \<psi>) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. \<psi> - trunc_ell2 S \<psi>) \<longlongrightarrow> 0) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
apply (rule Lim_transform2[where f=\<open>\<lambda>_. \<psi>\<close>, rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>_. \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trunc_ell2_norm_mono: \<open>M \<subseteq> N \<Longrightarrow> norm (trunc_ell2 M \<psi>) \<le> norm (trunc_ell2 N \<psi>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subseteq> N \<Longrightarrow> norm (trunc_ell2 M \<psi>) \<le> norm (trunc_ell2 N \<psi>)
[PROOF STEP]
proof (rule power2_le_imp_le[rotated], force, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
fix M N :: \<open>'a set\<close> and \<psi> :: \<open>'a \<Rightarrow> complex\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
assume \<open>M \<subseteq> N\<close> and \<open>has_ell2_norm \<psi>\<close>
[PROOF STATE]
proof (state)
this:
M \<subseteq> N
has_ell2_norm \<psi>

goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
have \<open>(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 = (\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 = (\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2)
[PROOF STEP]
unfolding ell2_norm_square
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>i. (cmod (if i \<in> M then \<psi> i else 0))\<^sup>2) = (\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2)
[PROOF STEP]
apply (rule infsum_cong_neutral)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> M - UNIV \<Longrightarrow> (cmod (\<psi> x))\<^sup>2 = 0
 2. \<And>x. x \<in> UNIV - M \<Longrightarrow> (cmod (if x \<in> M then \<psi> x else 0))\<^sup>2 = 0
 3. \<And>x. x \<in> UNIV \<inter> M \<Longrightarrow> (cmod (if x \<in> M then \<psi> x else 0))\<^sup>2 = (cmod (\<psi> x))\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 = (\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2)

goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 = (\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2)

goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
have \<open>\<dots> \<le> (\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2) \<le> (\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2)
[PROOF STEP]
apply (rule infsum_mono2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>i. (cmod (\<psi> i))\<^sup>2) summable_on M
 2. (\<lambda>i. (cmod (\<psi> i))\<^sup>2) summable_on N
 3. M \<subseteq> N
 4. \<And>x. x \<in> N - M \<Longrightarrow> 0 \<le> (cmod (\<psi> x))\<^sup>2
[PROOF STEP]
using \<open>has_ell2_norm \<psi>\<close> \<open>M \<subseteq> N\<close>
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm \<psi>
M \<subseteq> N

goal (4 subgoals):
 1. (\<lambda>i. (cmod (\<psi> i))\<^sup>2) summable_on M
 2. (\<lambda>i. (cmod (\<psi> i))\<^sup>2) summable_on N
 3. M \<subseteq> N
 4. \<And>x. x \<in> N - M \<Longrightarrow> 0 \<le> (cmod (\<psi> x))\<^sup>2
[PROOF STEP]
by (auto simp add: ell2_norm_square has_ell2_norm_def simp flip: norm_power intro: summable_on_subset_banach)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2) \<le> (\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2)

goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>i\<in>M. (cmod (\<psi> i))\<^sup>2) \<le> (\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2)

goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
have \<open>\<dots> = (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2) = (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
unfolding ell2_norm_square
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2) = (\<Sum>\<^sub>\<infinity>i. (cmod (if i \<in> N then \<psi> i else 0))\<^sup>2)
[PROOF STEP]
apply (rule infsum_cong_neutral)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> UNIV - N \<Longrightarrow> (cmod (if x \<in> N then \<psi> x else 0))\<^sup>2 = 0
 2. \<And>x. x \<in> N - UNIV \<Longrightarrow> (cmod (\<psi> x))\<^sup>2 = 0
 3. \<And>x. x \<in> N \<inter> UNIV \<Longrightarrow> (cmod (\<psi> x))\<^sup>2 = (cmod (if x \<in> N then \<psi> x else 0))\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>i\<in>N. (cmod (\<psi> i))\<^sup>2) = (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2

goal (1 subgoal):
 1. \<And>M N \<psi>. \<lbrakk>M \<subseteq> N; has_ell2_norm \<psi>\<rbrakk> \<Longrightarrow> (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
show \<open>(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2\<close>
[PROOF STATE]
proof (prove)
using this:
(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2

goal (1 subgoal):
 1. (ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
(ell2_norm (\<lambda>i. if i \<in> M then \<psi> i else 0))\<^sup>2 \<le> (ell2_norm (\<lambda>i. if i \<in> N then \<psi> i else 0))\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trunc_ell2_reduces_norm: \<open>norm (trunc_ell2 M \<psi>) \<le> norm \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (trunc_ell2 M \<psi>) \<le> norm \<psi>
[PROOF STEP]
by (metis subset_UNIV trunc_ell2_UNIV trunc_ell2_norm_mono)


[STATEMENT]
lemma trunc_ell2_twice[simp]: \<open>trunc_ell2 M (trunc_ell2 N \<psi>) = trunc_ell2 (M\<inter>N) \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 M (trunc_ell2 N \<psi>) = trunc_ell2 (M \<inter> N) \<psi>
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M N \<psi>. has_ell2_norm \<psi> \<Longrightarrow> (\<lambda>i. if i \<in> M then if i \<in> N then \<psi> i else 0 else 0) = (\<lambda>i. if i \<in> M \<inter> N then \<psi> i else 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma trunc_ell2_union: \<open>trunc_ell2 (M \<union> N) \<psi> = trunc_ell2 M \<psi> + trunc_ell2 N \<psi> - trunc_ell2 (M\<inter>N) \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 (M \<union> N) \<psi> = trunc_ell2 M \<psi> + trunc_ell2 N \<psi> - trunc_ell2 (M \<inter> N) \<psi>
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M N \<psi>. has_ell2_norm \<psi> \<Longrightarrow> (\<lambda>i. if i \<in> M \<union> N then \<psi> i else 0) = (\<lambda>x. (if x \<in> M then \<psi> x else 0) + (if x \<in> N then \<psi> x else 0) - (if x \<in> M \<inter> N then \<psi> x else 0))
[PROOF STEP]
by auto


[STATEMENT]
lemma trunc_ell2_union_disjoint: \<open>M\<inter>N = {} \<Longrightarrow> trunc_ell2 (M \<union> N) \<psi> = trunc_ell2 M \<psi> + trunc_ell2 N \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<inter> N = {} \<Longrightarrow> trunc_ell2 (M \<union> N) \<psi> = trunc_ell2 M \<psi> + trunc_ell2 N \<psi>
[PROOF STEP]
by (simp add: trunc_ell2_union)


[STATEMENT]
lemma trunc_ell2_union_Diff: \<open>M \<subseteq> N \<Longrightarrow> trunc_ell2 (N-M) \<psi> = trunc_ell2 N \<psi> - trunc_ell2 M \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subseteq> N \<Longrightarrow> trunc_ell2 (N - M) \<psi> = trunc_ell2 N \<psi> - trunc_ell2 M \<psi>
[PROOF STEP]
using trunc_ell2_union_disjoint[where M=\<open>N-M\<close> and N=M and \<psi>=\<psi>]
[PROOF STATE]
proof (prove)
using this:
(N - M) \<inter> M = {} \<Longrightarrow> trunc_ell2 (N - M \<union> M) \<psi> = trunc_ell2 (N - M) \<psi> + trunc_ell2 M \<psi>

goal (1 subgoal):
 1. M \<subseteq> N \<Longrightarrow> trunc_ell2 (N - M) \<psi> = trunc_ell2 N \<psi> - trunc_ell2 M \<psi>
[PROOF STEP]
by (simp add: Un_commute inf.commute le_iff_sup)


[STATEMENT]
lemma trunc_ell2_add: \<open>trunc_ell2 M (\<psi> + \<phi>) = trunc_ell2 M \<psi> + trunc_ell2 M \<phi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 M (\<psi> + \<phi>) = trunc_ell2 M \<psi> + trunc_ell2 M \<phi>
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M \<psi> \<phi>. \<lbrakk>has_ell2_norm \<psi>; has_ell2_norm \<phi>\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<in> M then \<psi> i + \<phi> i else 0) = (\<lambda>x. (if x \<in> M then \<psi> x else 0) + (if x \<in> M then \<phi> x else 0))
[PROOF STEP]
by auto


[STATEMENT]
lemma trunc_ell2_scaleC: \<open>trunc_ell2 M (c *\<^sub>C \<psi>) = c *\<^sub>C trunc_ell2 M \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 M (c *\<^sub>C \<psi>) = c *\<^sub>C trunc_ell2 M \<psi>
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M c \<psi>. has_ell2_norm \<psi> \<Longrightarrow> (\<lambda>i. if i \<in> M then c * \<psi> i else 0) = (\<lambda>x. c * (if x \<in> M then \<psi> x else 0))
[PROOF STEP]
by auto


[STATEMENT]
lemma bounded_clinear_trunc_ell2[bounded_clinear]: \<open>bounded_clinear (trunc_ell2 M)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (trunc_ell2 M)
[PROOF STEP]
by (auto intro!: bounded_clinearI[where K=1] trunc_ell2_reduces_norm
      simp: trunc_ell2_add trunc_ell2_scaleC)


[STATEMENT]
lemma trunc_ell2_lim: \<open>((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)
[PROOF STEP]
have \<open>((\<lambda>S. trunc_ell2 S (trunc_ell2 M \<psi>)) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S (trunc_ell2 M \<psi>)) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
using trunc_ell2_lim_at_UNIV
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. trunc_ell2 S ?\<psi>) \<longlongrightarrow> ?\<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S (trunc_ell2 M \<psi>)) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((\<lambda>S. trunc_ell2 S (trunc_ell2 M \<psi>)) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. trunc_ell2 S (trunc_ell2 M \<psi>)) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
have \<open>((\<lambda>S. trunc_ell2 (S\<inter>M) \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. trunc_ell2 S (trunc_ell2 M \<psi>)) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 (S \<inter> M) \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>S. trunc_ell2 (S \<inter> M) \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. trunc_ell2 (S \<inter> M) \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
show \<open>((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. trunc_ell2 (S \<inter> M) \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)
[PROOF STEP]
unfolding filterlim_def
[PROOF STATE]
proof (prove)
using this:
filtermap (\<lambda>S. trunc_ell2 (S \<inter> M) \<psi>) (finite_subsets_at_top UNIV) \<le> nhds (trunc_ell2 M \<psi>)

goal (1 subgoal):
 1. filtermap (\<lambda>S. trunc_ell2 S \<psi>) (finite_subsets_at_top M) \<le> nhds (trunc_ell2 M \<psi>)
[PROOF STEP]
apply (subst (asm) filtermap_filtermap[where g=\<open>\<lambda>S. S\<inter>M\<close>, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filtermap (\<lambda>a. trunc_ell2 a \<psi>) (filtermap (\<lambda>S. S \<inter> M) (finite_subsets_at_top UNIV)) \<le> nhds (trunc_ell2 M \<psi>) \<Longrightarrow> filtermap (\<lambda>S. trunc_ell2 S \<psi>) (finite_subsets_at_top M) \<le> nhds (trunc_ell2 M \<psi>)
[PROOF STEP]
apply (subst (asm) finite_subsets_at_top_inter[where A=M and B=UNIV])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. M \<subseteq> UNIV
 2. filtermap (\<lambda>a. trunc_ell2 a \<psi>) (finite_subsets_at_top M) \<le> nhds (trunc_ell2 M \<psi>) \<Longrightarrow> filtermap (\<lambda>S. trunc_ell2 S \<psi>) (finite_subsets_at_top M) \<le> nhds (trunc_ell2 M \<psi>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) (finite_subsets_at_top M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trunc_ell2_lim_general:
  assumes big: \<open>\<And>G. finite G \<Longrightarrow> G \<subseteq> M \<Longrightarrow> (\<forall>\<^sub>F H in F. H \<supseteq> G)\<close>
  assumes small: \<open>\<forall>\<^sub>F H in F. H \<subseteq> M\<close>
  shows \<open>((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) F\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> trunc_ell2 M \<psi>) F
[PROOF STEP]
proof (rule tendstoI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in F. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
fix e :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in F. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
assume \<open>e > 0\<close>
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in F. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
from trunc_ell2_lim[THEN tendsto_iff[THEN iffD1], rule_format, OF \<open>e > 0\<close>, where M=M and \<psi>=\<psi>]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in finite_subsets_at_top M. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
obtain G where \<open>finite G\<close> and \<open>G \<subseteq> M\<close> and
    close: \<open>dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in finite_subsets_at_top M. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e

goal (1 subgoal):
 1. (\<And>G. \<lbrakk>finite G; G \<subseteq> M; dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in finite_subsets_at_top M. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e \<Longrightarrow> \<exists>G. finite G \<and> G \<subseteq> M \<and> dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
unfolding eventually_finite_subsets_at_top
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X. finite X \<and> X \<subseteq> M \<and> (\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> M \<longrightarrow> dist (trunc_ell2 Y \<psi>) (trunc_ell2 M \<psi>) < e) \<Longrightarrow> \<exists>G. finite G \<and> G \<subseteq> M \<and> dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite G
G \<subseteq> M
dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in F. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
from \<open>finite G\<close> \<open>G \<subseteq> M\<close> and big
[PROOF STATE]
proof (chain)
picking this:
finite G
G \<subseteq> M
\<lbrakk>finite ?G; ?G \<subseteq> M\<rbrakk> \<Longrightarrow> eventually ((\<subseteq>) ?G) F
[PROOF STEP]
have \<open>\<forall>\<^sub>F H in F. H \<supseteq> G\<close>
[PROOF STATE]
proof (prove)
using this:
finite G
G \<subseteq> M
\<lbrakk>finite ?G; ?G \<subseteq> M\<rbrakk> \<Longrightarrow> eventually ((\<subseteq>) ?G) F

goal (1 subgoal):
 1. eventually ((\<subseteq>) G) F
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
eventually ((\<subseteq>) G) F

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in F. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
with small
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F H in F. H \<subseteq> M
eventually ((\<subseteq>) G) F
[PROOF STEP]
have \<open>\<forall>\<^sub>F H in F. H \<subseteq> M \<and> H \<supseteq> G\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F H in F. H \<subseteq> M
eventually ((\<subseteq>) G) F

goal (1 subgoal):
 1. \<forall>\<^sub>F H in F. H \<subseteq> M \<and> G \<subseteq> H
[PROOF STEP]
by (simp add: eventually_conj_iff)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F H in F. H \<subseteq> M \<and> G \<subseteq> H

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in F. dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F H in F. H \<subseteq> M \<and> G \<subseteq> H
[PROOF STEP]
show \<open>\<forall>\<^sub>F H in F. dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F H in F. H \<subseteq> M \<and> G \<subseteq> H

goal (1 subgoal):
 1. \<forall>\<^sub>F H in F. dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
proof (rule eventually_mono)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
assume GHM: \<open>H \<subseteq> M \<and> H \<supseteq> G\<close>
[PROOF STATE]
proof (state)
this:
H \<subseteq> M \<and> G \<subseteq> H

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
have \<open>dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) = norm (trunc_ell2 (M-H) \<psi>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) = norm (trunc_ell2 (M - H) \<psi>)
[PROOF STEP]
by (simp add: GHM dist_ell2_def norm_minus_commute trunc_ell2_union_Diff)
[PROOF STATE]
proof (state)
this:
dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) = norm (trunc_ell2 (M - H) \<psi>)

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) = norm (trunc_ell2 (M - H) \<psi>)

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
have \<open>\<dots> \<le> norm (trunc_ell2 (M-G) \<psi>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (trunc_ell2 (M - H) \<psi>) \<le> norm (trunc_ell2 (M - G) \<psi>)
[PROOF STEP]
by (simp add: Diff_mono GHM trunc_ell2_norm_mono)
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 (M - H) \<psi>) \<le> norm (trunc_ell2 (M - G) \<psi>)

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 (M - H) \<psi>) \<le> norm (trunc_ell2 (M - G) \<psi>)

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
have \<open>\<dots>  = dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (trunc_ell2 (M - G) \<psi>) = dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>)
[PROOF STEP]
by (simp add: \<open>G \<subseteq> M\<close> dist_ell2_def norm_minus_commute trunc_ell2_union_Diff)
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 (M - G) \<psi>) = dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>)

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (trunc_ell2 (M - G) \<psi>) = dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>)

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
have \<open>\<dots> < e\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
using close
[PROOF STATE]
proof (prove)
using this:
dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e

goal (1 subgoal):
 1. dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (trunc_ell2 G \<psi>) (trunc_ell2 M \<psi>) < e

goal (1 subgoal):
 1. \<And>x. x \<subseteq> M \<and> G \<subseteq> x \<Longrightarrow> dist (trunc_ell2 x \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
show \<open>dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e\<close>
[PROOF STATE]
proof (prove)
using this:
dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e

goal (1 subgoal):
 1. dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F H in F. dist (trunc_ell2 H \<psi>) (trunc_ell2 M \<psi>) < e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cinner_ket_left: \<open>(ket i \<bullet>\<^sub>C \<psi>) = Rep_ell2 \<psi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C \<psi> = Rep_ell2 \<psi> i
[PROOF STEP]
apply (transfer fixing: i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> (\<Sum>\<^sub>\<infinity>ia. cnj (if i = ia then 1 else 0) * \<psi> ia) = \<psi> i
[PROOF STEP]
apply (subst infsum_cong_neutral[where T=\<open>{i}\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>\<psi> x. \<lbrakk>has_ell2_norm \<psi>; x \<in> {i} - UNIV\<rbrakk> \<Longrightarrow> ?g36 \<psi> x = 0
 2. \<And>\<psi> x. \<lbrakk>has_ell2_norm \<psi>; x \<in> UNIV - {i}\<rbrakk> \<Longrightarrow> cnj (if i = x then 1 else 0) * \<psi> x = 0
 3. \<And>\<psi> x. \<lbrakk>has_ell2_norm \<psi>; x \<in> UNIV \<inter> {i}\<rbrakk> \<Longrightarrow> cnj (if i = x then 1 else 0) * \<psi> x = ?g36 \<psi> x
 4. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> infsum (?g36 \<psi>) {i} = \<psi> i
[PROOF STEP]
by auto


[STATEMENT]
lemma cinner_ket_right: \<open>(\<psi> \<bullet>\<^sub>C ket i) = cnj (Rep_ell2 \<psi> i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> \<bullet>\<^sub>C ket i = cnj (Rep_ell2 \<psi> i)
[PROOF STEP]
apply (transfer fixing: i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> (\<Sum>\<^sub>\<infinity>ia. cnj (\<psi> ia) * (if i = ia then 1 else 0)) = cnj (\<psi> i)
[PROOF STEP]
apply (subst infsum_cong_neutral[where T=\<open>{i}\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>\<psi> x. \<lbrakk>has_ell2_norm \<psi>; x \<in> {i} - UNIV\<rbrakk> \<Longrightarrow> ?g45 \<psi> x = 0
 2. \<And>\<psi> x. \<lbrakk>has_ell2_norm \<psi>; x \<in> UNIV - {i}\<rbrakk> \<Longrightarrow> cnj (\<psi> x) * (if i = x then 1 else 0) = 0
 3. \<And>\<psi> x. \<lbrakk>has_ell2_norm \<psi>; x \<in> UNIV \<inter> {i}\<rbrakk> \<Longrightarrow> cnj (\<psi> x) * (if i = x then 1 else 0) = ?g45 \<psi> x
 4. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> infsum (?g45 \<psi>) {i} = cnj (\<psi> i)
[PROOF STEP]
by auto


[STATEMENT]
lemma cinner_ket_eqI:
  assumes \<open>\<And>i. cinner (ket i) \<psi> = cinner (ket i) \<phi>\<close>
  shows \<open>\<psi> = \<phi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> = \<phi>
[PROOF STEP]
by (metis Rep_ell2_inject assms cinner_ket_left ext)


[STATEMENT]
lemma norm_ket[simp]: "norm (ket i) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (ket i) = 1
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. ell2_norm (\<lambda>y. if i = y then 1 else 0) = 1
[PROOF STEP]
by (rule ell2_norm_ket)


[STATEMENT]
lemma cinner_ket_same[simp]:
  \<open>(ket i \<bullet>\<^sub>C ket i) = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
have \<open>norm (ket i) = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (ket i) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (ket i) = 1

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
hence \<open>sqrt (cmod (ket i \<bullet>\<^sub>C ket i)) = 1\<close>
[PROOF STATE]
proof (prove)
using this:
norm (ket i) = 1

goal (1 subgoal):
 1. sqrt (cmod (ket i \<bullet>\<^sub>C ket i)) = 1
[PROOF STEP]
by (metis norm_eq_sqrt_cinner)
[PROOF STATE]
proof (state)
this:
sqrt (cmod (ket i \<bullet>\<^sub>C ket i)) = 1

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
hence \<open>cmod (ket i \<bullet>\<^sub>C ket i) = 1\<close>
[PROOF STATE]
proof (prove)
using this:
sqrt (cmod (ket i \<bullet>\<^sub>C ket i)) = 1

goal (1 subgoal):
 1. cmod (ket i \<bullet>\<^sub>C ket i) = 1
[PROOF STEP]
using real_sqrt_eq_1_iff
[PROOF STATE]
proof (prove)
using this:
sqrt (cmod (ket i \<bullet>\<^sub>C ket i)) = 1
(sqrt ?x = 1) = (?x = 1)

goal (1 subgoal):
 1. cmod (ket i \<bullet>\<^sub>C ket i) = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cmod (ket i \<bullet>\<^sub>C ket i) = 1

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cmod (ket i \<bullet>\<^sub>C ket i) = 1

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
have \<open>(ket i \<bullet>\<^sub>C ket i) = cmod (ket i \<bullet>\<^sub>C ket i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))
[PROOF STEP]
have \<open>(ket i \<bullet>\<^sub>C ket i) \<in> \<real>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i \<in> \<real>
[PROOF STEP]
by (simp add: cinner_real)
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C ket i \<in> \<real>

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ket i \<bullet>\<^sub>C ket i \<in> \<real>

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))
[PROOF STEP]
by (metis cinner_ge_zero complex_of_real_cmod)
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cmod (ket i \<bullet>\<^sub>C ket i) = 1
ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod (ket i \<bullet>\<^sub>C ket i) = 1
ket i \<bullet>\<^sub>C ket i = complex_of_real (cmod (ket i \<bullet>\<^sub>C ket i))

goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket i = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C ket i = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthogonal_ket[simp]:
  \<open>is_orthogonal (ket i) (ket j) \<longleftrightarrow> i \<noteq> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_orthogonal (ket i) (ket j) = (i \<noteq> j)
[PROOF STEP]
by (simp add: cinner_ket_left ket.rep_eq)


[STATEMENT]
lemma cinner_ket: \<open>(ket i \<bullet>\<^sub>C ket j) = (if i=j then 1 else 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C ket j = (if i = j then 1 else 0)
[PROOF STEP]
by (simp add: cinner_ket_left ket.rep_eq)


[STATEMENT]
lemma ket_injective[simp]: \<open>ket i = ket j \<longleftrightarrow> i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ket i = ket j) = (i = j)
[PROOF STEP]
by (metis cinner_ket one_neq_zero)


[STATEMENT]
lemma inj_ket[simp]: \<open>inj ket\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj ket
[PROOF STEP]
by (simp add: inj_on_def)


[STATEMENT]
lemma trunc_ell2_ket_cspan:
  \<open>trunc_ell2 S x \<in> (cspan (range ket))\<close> if \<open>finite S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 S x \<in> cspan (range ket)
[PROOF STEP]
proof (use that in induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trunc_ell2 {} x \<in> cspan (range ket)
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; trunc_ell2 F x \<in> cspan (range ket)\<rbrakk> \<Longrightarrow> trunc_ell2 (insert xa F) x \<in> cspan (range ket)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. trunc_ell2 {} x \<in> cspan (range ket)
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; trunc_ell2 F x \<in> cspan (range ket)\<rbrakk> \<Longrightarrow> trunc_ell2 (insert xa F) x \<in> cspan (range ket)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 {} x \<in> cspan (range ket)
[PROOF STEP]
by (auto intro: complex_vector.span_zero)
[PROOF STATE]
proof (state)
this:
trunc_ell2 {} x \<in> cspan (range ket)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; trunc_ell2 F x \<in> cspan (range ket)\<rbrakk> \<Longrightarrow> trunc_ell2 (insert xa F) x \<in> cspan (range ket)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; trunc_ell2 F x \<in> cspan (range ket)\<rbrakk> \<Longrightarrow> trunc_ell2 (insert xa F) x \<in> cspan (range ket)
[PROOF STEP]
case (insert a F)
[PROOF STATE]
proof (state)
this:
finite F
a \<notin> F
trunc_ell2 F x \<in> cspan (range ket)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; trunc_ell2 F x \<in> cspan (range ket)\<rbrakk> \<Longrightarrow> trunc_ell2 (insert xa F) x \<in> cspan (range ket)
[PROOF STEP]
from insert.hyps
[PROOF STATE]
proof (chain)
picking this:
finite F
a \<notin> F
[PROOF STEP]
have \<open>trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *\<^sub>C ket a\<close>
[PROOF STATE]
proof (prove)
using this:
finite F
a \<notin> F

goal (1 subgoal):
 1. trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *\<^sub>C ket a
[PROOF STEP]
apply (transfer fixing: F a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite F; a \<notin> F; has_ell2_norm x\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<in> insert a F then x i else 0) = (\<lambda>xa. (if xa \<in> F then x xa else 0) + x a * (if a = xa then 1 else 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *\<^sub>C ket a

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; trunc_ell2 F x \<in> cspan (range ket)\<rbrakk> \<Longrightarrow> trunc_ell2 (insert xa F) x \<in> cspan (range ket)
[PROOF STEP]
with insert.IH
[PROOF STATE]
proof (chain)
picking this:
trunc_ell2 F x \<in> cspan (range ket)
trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *\<^sub>C ket a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
trunc_ell2 F x \<in> cspan (range ket)
trunc_ell2 (insert a F) x = trunc_ell2 F x + Rep_ell2 x a *\<^sub>C ket a

goal (1 subgoal):
 1. trunc_ell2 (insert a F) x \<in> cspan (range ket)
[PROOF STEP]
by (simp add: complex_vector.span_add_eq complex_vector.span_base complex_vector.span_scale)
[PROOF STATE]
proof (state)
this:
trunc_ell2 (insert a F) x \<in> cspan (range ket)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closed_cspan_range_ket[simp]:
  \<open>closure (cspan (range ket)) = UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (cspan (range ket)) = UNIV
[PROOF STEP]
proof (intro set_eqI iffI UNIV_I closure_approachable[THEN iffD2] allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
fix \<psi> :: \<open>'a ell2\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
fix e :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
assume \<open>e > 0\<close>
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
have \<open>((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
by (rule trunc_ell2_lim_at_UNIV)
[PROOF STATE]
proof (state)
this:
((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)
[PROOF STEP]
obtain F where \<open>finite F\<close> and \<open>dist (trunc_ell2 F \<psi>) \<psi> < e\<close>
[PROOF STATE]
proof (prove)
using this:
((\<lambda>S. trunc_ell2 S \<psi>) \<longlongrightarrow> \<psi>) (finite_subsets_at_top UNIV)

goal (1 subgoal):
 1. (\<And>F. \<lbrakk>finite F; dist (trunc_ell2 F \<psi>) \<psi> < e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (drule_tac tendstoD[OF _ \<open>e > 0\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>F. \<lbrakk>finite F; dist (trunc_ell2 F \<psi>) \<psi> < e\<rbrakk> \<Longrightarrow> thesis; \<forall>\<^sub>F x in finite_subsets_at_top UNIV. dist (trunc_ell2 x \<psi>) \<psi> < e\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: simp: eventually_finite_subsets_at_top)
[PROOF STATE]
proof (state)
this:
finite F
dist (trunc_ell2 F \<psi>) \<psi> < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite F
dist (trunc_ell2 F \<psi>) \<psi> < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
have \<open>trunc_ell2 F \<psi> \<in> cspan (range ket)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trunc_ell2 F \<psi> \<in> cspan (range ket)
[PROOF STEP]
using \<open>finite F\<close> trunc_ell2_ket_cspan
[PROOF STATE]
proof (prove)
using this:
finite F
finite ?S \<Longrightarrow> trunc_ell2 ?S ?x \<in> cspan (range ket)

goal (1 subgoal):
 1. trunc_ell2 F \<psi> \<in> cspan (range ket)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trunc_ell2 F \<psi> \<in> cspan (range ket)

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>x \<in> UNIV; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>cspan (range ket). dist y x < e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite F
dist (trunc_ell2 F \<psi>) \<psi> < e
trunc_ell2 F \<psi> \<in> cspan (range ket)
[PROOF STEP]
show \<open>\<exists>\<phi>\<in>cspan (range ket). dist \<phi> \<psi> < e\<close>
[PROOF STATE]
proof (prove)
using this:
finite F
dist (trunc_ell2 F \<psi>) \<psi> < e
trunc_ell2 F \<psi> \<in> cspan (range ket)

goal (1 subgoal):
 1. \<exists>\<phi>\<in>cspan (range ket). dist \<phi> \<psi> < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<phi>\<in>cspan (range ket). dist \<phi> \<psi> < e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ccspan_range_ket[simp]: "ccspan (range ket) = (top::('a ell2 ccsubspace))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccspan (range ket) = \<top>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ccspan (range ket) = \<top>
[PROOF STEP]
have \<open>closure (complex_vector.span (range ket)) = (UNIV::'a ell2 set)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (cspan (range ket)) = UNIV
[PROOF STEP]
using Complex_L2.closed_cspan_range_ket
[PROOF STATE]
proof (prove)
using this:
closure (cspan (range ket)) = UNIV

goal (1 subgoal):
 1. closure (cspan (range ket)) = UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closure (cspan (range ket)) = UNIV

goal (1 subgoal):
 1. ccspan (range ket) = \<top>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
closure (cspan (range ket)) = UNIV

goal (1 subgoal):
 1. ccspan (range ket) = \<top>
[PROOF STEP]
by (simp add: ccspan.abs_eq top_ccsubspace.abs_eq)
[PROOF STATE]
proof (state)
this:
ccspan (range ket) = \<top>

goal:
No subgoals!
[PROOF STEP]
qed