Theory HS2Ell2
section ‹‹HS2Ell2› -- Representing any Hilbert space as $\ell_2(X)$›
theory HS2Ell2
imports Complex_Bounded_Operators.Complex_L2
begin
unbundle cblinfun_syntax
typedef (overloaded) 'a::‹{chilbert_space, not_singleton}› chilbert2ell2 = ‹some_chilbert_basis :: 'a set›
using some_chilbert_basis_nonempty by auto
definition ell2_to_hilbert where ‹ell2_to_hilbert = cblinfun_extension (range ket) (Rep_chilbert2ell2 o inv ket)›
lemma ell2_to_hilbert_ket: ‹ell2_to_hilbert *⇩V ket x = Rep_chilbert2ell2 x›
proof -
have ‹cblinfun_extension_exists (range ket) (Rep_chilbert2ell2 o inv ket)›
proof (rule cblinfun_extension_exists_ortho[where B=1])
fix x y :: "'b chilbert2ell2 ell2"
assume "x ∈ range ket" "y ∈ range ket" "x ≠ y"
then obtain x' y' where x'_y': "x = ket x'" "y = ket y'" "x' ≠ y'"
by auto
have "is_orthogonal (Rep_chilbert2ell2 x') (Rep_chilbert2ell2 y')"
by (meson Rep_chilbert2ell2 Rep_chilbert2ell2_inject ‹x' ≠ y'› is_ortho_set_def is_ortho_set_some_chilbert_basis)
thus "is_orthogonal ((Rep_chilbert2ell2 ∘ inv ket) x) ((Rep_chilbert2ell2 ∘ inv ket) y)"
using x'_y' by auto
qed (auto simp: Rep_chilbert2ell2 is_normal_some_chilbert_basis)
from cblinfun_extension_apply[OF this]
have "cblinfun_extension (range ket) (Rep_chilbert2ell2 ∘ inv ket) *⇩V (ket x) =
(Rep_chilbert2ell2 ∘ inv ket) (ket x)"
by blast
thus ?thesis
by (simp add: ell2_to_hilbert_def)
qed
lemma norm_ell2_to_hilbert: ‹norm ell2_to_hilbert = 1›
proof (rule order.antisym)
show ‹norm ell2_to_hilbert ≤ 1›
unfolding ell2_to_hilbert_def
proof (rule cblinfun_extension_exists_ortho_norm[where B=1])
fix x y :: "'b chilbert2ell2 ell2"
assume "x ∈ range ket" "y ∈ range ket" "x ≠ y"
then obtain x' y' where x'_y': "x = ket x'" "y = ket y'" "x' ≠ y'"
by auto
have "is_orthogonal (Rep_chilbert2ell2 x') (Rep_chilbert2ell2 y')"
by (meson Rep_chilbert2ell2 Rep_chilbert2ell2_inject ‹x' ≠ y'› is_ortho_set_def is_ortho_set_some_chilbert_basis)
thus "is_orthogonal ((Rep_chilbert2ell2 ∘ inv ket) x) ((Rep_chilbert2ell2 ∘ inv ket) y)"
using x'_y' by auto
qed (auto simp: Rep_chilbert2ell2 is_normal_some_chilbert_basis)
show ‹norm ell2_to_hilbert ≥ 1›
by (rule cblinfun_norm_geqI[where x=‹ket undefined›])
(auto simp: ell2_to_hilbert_ket Rep_chilbert2ell2 is_normal_some_chilbert_basis)
qed
lemma unitary_ell2_to_hilbert[simp]: ‹unitary ell2_to_hilbert›
proof (rule surj_isometry_is_unitary)
show ‹isometry (ell2_to_hilbert :: 'a chilbert2ell2 ell2 ⇒⇩C⇩L _)›
proof (rule orthogonal_on_basis_is_isometry)
show ‹ccspan (range ket) = top›
by auto
fix x y :: ‹'a chilbert2ell2 ell2›
assume ‹x ∈ range ket› ‹y ∈ range ket›
then obtain x' y' where [simp]: ‹x = ket x'› ‹y = ket y'›
by auto
show ‹(ell2_to_hilbert *⇩V x) ∙⇩C (ell2_to_hilbert *⇩V y) = x ∙⇩C y›
proof (cases ‹x'=y'›)
case True
hence "Rep_chilbert2ell2 y' ∙⇩C Rep_chilbert2ell2 y' = 1 "
using Rep_chilbert2ell2 cnorm_eq_1 is_normal_some_chilbert_basis by blast
then show ?thesis using True
by (auto simp: ell2_to_hilbert_ket)
next
case False
hence "is_orthogonal (Rep_chilbert2ell2 x') (Rep_chilbert2ell2 y') "
by (metis Rep_chilbert2ell2 Rep_chilbert2ell2_inject is_ortho_set_def is_ortho_set_some_chilbert_basis)
then show ?thesis
using False by (auto simp: ell2_to_hilbert_ket cinner_ket)
qed
qed
have ‹cblinfun_apply ell2_to_hilbert ` range ket ⊇ some_chilbert_basis›
by (metis Rep_chilbert2ell2_cases UNIV_I ell2_to_hilbert_ket image_eqI subsetI)
then have ‹ell2_to_hilbert *⇩S top ≥ ccspan some_chilbert_basis› (is ‹_ ≥ …›)
by (smt (verit, del_insts) cblinfun_image_ccspan ccspan_mono ccspan_range_ket)
also have ‹… = top›
by simp
finally show ‹ell2_to_hilbert *⇩S top = top›
by (simp add: top.extremum_unique)
qed
lemma ell2_to_hilbert_adj_ket: ‹ell2_to_hilbert* *⇩V ψ = ket (Abs_chilbert2ell2 ψ)› if ‹ψ ∈ some_chilbert_basis›
using ell2_to_hilbert_ket unitary_ell2_to_hilbert
by (metis (no_types, lifting) cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply that type_definition.Abs_inverse type_definition_chilbert2ell2 unitaryD1)
definition ‹cr_chilbert2ell2_ell2 x y ⟷ ell2_to_hilbert *⇩V x = y›
lemma bi_unique_cr_chilbert2ell2_ell2[transfer_rule]: ‹bi_unique cr_chilbert2ell2_ell2›
by (metis (no_types, opaque_lifting) bi_unique_def cblinfun_apply_cblinfun_compose cr_chilbert2ell2_ell2_def id_cblinfun_apply unitaryD1 unitary_ell2_to_hilbert)
lemma bi_total_cr_chilbert2ell2_ell2[transfer_rule]: ‹bi_total cr_chilbert2ell2_ell2›
by (metis (no_types, opaque_lifting) bi_total_def cblinfun_apply_cblinfun_compose cr_chilbert2ell2_ell2_def id_cblinfun_apply unitaryD2 unitary_ell2_to_hilbert)
named_theorems c2l2l2
lemma c2l2l2_cinner[c2l2l2]:
includes lifting_syntax
shows ‹(cr_chilbert2ell2_ell2 ===> cr_chilbert2ell2_ell2 ===> (=)) cinner cinner›
proof -
have *: ‹ket x ∙⇩C ket y = (ell2_to_hilbert *⇩V ket x) ∙⇩C (ell2_to_hilbert *⇩V ket y)› for x y :: ‹'a chilbert2ell2›
by (metis Rep_chilbert2ell2 Rep_chilbert2ell2_inverse cinner_adj_right ell2_to_hilbert_adj_ket ell2_to_hilbert_ket)
have ‹x ∙⇩C y = (ell2_to_hilbert *⇩V x) ∙⇩C (ell2_to_hilbert *⇩V y) › for x y :: ‹'a chilbert2ell2 ell2›
apply (rule fun_cong[where x=x])
apply (rule bounded_antilinear_equal_ket)
apply (intro bounded_linear_intros)
apply (intro bounded_linear_intros)
apply (rule fun_cong[where x=y])
apply (rule bounded_clinear_equal_ket)
apply (intro bounded_linear_intros)
apply (intro bounded_linear_intros)
by (simp add: *)
then show ?thesis
by (auto intro!: rel_funI simp: cr_chilbert2ell2_ell2_def)
qed
lemma c2l2l2_norm[c2l2l2]:
includes lifting_syntax
shows ‹(cr_chilbert2ell2_ell2 ===> (=)) norm norm›
apply (subst norm_eq_sqrt_cinner[abs_def])
apply (subst (2) norm_eq_sqrt_cinner[abs_def])
using c2l2l2_cinner[transfer_rule] apply fail?
by transfer_prover
lemma c2l2l2_scaleC[c2l2l2]:
includes lifting_syntax
shows ‹((=) ===> cr_chilbert2ell2_ell2 ===> cr_chilbert2ell2_ell2) scaleC scaleC›
proof -
have ‹ell2_to_hilbert *⇩V c *⇩C x = c *⇩C (ell2_to_hilbert *⇩V x)› for c and x :: ‹'a chilbert2ell2 ell2›
by (simp add: cblinfun.scaleC_right)
then show ?thesis
by (auto intro!: rel_funI simp: cr_chilbert2ell2_ell2_def)
qed
lemma c2l2l2_zero[c2l2l2]:
includes lifting_syntax
shows ‹cr_chilbert2ell2_ell2 0 0›
unfolding cr_chilbert2ell2_ell2_def by simp
lemma c2l2l2_is_ortho_set[c2l2l2]:
includes lifting_syntax
shows ‹(rel_set cr_chilbert2ell2_ell2 ===> (=)) is_ortho_set (is_ortho_set :: 'a::{chilbert_space,not_singleton} set ⇒ bool)›
unfolding is_ortho_set_def
using c2l2l2[where 'a='a, transfer_rule] apply fail?
by transfer_prover
lemma c2l2l2_ccspan[c2l2l2]:
includes lifting_syntax
shows ‹(rel_set cr_chilbert2ell2_ell2 ===> rel_ccsubspace cr_chilbert2ell2_ell2) ccspan ccspan›
proof (rule rel_funI, rename_tac A B)
fix A and B :: ‹'a set›
assume ‹rel_set cr_chilbert2ell2_ell2 A B›
then have ‹B = ell2_to_hilbert ` A›
by (metis (no_types, lifting) bi_unique_cr_chilbert2ell2_ell2 bi_unique_rel_set_lemma cr_chilbert2ell2_ell2_def image_cong)
then have ‹space_as_set (ccspan B) = ell2_to_hilbert ` space_as_set (ccspan A)›
by (subst space_as_set_image_commute[where V=‹ell2_to_hilbert*›])
(auto intro: unitaryD2 simp: cblinfun_image_ccspan)
then have ‹rel_set cr_chilbert2ell2_ell2 (space_as_set (ccspan A)) (space_as_set (ccspan B))›
by (smt (verit, best) cr_chilbert2ell2_ell2_def image_iff rel_setI)
then show ‹rel_ccsubspace cr_chilbert2ell2_ell2 (ccspan A) (ccspan B)›
by (simp add: rel_ccsubspace_def)
qed
lemma ell2_to_hilbert_adj_ell2_to_hilbert [simp]: "ell2_to_hilbert* *⇩V ell2_to_hilbert *⇩V x = x"
using unitary_ell2_to_hilbert unfolding unitary_def
by (metis cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply)
lemma ell2_to_hilbert_ell2_to_hilbert_adj [simp]: "ell2_to_hilbert *⇩V ell2_to_hilbert* *⇩V x = x"
using unitary_ell2_to_hilbert unfolding unitary_def
by (metis cblinfun_apply_cblinfun_compose cblinfun_id_cblinfun_apply)
lemma bi_total_rel_ccsubspace_cr_chilbert2ell2_ell2[transfer_rule]:
‹bi_total (rel_ccsubspace cr_chilbert2ell2_ell2)›
apply (rule bi_totalI)
subgoal
by (rule left_total_rel_ccsubspace[where U=ell2_to_hilbert and V=‹ell2_to_hilbert*›])
(auto simp: cr_chilbert2ell2_ell2_def)[3]
subgoal
by (rule right_total_rel_ccsubspace[where U=‹ell2_to_hilbert*› and V=‹ell2_to_hilbert›])
(auto simp: cr_chilbert2ell2_ell2_def)
done
lemma c2l2l2_top[c2l2l2]:
includes lifting_syntax
shows ‹(rel_ccsubspace cr_chilbert2ell2_ell2) top top›
unfolding rel_ccsubspace_def
by (simp add: UNIV_transfer bi_total_cr_chilbert2ell2_ell2)
lemma c2l2l2_is_onb[c2l2l2]:
includes lifting_syntax
shows ‹(rel_set cr_chilbert2ell2_ell2 ===> (=)) is_onb is_onb›
unfolding is_onb_def
using c2l2l2[where 'a='a, transfer_rule] apply fail?
by transfer_prover
unbundle no cblinfun_syntax
end