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 classcomplex_algebra_1s 
     via the canonical isomorphism between a one-dimensional vector space and 
     typcomplex.›
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 classfield, 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 classbasis_enum),
  then termone_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)

lemma one_dim_iso_adjoint[simp]: cadjoint one_dim_iso = one_dim_iso
  apply (rule cadjoint_eqI)
  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)

lemma one_dim_iso_add[simp]:
  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