# Theory One_Dimensional_Spaces

```section ‹‹One_Dimensional_Spaces› -- One dimensional complex vector spaces›

theory One_Dimensional_Spaces
imports
Complex_Inner_Product
"Complex_Bounded_Operators.Extra_Operator_Norm"
begin

text ‹The class ‹one_dim› applies to one-dimensional vector spaces.
Those are additionally interpreted as \<^class>‹complex_algebra_1›s
via the canonical isomorphism between a one-dimensional vector space and
\<^typ>‹complex›.›
class one_dim = onb_enum + one + times + inverse +
assumes one_dim_canonical_basis[simp]: "canonical_basis = [1]"
assumes one_dim_prod_scale1: "(a *⇩C 1) * (b *⇩C 1) = (a * b) *⇩C 1"
assumes divide_inverse: "x / y = x * inverse y"
assumes one_dim_inverse: "inverse (a *⇩C 1) = inverse a *⇩C 1"

hide_fact (open) divide_inverse
― ‹@{thm [source] divide_inverse} from class \<^class>‹field›, instantiated below, subsumes this fact.›

instance complex :: one_dim
apply intro_classes
unfolding canonical_basis_complex_def is_ortho_set_def
by (auto simp: divide_complex_def)

lemma one_cinner_one[simp]: ‹(1::('a::one_dim)) ∙⇩C 1 = 1›
proof-
include notation_norm
have ‹(canonical_basis::'a list) = [1::('a::one_dim)]›
by simp
hence ‹∥1::'a::one_dim∥ = 1›
by (metis is_normal list.set_intros(1))
hence ‹∥1::'a::one_dim∥^2 = 1›
by simp
moreover have  ‹∥(1::('a::one_dim))∥^2 = (1::('a::one_dim)) ∙⇩C 1›
by (metis cnorm_eq_square)
ultimately show ?thesis by simp
qed

lemma one_cinner_a_scaleC_one[simp]: ‹((1::'a::one_dim) ∙⇩C a) *⇩C 1 = a›
proof-
have ‹(canonical_basis::'a list) = [1]›
by simp
hence r2: ‹a ∈ complex_vector.span ({1::'a})›
using  iso_tuple_UNIV_I empty_set is_generator_set list.simps(15)
by metis
have "(1::'a) ∉ {}"
by (metis equals0D)
hence r1: ‹∃ s. a = s *⇩C 1›
by (metis Diff_insert_absorb r2 complex_vector.span_breakdown
complex_vector.span_empty eq_iff_diff_eq_0 singleton_iff)
then obtain s where s_def: ‹a = s *⇩C 1›
by blast
have  ‹(1::'a) ∙⇩C a = (1::'a) ∙⇩C (s *⇩C 1)›
using ‹a = s *⇩C 1›
by simp
also have ‹… = s * ((1::'a) ∙⇩C 1)›
by simp
also have ‹… = s›
using one_cinner_one by auto
finally show ?thesis
by (simp add: s_def)
qed

lemma one_dim_apply_is_times_def:
"ψ * φ = ((1 ∙⇩C ψ) * (1 ∙⇩C φ)) *⇩C 1" for ψ :: ‹'a::one_dim›
by (metis one_cinner_a_scaleC_one one_dim_prod_scale1)

instance one_dim ⊆ complex_algebra_1
proof
fix x y z :: ‹'a::one_dim› and c :: complex
show "(x * y) * z = x * (y * z)"
by (simp add: one_dim_apply_is_times_def[where ?'a='a])
show "(x + y) * z = x * z + y * z"
by (metis (no_types, lifting) cinner_simps(2) complex_vector.vector_space_assms(2) complex_vector.vector_space_assms(3) one_dim_apply_is_times_def)
show "x * (y + z) = x * y + x * z"
by (metis (mono_tags, lifting) cinner_simps(2) complex_vector.vector_space_assms(2) distrib_left one_dim_apply_is_times_def)
show "(c *⇩C x) * y = c *⇩C (x * y)"
by (simp add: one_dim_apply_is_times_def[where ?'a='a])
show "x * (c *⇩C y) = c *⇩C (x * y)"
by (simp add: one_dim_apply_is_times_def[where ?'a='a])
show "1 * x = x"
by (metis mult.left_neutral one_cinner_a_scaleC_one one_cinner_one one_dim_apply_is_times_def)
show "x * 1 = x"
by (simp add: one_dim_apply_is_times_def [where ?'a = 'a])
show "(0::'a) ≠ 1"
by (metis cinner_eq_zero_iff one_cinner_one zero_neq_one)
qed

instance one_dim ⊆ complex_normed_algebra
proof
fix x y :: ‹'a::one_dim›
show "norm (x * y) ≤ norm x * norm y"
proof-
have r1:  "cmod ((1::'a) ∙⇩C x) ≤ norm (1::'a) * norm x"
by (simp add: complex_inner_class.Cauchy_Schwarz_ineq2)
have r2: "cmod ((1::'a) ∙⇩C y) ≤ norm (1::'a) * norm y"
by (simp add: complex_inner_class.Cauchy_Schwarz_ineq2)

have q1: "(1::'a) ∙⇩C 1 = 1"
by simp
hence "(norm (1::'a))^2 = 1"
by (simp add: cnorm_eq_1 power2_eq_1_iff)
hence "norm (1::'a) = 1"
by (smt abs_norm_cancel power2_eq_1_iff)
hence "cmod (((1::'a) ∙⇩C x) * ((1::'a) ∙⇩C y)) * norm (1::'a) = cmod (((1::'a) ∙⇩C x) * ((1::'a) ∙⇩C y))"
by simp
also have "… = cmod (((1::'a) ∙⇩C x)) * cmod (((1::'a) ∙⇩C y))"
by (simp add: norm_mult)
also have "… ≤ norm (1::'a) * norm x * norm (1::'a) * norm y"
by (smt ‹norm 1 = 1› mult.commute mult_cancel_right1 norm_scaleC one_cinner_a_scaleC_one)
also have "… = norm x * norm y"
by (simp add: ‹norm 1 = 1›)
finally show ?thesis
by (simp add: one_dim_apply_is_times_def[where ?'a='a])
qed
qed

instance one_dim ⊆ complex_normed_algebra_1
proof intro_classes
show "norm (1::'a) = 1"
by (metis complex_inner_1_left norm_eq_sqrt_cinner norm_one one_cinner_one)
qed

text ‹This is the canonical isomorphism between any two one dimensional spaces. Specifically,
if 1 denotes the element of the canonical basis (which is specified by type class \<^class>‹basis_enum›),
then \<^term>‹one_dim_iso› is the unique isomorphism that maps 1 to 1.›
definition one_dim_iso :: "'a::one_dim ⇒ 'b::one_dim"
where "one_dim_iso a = of_complex (1 ∙⇩C a)"

lemma one_dim_iso_idem[simp]: "one_dim_iso (one_dim_iso x) = one_dim_iso x"
by (simp add: one_dim_iso_def)

lemma one_dim_iso_id[simp]: "one_dim_iso = id"
unfolding one_dim_iso_def
by (auto simp add: of_complex_def)

by (simp add: one_dim_iso_def of_complex_def)

lemma one_dim_iso_is_of_complex[simp]: "one_dim_iso = of_complex"
unfolding one_dim_iso_def by auto

lemma of_complex_one_dim_iso[simp]: "of_complex (one_dim_iso ψ) = one_dim_iso ψ"
by (metis one_dim_iso_is_of_complex one_dim_iso_idem)

lemma one_dim_iso_of_complex[simp]: "one_dim_iso (of_complex c) = of_complex c"
by (metis one_dim_iso_is_of_complex one_dim_iso_idem)

‹one_dim_iso (a + b) = one_dim_iso a + one_dim_iso b›
by (simp add: cinner_simps(2) one_dim_iso_def)

lemma one_dim_iso_minus[simp]:
‹one_dim_iso (a - b) = one_dim_iso a - one_dim_iso b›
by (simp add: cinner_simps(3) one_dim_iso_def)

lemma one_dim_iso_scaleC[simp]: "one_dim_iso (c *⇩C ψ) = c *⇩C one_dim_iso ψ"
by (metis cinner_scaleC_right of_complex_mult one_dim_iso_def scaleC_conv_of_complex)

lemma clinear_one_dim_iso[simp]: "clinear one_dim_iso"
by (rule clinearI, auto)

lemma bounded_clinear_one_dim_iso[simp]: "bounded_clinear one_dim_iso"
proof (rule bounded_clinear_intro [where K = 1] , auto)
fix x :: ‹'a::one_dim›
show "norm (one_dim_iso x) ≤ norm x"
by (metis (full_types) norm_of_complex of_complex_def one_cinner_a_scaleC_one one_dim_iso_def
order_refl)
qed

lemma one_dim_iso_of_one[simp]: "one_dim_iso 1 = 1"
by (simp add: one_dim_iso_def)

lemma onorm_one_dim_iso[simp]: "onorm one_dim_iso = 1"
proof (rule onormI [where b = 1 and x = 1])
fix x :: ‹'a::one_dim›
have "norm (one_dim_iso x ::'b) ≤ norm x"
by (metis eq_iff norm_of_complex of_complex_def one_cinner_a_scaleC_one one_dim_iso_def)
thus "norm (one_dim_iso (x::'a)::'b) ≤ 1 * norm x"
by auto
show "(1::'a) ≠ 0"
by simp
show "norm (one_dim_iso (1::'a)::'b) = 1 * norm (1::'a)"
by auto
qed

lemma one_dim_iso_times[simp]: "one_dim_iso (ψ * φ) = one_dim_iso ψ * one_dim_iso φ"
by (metis mult.left_neutral mult_scaleC_left of_complex_def one_cinner_a_scaleC_one one_dim_iso_def one_dim_iso_scaleC)

lemma one_dim_iso_of_zero[simp]: "one_dim_iso 0 = 0"
by (simp add: complex_vector.linear_0)

lemma one_dim_iso_of_zero': "one_dim_iso x = 0 ⟹ x = 0"
by (metis of_complex_def of_complex_eq_0_iff one_cinner_a_scaleC_one one_dim_iso_def)

lemma one_dim_scaleC_1[simp]: "one_dim_iso x *⇩C 1 = x"
by (simp add: one_dim_iso_def)

lemma one_dim_clinear_eqI:
assumes "(x::'a::one_dim) ≠ 0" and "clinear f" and "clinear g" and "f x = g x"
shows "f = g"
proof (rule ext)
fix y :: 'a
from ‹f x = g x›
have ‹one_dim_iso x *⇩C f 1 = one_dim_iso x *⇩C g 1›
by (metis assms(2) assms(3) complex_vector.linear_scale one_dim_scaleC_1)
hence "f 1 = g 1"
using assms(1) one_dim_iso_of_zero' by auto
then show "f y = g y"
by (metis assms(2) assms(3) complex_vector.linear_scale one_dim_scaleC_1)
qed

lemma one_dim_norm: "norm x = cmod (one_dim_iso x)"
proof (subst one_dim_scaleC_1 [symmetric])
show "norm (one_dim_iso x *⇩C (1::'a)) = cmod (one_dim_iso x)"
by (metis norm_of_complex of_complex_def)
qed

lemma norm_one_dim_iso[simp]: ‹norm (one_dim_iso x) = norm x›
by (metis norm_of_complex of_complex_one_dim_iso one_dim_norm)

lemma one_dim_onorm:
fixes f :: "'a::one_dim ⇒ 'b::complex_normed_vector"
assumes "clinear f"
shows "onorm f = norm (f 1)"
proof (rule onormI[where x=1])
fix x :: 'a
have "norm x * norm (f 1) ≤ norm (f 1) * norm x"
by simp
hence "norm (f (one_dim_iso x *⇩C 1)) ≤ norm (f 1) * norm x"
by (metis (mono_tags, lifting) assms complex_vector.linear_scale norm_scaleC one_dim_norm)
thus "norm (f x) ≤ norm (f 1) * norm x"
by (subst one_dim_scaleC_1 [symmetric])
qed auto

lemma one_dim_onorm':
fixes f :: "'a::one_dim ⇒ 'b::one_dim"
assumes "clinear f"
shows "onorm f = cmod (one_dim_iso (f 1))"
using assms one_dim_norm one_dim_onorm by fastforce

instance one_dim ⊆ zero_neq_one ..

lemma one_dim_iso_inj: "one_dim_iso x = one_dim_iso y ⟹ x = y"
by (metis one_dim_iso_idem one_dim_scaleC_1)

instance one_dim ⊆ comm_ring
proof intro_classes
fix x y z :: 'a
show "x * y = y * x"
by (metis one_dim_apply_is_times_def ordered_field_class.sign_simps(5))
show "(x + y) * z = x * z + y * z"
by (simp add: ring_class.ring_distribs(2))
qed

instance one_dim ⊆ field
proof intro_classes
fix x y z :: ‹'a::one_dim›
show "1 * x = x"
by simp

have "(inverse ((1::'a) ∙⇩C x) * ((1::'a) ∙⇩C x)) *⇩C (1::'a) = 1" if "x ≠ 0"
by (metis left_inverse of_complex_def one_cinner_a_scaleC_one one_dim_iso_of_zero
one_dim_iso_is_of_complex one_dim_iso_of_one that)
hence "inverse (((1::'a) ∙⇩C x) *⇩C 1) * ((1::'a) ∙⇩C x) *⇩C 1 = (1::'a)" if "x ≠ 0"
by (metis one_dim_inverse one_dim_prod_scale1 that)
hence "inverse (((1::'a) ∙⇩C x) *⇩C 1) * x = 1" if "x ≠ 0"
using one_cinner_a_scaleC_one[of x, symmetric] that by auto
thus "inverse x * x = 1" if "x ≠ 0"
by (simp add: that)
show "x / y = x * inverse y"
by (simp add: one_dim_class.divide_inverse)
show "inverse (0::'a) = 0"
by (subst complex_vector.scale_zero_left[symmetric], subst one_dim_inverse, simp)
qed

instance one_dim ⊆ complex_normed_field
proof intro_classes
fix x y :: 'a
show "norm (x * y) = norm x * norm y"
by (metis norm_mult one_dim_iso_times one_dim_norm)
qed

instance one_dim ⊆ chilbert_space..

lemma ccspan_one_dim[simp]: ‹ccspan {x} = top› if ‹x ≠ 0› for x :: ‹_ :: one_dim›
proof -
have ‹y ∈ cspan {x}› for y
using that by (metis complex_vector.span_base complex_vector.span_zero cspan_singleton_scaleC insertI1 one_dim_scaleC_1 scaleC_zero_left)
then show ?thesis
by (auto intro!: order.antisym ccsubspace_leI
simp: top_ccsubspace.rep_eq ccspan.rep_eq)
qed

lemma one_dim_ccsubspace_all_or_nothing: ‹A = bot ∨ A = top› for A :: ‹_::one_dim ccsubspace›
proof (rule Meson.disj_comm, rule disjCI)
assume ‹A ≠ bot›
then obtain ψ where ‹ψ ∈ space_as_set A› and ‹ψ ≠ 0›
by (metis ccsubspace_eqI singleton_iff space_as_set_bot zero_space_as_set)
then have ‹A ≥ ccspan {ψ}› (is ‹_ ≥ …›)
by (metis bot.extremum ccspan_leqI insert_absorb insert_mono)
also have ‹… = ccspan {one_dim_iso ψ *⇩C 1}›
by auto
also have ‹… = ccspan {1}›
apply (rule ccspan_singleton_scaleC)
using ‹ψ ≠ 0› one_dim_iso_of_zero' by auto
also have ‹… = top›
by auto
finally show ‹A = top›
by (simp add: top.extremum_uniqueI)
qed

lemma scaleC_1_right[simp]: ‹scaleC x (1::'a::one_dim) = of_complex x›
unfolding of_complex_def by simp

end
```