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)

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 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