Theory Complex_Vector_Spaces0

(*  Based on HOL/Real_Vector_Spaces.thy by Brian Huffman, Johannes Hölzl
    Adapted to the complex case by Dominique Unruh *)

section ‹‹Complex_Vector_Spaces0› -- Vector Spaces and Algebras over the Complex Numbers›

theory Complex_Vector_Spaces0
  imports HOL.Real_Vector_Spaces HOL.Topological_Spaces HOL.Vector_Spaces
    Complex_Main 
    "HOL-Library.Complex_Order"
    "HOL-Analysis.Product_Vector"
begin                              

subsection ‹Complex vector spaces›

class scaleC = scaleR +
  fixes scaleC :: "complex ⇒ 'a ⇒ 'a" (infixr "*C" 75)
  assumes scaleR_scaleC: "scaleR r = scaleC (complex_of_real r)"
begin

abbreviation divideC :: "'a ⇒ complex ⇒ 'a"  (infixl "'/C" 70)
  where "x /C c ≡ inverse c *C x"

end

class complex_vector = scaleC + ab_group_add +
  assumes scaleC_add_right: "a *C (x + y) = (a *C x) + (a *C y)"
    and scaleC_add_left: "(a + b) *C x = (a *C x) + (b *C x)"
    and scaleC_scaleC[simp]: "a *C (b *C x) =  (a * b) *C x"
    and scaleC_one[simp]: "1 *C x = x"

(* Not present in Real_Vector_Spaces *)
subclass (in complex_vector) real_vector
  by (standard, simp_all add: scaleR_scaleC scaleC_add_right scaleC_add_left)

class complex_algebra = complex_vector + ring +
  assumes mult_scaleC_left [simp]: "a *C x * y = a *C (x * y)"
    and mult_scaleC_right [simp]: "x * a *C y = a *C (x * y)"

(* Not present in Real_Vector_Spaces *)
subclass (in complex_algebra) real_algebra
  by (standard, simp_all add: scaleR_scaleC)

class complex_algebra_1 = complex_algebra + ring_1

(* Not present in Real_Vector_Spaces *)
subclass (in complex_algebra_1) real_algebra_1 ..

class complex_div_algebra = complex_algebra_1 + division_ring

(* Not present in Real_Vector_Spaces *)
subclass (in complex_div_algebra) real_div_algebra ..

class complex_field = complex_div_algebra + field

(* Not present in Real_Vector_Spaces *)
subclass (in complex_field) real_field ..

instantiation complex :: complex_field
begin

definition complex_scaleC_def [simp]: "scaleC a x = a * x"

instance
proof intro_classes
  fix r :: real and a b x y :: complex
  show "((*R) r::complex ⇒ _) = (*C) (complex_of_real r)"
    by (auto simp add: scaleR_conv_of_real)
  show "a *C (x + y) = a *C x + a *C y"
    by (simp add: ring_class.ring_distribs(1))
  show "(a + b) *C x = a *C x + b *C x"
    by (simp add: algebra_simps)
  show "a *C b *C x = (a * b) *C x"
    by simp
  show "1 *C x = x"
    by simp
  show "a *C (x::complex) * y = a *C (x * y)"
    by simp
  show "(x::complex) * a *C y = a *C (x * y)"
    by simp
qed

end

locale clinear = Vector_Spaces.linear "scaleC::_⇒_⇒'a::complex_vector" "scaleC::_⇒_⇒'b::complex_vector"
begin

(* Not present in Real_Vector_Spaces. *)
sublocale real: linear
  ― ‹Gives access to all lemmas from locale‹linear› using prefix ‹real.››
  apply standard
  by (auto simp add: add scale scaleR_scaleC)

lemmas scaleC = scale

end

global_interpretation complex_vector: vector_space "scaleC :: complex ⇒ 'a ⇒ 'a :: complex_vector"
  rewrites "Vector_Spaces.linear (*C) (*C) = clinear"
    and "Vector_Spaces.linear (*) (*C) = clinear"
  defines cdependent_raw_def: cdependent = complex_vector.dependent
    and crepresentation_raw_def: crepresentation = complex_vector.representation
    and csubspace_raw_def: csubspace = complex_vector.subspace
    and cspan_raw_def: cspan = complex_vector.span
    and cextend_basis_raw_def: cextend_basis = complex_vector.extend_basis
    and cdim_raw_def: cdim = complex_vector.dim
proof unfold_locales
  show "Vector_Spaces.linear (*C) (*C) = clinear" "Vector_Spaces.linear (*) (*C) = clinear"
    by (force simp: clinear_def complex_scaleC_def[abs_def])+
qed (use scaleC_add_right scaleC_add_left in auto)


(* Not needed since we did the global_interpretation with mandatory complex_vector-prefix:
hide_const (open)― ‹locale constants›
  complex_vector.dependent
  complex_vector.independent
  complex_vector.representation
  complex_vector.subspace
  complex_vector.span
  complex_vector.extend_basis
  complex_vector.dim *)

abbreviation "cindependent x ≡ ¬ cdependent x"

global_interpretation complex_vector: vector_space_pair "scaleC::_⇒_⇒'a::complex_vector" "scaleC::_⇒_⇒'b::complex_vector"
  rewrites  "Vector_Spaces.linear (*C) (*C) = clinear"
    and "Vector_Spaces.linear (*) (*C) = clinear"
  defines cconstruct_raw_def: cconstruct = complex_vector.construct
proof unfold_locales
  show "Vector_Spaces.linear (*) (*C) = clinear"
    unfolding clinear_def complex_scaleC_def by auto
qed (auto simp: clinear_def)

(* Not needed since we did the global_interpretation with mandatory complex_vector-prefix:
hide_const (open)― ‹locale constants›
  complex_vector.construct *)

lemma clinear_compose: "clinear f ⟹ clinear g ⟹ clinear (g ∘ f)"
  unfolding clinear_def by (rule Vector_Spaces.linear_compose)

text ‹Recover original theorem names›

lemmas scaleC_left_commute = complex_vector.scale_left_commute
lemmas scaleC_zero_left = complex_vector.scale_zero_left
lemmas scaleC_minus_left = complex_vector.scale_minus_left
lemmas scaleC_diff_left = complex_vector.scale_left_diff_distrib
lemmas scaleC_sum_left = complex_vector.scale_sum_left
lemmas scaleC_zero_right = complex_vector.scale_zero_right
lemmas scaleC_minus_right = complex_vector.scale_minus_right
lemmas scaleC_diff_right = complex_vector.scale_right_diff_distrib
lemmas scaleC_sum_right = complex_vector.scale_sum_right
lemmas scaleC_eq_0_iff = complex_vector.scale_eq_0_iff
lemmas scaleC_left_imp_eq = complex_vector.scale_left_imp_eq
lemmas scaleC_right_imp_eq = complex_vector.scale_right_imp_eq
lemmas scaleC_cancel_left = complex_vector.scale_cancel_left
lemmas scaleC_cancel_right = complex_vector.scale_cancel_right

lemma divideC_field_simps[field_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "c ≠ 0 ⟹ a = b /C c ⟷ c *C a = b"
  "c ≠ 0 ⟹ b /C c = a ⟷ b = c *C a"
  "c ≠ 0 ⟹ a + b /C c = (c *C a + b) /C c"
  "c ≠ 0 ⟹ a /C c + b = (a + c *C b) /C c"
  "c ≠ 0 ⟹ a - b /C c = (c *C a - b) /C c"
  "c ≠ 0 ⟹ a /C c - b = (a - c *C b) /C c"
  "c ≠ 0 ⟹ - (a /C c) + b = (- a + c *C b) /C c"
  "c ≠ 0 ⟹ - (a /C c) - b = (- a - c *C b) /C c"
  for a b :: "'a :: complex_vector"
  by (auto simp add: scaleC_add_right scaleC_add_left scaleC_diff_right scaleC_diff_left)


text ‹Legacy names -- omitted›

(* lemmas scaleC_left_distrib = scaleC_add_left
lemmas scaleC_right_distrib = scaleC_add_right
lemmas scaleC_left_diff_distrib = scaleC_diff_left
lemmas scaleC_right_diff_distrib = scaleC_diff_right *)

lemmas clinear_injective_0 = linear_inj_iff_eq_0
  and clinear_injective_on_subspace_0 = linear_inj_on_iff_eq_0
  and clinear_cmul = linear_scale
  and clinear_scaleC = linear_scale_self
  and csubspace_mul = subspace_scale
  and cspan_linear_image = linear_span_image
  and cspan_0 = span_zero
  and cspan_mul = span_scale
  and injective_scaleC = injective_scale

lemma scaleC_minus1_left [simp]: "scaleC (-1) x = - x"
  for x :: "'a::complex_vector"
  using scaleC_minus_left [of 1 x] by simp

lemma scaleC_2:
  fixes x :: "'a::complex_vector"
  shows "scaleC 2 x = x + x"
  unfolding one_add_one [symmetric] scaleC_add_left by simp

lemma scaleC_half_double [simp]:
  fixes a :: "'a::complex_vector"
  shows "(1 / 2) *C (a + a) = a"
proof -
  have "⋀r. r *C (a + a) = (r * 2) *C a"
    by (metis scaleC_2 scaleC_scaleC)
  thus ?thesis
    by simp
qed

lemma clinear_scale_complex:
  fixes c::complex shows "clinear f ⟹ f (c * b) = c * f b"
  using complex_vector.linear_scale by fastforce


interpretation scaleC_left: additive "(λa. scaleC a x :: 'a::complex_vector)"
  by standard (rule scaleC_add_left)

interpretation scaleC_right: additive "(λx. scaleC a x :: 'a::complex_vector)"
  by standard (rule scaleC_add_right)

lemma nonzero_inverse_scaleC_distrib:
  "a ≠ 0 ⟹ x ≠ 0 ⟹ inverse (scaleC a x) = scaleC (inverse a) (inverse x)"
  for x :: "'a::complex_div_algebra"
  by (rule inverse_unique) simp

lemma inverse_scaleC_distrib: "inverse (scaleC a x) = scaleC (inverse a) (inverse x)"
  for x :: "'a::{complex_div_algebra,division_ring}"
  by (metis inverse_zero nonzero_inverse_scaleC_distrib complex_vector.scale_eq_0_iff)

(* lemmas sum_constant_scaleC = real_vector.sum_constant_scale― ‹legacy name› *)

(* Defined in Real_Vector_Spaces:
named_theorems vector_add_divide_simps "to simplify sums of scaled vectors" *)

lemma complex_add_divide_simps[vector_add_divide_simps]:  (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "v + (b / z) *C w = (if z = 0 then v else (z *C v + b *C w) /C z)"
  "a *C v + (b / z) *C w = (if z = 0 then a *C v else ((a * z) *C v + b *C w) /C z)"
  "(a / z) *C v + w = (if z = 0 then w else (a *C v + z *C w) /C z)"
  "(a / z) *C v + b *C w = (if z = 0 then b *C w else (a *C v + (b * z) *C w) /C z)"
  "v - (b / z) *C w = (if z = 0 then v else (z *C v - b *C w) /C z)"
  "a *C v - (b / z) *C w = (if z = 0 then a *C v else ((a * z) *C v - b *C w) /C z)"
  "(a / z) *C v - w = (if z = 0 then -w else (a *C v - z *C w) /C z)"
  "(a / z) *C v - b *C w = (if z = 0 then -b *C w else (a *C v - (b * z) *C w) /C z)"
  for v :: "'a :: complex_vector"
  by (simp_all add: divide_inverse_commute scaleC_add_right scaleC_diff_right)

lemma ceq_vector_fraction_iff [vector_add_divide_simps]:
  fixes x :: "'a :: complex_vector"
  shows "(x = (u / v) *C a) ⟷ (if v=0 then x = 0 else v *C x = u *C a)"
  by auto (metis (no_types) divide_eq_1_iff divide_inverse_commute scaleC_one scaleC_scaleC)

lemma cvector_fraction_eq_iff [vector_add_divide_simps]:
  fixes x :: "'a :: complex_vector"
  shows "((u / v) *C a = x) ⟷ (if v=0 then x = 0 else u *C a = v *C x)"
  by (metis ceq_vector_fraction_iff)

lemma complex_vector_affinity_eq:
  fixes x :: "'a :: complex_vector"
  assumes m0: "m ≠ 0"
  shows "m *C x + c = y ⟷ x = inverse m *C y - (inverse m *C c)"
    (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  hence "m *C x = y - c" by (simp add: field_simps)
  hence "inverse m *C (m *C x) = inverse m *C (y - c)" by simp
  thus "x = inverse m *C y - (inverse m *C c)"
    using m0
    by (simp add: complex_vector.scale_right_diff_distrib)
next
  assume ?rhs
  with m0 show "m *C x + c = y"
    by (simp add: complex_vector.scale_right_diff_distrib)
qed

lemma complex_vector_eq_affinity: "m ≠ 0 ⟹ y = m *C x + c ⟷ inverse m *C y - (inverse m *C c) = x"
  for x :: "'a::complex_vector"
  using complex_vector_affinity_eq[where m=m and x=x and y=y and c=c]
  by metis

lemma scaleC_eq_iff [simp]: "b + u *C a = a + u *C b ⟷ a = b ∨ u = 1"
  for a :: "'a::complex_vector"
proof (cases "u = 1")
  case True
  thus ?thesis by auto
next
  case False
  have "a = b" if "b + u *C a = a + u *C b"
  proof -
    from that have "(u - 1) *C a = (u - 1) *C b"
      by (simp add: algebra_simps)
    with False show ?thesis
      by auto
  qed
  thus ?thesis by auto
qed

lemma scaleC_collapse [simp]: "(1 - u) *C a + u *C a = a"
  for a :: "'a::complex_vector"
  by (simp add: algebra_simps)

subsection ‹Embedding of the Complex Numbers into any ‹complex_algebra_1›: ‹of_complex››


definition of_complex :: "complex ⇒ 'a::complex_algebra_1"
  where "of_complex c = scaleC c 1"


lemma scaleC_conv_of_complex: "scaleC r x = of_complex r * x"
  by (simp add: of_complex_def)

lemma of_complex_0 [simp]: "of_complex 0 = 0"
  by (simp add: of_complex_def)

lemma of_complex_1 [simp]: "of_complex 1 = 1"
  by (simp add: of_complex_def)

lemma of_complex_add [simp]: "of_complex (x + y) = of_complex x + of_complex y"
  by (simp add: of_complex_def scaleC_add_left)

lemma of_complex_minus [simp]: "of_complex (- x) = - of_complex x"
  by (simp add: of_complex_def)

lemma of_complex_diff [simp]: "of_complex (x - y) = of_complex x - of_complex y"
  by (simp add: of_complex_def scaleC_diff_left)

lemma of_complex_mult [simp]: "of_complex (x * y) = of_complex x * of_complex y"
  by (simp add: of_complex_def mult.commute)

lemma of_complex_sum[simp]: "of_complex (sum f s) = (∑x∈s. of_complex (f x))"
  by (induct s rule: infinite_finite_induct) auto

lemma of_complex_prod[simp]: "of_complex (prod f s) = (∏x∈s. of_complex (f x))"
  by (induct s rule: infinite_finite_induct) auto

lemma nonzero_of_complex_inverse:
  "x ≠ 0 ⟹ of_complex (inverse x) = inverse (of_complex x :: 'a::complex_div_algebra)"
  by (simp add: of_complex_def nonzero_inverse_scaleC_distrib)

lemma of_complex_inverse [simp]:
  "of_complex (inverse x) = inverse (of_complex x :: 'a::{complex_div_algebra,division_ring})"
  by (simp add: of_complex_def inverse_scaleC_distrib)

lemma nonzero_of_complex_divide:
  "y ≠ 0 ⟹ of_complex (x / y) = (of_complex x / of_complex y :: 'a::complex_field)"
  by (simp add: divide_inverse nonzero_of_complex_inverse)

lemma of_complex_divide [simp]:
  "of_complex (x / y) = (of_complex x / of_complex y :: 'a::complex_div_algebra)"
  by (simp add: divide_inverse)

lemma of_complex_power [simp]:
  "of_complex (x ^ n) = (of_complex x :: 'a::{complex_algebra_1}) ^ n"
  by (induct n) simp_all

lemma of_complex_power_int [simp]:
  "of_complex (power_int x n) = power_int (of_complex x :: 'a :: {complex_div_algebra,division_ring}) n"
  by (auto simp: power_int_def)

lemma of_complex_eq_iff [simp]: "of_complex x = of_complex y ⟷ x = y"
  by (simp add: of_complex_def)

lemma inj_of_complex: "inj of_complex"
  by (auto intro: injI)

lemmas of_complex_eq_0_iff [simp] = of_complex_eq_iff [of _ 0, simplified]
lemmas of_complex_eq_1_iff [simp] = of_complex_eq_iff [of _ 1, simplified]

lemma minus_of_complex_eq_of_complex_iff [simp]: "-of_complex x = of_complex y ⟷ -x = y"
  using of_complex_eq_iff[of "-x" y] by (simp only: of_complex_minus)

lemma of_complex_eq_minus_of_complex_iff [simp]: "of_complex x = -of_complex y ⟷ x = -y"
  using of_complex_eq_iff[of x "-y"] by (simp only: of_complex_minus)

lemma of_complex_eq_id [simp]: "of_complex = (id :: complex ⇒ complex)"
  by (rule ext) (simp add: of_complex_def)

text ‹Collapse nested embeddings.›
lemma of_complex_of_nat_eq [simp]: "of_complex (of_nat n) = of_nat n"
  by (induct n) auto

lemma of_complex_of_int_eq [simp]: "of_complex (of_int z) = of_int z"
  by (cases z rule: int_diff_cases) simp

lemma of_complex_numeral [simp]: "of_complex (numeral w) = numeral w"
  using of_complex_of_int_eq [of "numeral w"] by simp

lemma of_complex_neg_numeral [simp]: "of_complex (- numeral w) = - numeral w"
  using of_complex_of_int_eq [of "- numeral w"] by simp

lemma numeral_power_int_eq_of_complex_cancel_iff [simp]:
  "power_int (numeral x) n = (of_complex y :: 'a :: {complex_div_algebra, division_ring}) ⟷
     power_int (numeral x) n = y"
proof -
  have "power_int (numeral x) n = (of_complex (power_int (numeral x) n) :: 'a)"
    by simp
  also have "… = of_complex y ⟷ power_int (numeral x) n = y"
    by (subst of_complex_eq_iff) auto
  finally show ?thesis .
qed

lemma of_complex_eq_numeral_power_int_cancel_iff [simp]:
  "(of_complex y :: 'a :: {complex_div_algebra, division_ring}) = power_int (numeral x) n ⟷
     y = power_int (numeral x) n"
  by (subst (1 2) eq_commute) simp

lemma of_complex_eq_of_complex_power_int_cancel_iff [simp]:
  "power_int (of_complex b :: 'a :: {complex_div_algebra, division_ring}) w = of_complex x ⟷
     power_int b w = x"
  by (metis of_complex_power_int of_complex_eq_iff)

lemma of_complex_in_Ints_iff [simp]: "of_complex x ∈ ℤ ⟷ x ∈ ℤ"
proof safe
  fix x assume "(of_complex x :: 'a) ∈ ℤ"
  then obtain n where "(of_complex x :: 'a) = of_int n"
    by (auto simp: Ints_def)
  also have "of_int n = of_complex (of_int n)"
    by simp
  finally have "x = of_int n"
    by (subst (asm) of_complex_eq_iff)
  thus "x ∈ ℤ"
    by auto
qed (auto simp: Ints_def)

lemma Ints_of_complex [intro]: "x ∈ ℤ ⟹ of_complex x ∈ ℤ"
  by simp


text ‹Every complex algebra has characteristic zero.›

(* Inherited from real_algebra_1 *)
(* instance complex_algebra_1 < ring_char_0 .. *)

lemma fraction_scaleC_times [simp]:
  fixes a :: "'a::complex_algebra_1"
  shows "(numeral u / numeral v) *C (numeral w * a) = (numeral u * numeral w / numeral v) *C a"
  by (metis (no_types, lifting) of_complex_numeral scaleC_conv_of_complex scaleC_scaleC times_divide_eq_left)

lemma inverse_scaleC_times [simp]:
  fixes a :: "'a::complex_algebra_1"
  shows "(1 / numeral v) *C (numeral w * a) = (numeral w / numeral v) *C a"
  by (metis divide_inverse_commute inverse_eq_divide of_complex_numeral scaleC_conv_of_complex scaleC_scaleC)

lemma scaleC_times [simp]:
  fixes a :: "'a::complex_algebra_1"
  shows "(numeral u) *C (numeral w * a) = (numeral u * numeral w) *C a"
  by (simp add: scaleC_conv_of_complex)

(* Inherited from real_field *)
(* instance complex_field < field_char_0 .. *)


subsection ‹The Set of Real Numbers›

definition Complexs :: "'a::complex_algebra_1 set"  ("ℂ")
  where "ℂ = range of_complex"

lemma Complexs_of_complex [simp]: "of_complex r ∈ ℂ"
  by (simp add: Complexs_def)

lemma Complexs_of_int [simp]: "of_int z ∈ ℂ"
  by (subst of_complex_of_int_eq [symmetric], rule Complexs_of_complex)

lemma Complexs_of_nat [simp]: "of_nat n ∈ ℂ"
  by (subst of_complex_of_nat_eq [symmetric], rule Complexs_of_complex)

lemma Complexs_numeral [simp]: "numeral w ∈ ℂ"
  by (subst of_complex_numeral [symmetric], rule Complexs_of_complex)

lemma Complexs_0 [simp]: "0 ∈ ℂ" and Complexs_1 [simp]: "1 ∈ ℂ"
  by (simp_all add: Complexs_def)

lemma Complexs_add [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a + b ∈ ℂ"
  apply (auto simp add: Complexs_def)
  by (metis of_complex_add range_eqI)

lemma Complexs_minus [simp]: "a ∈ ℂ ⟹ - a ∈ ℂ"
  by (auto simp: Complexs_def)

lemma Complexs_minus_iff [simp]: "- a ∈ ℂ ⟷ a ∈ ℂ"
  using Complexs_minus by fastforce

lemma Complexs_diff [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a - b ∈ ℂ"
  by (metis Complexs_add Complexs_minus_iff add_uminus_conv_diff)

lemma Complexs_mult [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a * b ∈ ℂ"
  apply (auto simp add: Complexs_def)
  by (metis of_complex_mult rangeI)

lemma nonzero_Complexs_inverse: "a ∈ ℂ ⟹ a ≠ 0 ⟹ inverse a ∈ ℂ"
  for a :: "'a::complex_div_algebra"
  apply (auto simp add: Complexs_def)
  by (metis of_complex_inverse range_eqI)

lemma Complexs_inverse: "a ∈ ℂ ⟹ inverse a ∈ ℂ"
  for a :: "'a::{complex_div_algebra,division_ring}"
  using nonzero_Complexs_inverse by fastforce

lemma Complexs_inverse_iff [simp]: "inverse x ∈ ℂ ⟷ x ∈ ℂ"
  for x :: "'a::{complex_div_algebra,division_ring}"
  by (metis Complexs_inverse inverse_inverse_eq)

lemma nonzero_Complexs_divide: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ b ≠ 0 ⟹ a / b ∈ ℂ"
  for a b :: "'a::complex_field"
  by (simp add: divide_inverse)

lemma Complexs_divide [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a / b ∈ ℂ"
  for a b :: "'a::{complex_field,field}"
  using nonzero_Complexs_divide by fastforce

lemma Complexs_power [simp]: "a ∈ ℂ ⟹ a ^ n ∈ ℂ"
  for a :: "'a::complex_algebra_1"
  apply (auto simp add: Complexs_def)
  by (metis range_eqI of_complex_power[symmetric])

lemma Complexs_cases [cases set: Complexs]:
  assumes "q ∈ ℂ"
  obtains (of_complex) c where "q = of_complex c"
  unfolding Complexs_def
proof -
  from ‹q ∈ ℂ› have "q ∈ range of_complex" unfolding Complexs_def .
  then obtain c where "q = of_complex c" ..
  then show thesis ..
qed

lemma sum_in_Complexs [intro,simp]: "(⋀i. i ∈ s ⟹ f i ∈ ℂ) ⟹ sum f s ∈ ℂ"
proof (induct s rule: infinite_finite_induct)
  case infinite
  then show ?case by (metis Complexs_0 sum.infinite)
qed simp_all

lemma prod_in_Complexs [intro,simp]: "(⋀i. i ∈ s ⟹ f i ∈ ℂ) ⟹ prod f s ∈ ℂ"
proof (induct s rule: infinite_finite_induct)
  case infinite
  then show ?case by (metis Complexs_1 prod.infinite)
qed simp_all

lemma Complexs_induct [case_names of_complex, induct set: Complexs]:
  "q ∈ ℂ ⟹ (⋀r. P (of_complex r)) ⟹ P q"
  by (rule Complexs_cases) auto



subsection ‹Ordered complex vector spaces›

class ordered_complex_vector = complex_vector + ordered_ab_group_add +
  assumes scaleC_left_mono: "x ≤ y ⟹ 0 ≤ a ⟹ a *C x ≤ a *C y"
    and scaleC_right_mono: "a ≤ b ⟹ 0 ≤ x ⟹ a *C x ≤ b *C x"
begin

subclass (in ordered_complex_vector) ordered_real_vector
  apply standard
  by (auto simp add: less_eq_complex_def scaleC_left_mono scaleC_right_mono scaleR_scaleC)

lemma scaleC_mono:
  "a ≤ b ⟹ x ≤ y ⟹ 0 ≤ b ⟹ 0 ≤ x ⟹ a *C x ≤ b *C y"
  by (meson order_trans scaleC_left_mono scaleC_right_mono)

lemma scaleC_mono':
  "a ≤ b ⟹ c ≤ d ⟹ 0 ≤ a ⟹ 0 ≤ c ⟹ a *C c ≤ b *C d"
  by (rule scaleC_mono) (auto intro: order.trans)

lemma pos_le_divideC_eq [field_simps]:
  "a ≤ b /C c ⟷ c *C a ≤ b" (is "?P ⟷ ?Q") if "0 < c"
proof
  assume ?P
  with scaleC_left_mono that have "c *C a ≤ c *C (b /C c)"
    using preorder_class.less_imp_le by blast
  with that show ?Q
    by auto
next
  assume ?Q
  with scaleC_left_mono that have "c *C a /C c ≤ b /C c"
    using less_complex_def less_eq_complex_def by fastforce
  with that show ?P
    by auto
qed

lemma pos_less_divideC_eq [field_simps]:
  "a < b /C c ⟷ c *C a < b" if "c > 0"
  using that pos_le_divideC_eq [of c a b]
  by (auto simp add: le_less)

lemma pos_divideC_le_eq [field_simps]:
  "b /C c ≤ a ⟷ b ≤ c *C a" if "c > 0"
  using that pos_le_divideC_eq [of "inverse c" b a]
    less_complex_def by auto

lemma pos_divideC_less_eq [field_simps]:
  "b /C c < a ⟷ b < c *C a" if "c > 0"
  using that pos_less_divideC_eq [of "inverse c" b a]
  by (simp add: local.less_le_not_le local.pos_divideC_le_eq local.pos_le_divideC_eq)

lemma pos_le_minus_divideC_eq [field_simps]:
  "a ≤ - (b /C c) ⟷ c *C a ≤ - b" if "c > 0"
  using that
  by (metis local.ab_left_minus local.add.inverse_unique local.add.right_inverse local.add_minus_cancel local.le_minus_iff local.pos_divideC_le_eq local.scaleC_add_right local.scaleC_one local.scaleC_scaleC)

lemma pos_less_minus_divideC_eq [field_simps]:
  "a < - (b /C c) ⟷ c *C a < - b" if "c > 0"
  using that
  by (metis le_less less_le_not_le pos_divideC_le_eq pos_divideC_less_eq pos_le_minus_divideC_eq)

lemma pos_minus_divideC_le_eq [field_simps]:
  "- (b /C c) ≤ a ⟷ - b ≤ c *C a" if "c > 0"
  using that
  by (metis local.add_minus_cancel local.left_minus local.pos_divideC_le_eq local.scaleC_add_right)

lemma pos_minus_divideC_less_eq [field_simps]:
  "- (b /C c) < a ⟷ - b < c *C a" if "c > 0"
  using that by (simp add: less_le_not_le pos_le_minus_divideC_eq pos_minus_divideC_le_eq)

lemma scaleC_image_atLeastAtMost: "c > 0 ⟹ scaleC c ` {x..y} = {c *C x..c *C y}"
  apply (auto intro!: scaleC_left_mono simp: image_iff Bex_def)
  by (meson order.eq_iff local.order.refl pos_divideC_le_eq pos_le_divideC_eq)

end (* class ordered_complex_vector *)

lemma neg_le_divideC_eq [field_simps]:
  "a ≤ b /C c ⟷ b ≤ c *C a" (is "?P ⟷ ?Q") if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
  using that pos_le_divideC_eq [of "- c" a "- b"]
  by (simp add: less_complex_def)

lemma neg_less_divideC_eq [field_simps]:
  "a < b /C c ⟷ b < c *C a" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
  using that neg_le_divideC_eq [of c a b]
  by (smt (verit, ccfv_SIG) neg_le_divideC_eq antisym_conv2 complex_vector.scale_minus_right dual_order.strict_implies_order le_less_trans neg_le_iff_le scaleC_scaleC)

lemma neg_divideC_le_eq [field_simps]:
  "b /C c ≤ a ⟷ c *C a ≤ b" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
  using that pos_divideC_le_eq [of "- c" "- b" a]
  by (simp add: less_complex_def)

lemma neg_divideC_less_eq [field_simps]:
  "b /C c < a ⟷ c *C a < b" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
  using that neg_divideC_le_eq [of c b a]
  by (meson neg_le_divideC_eq less_le_not_le)

lemma neg_le_minus_divideC_eq [field_simps]:
  "a ≤ - (b /C c) ⟷ - b ≤ c *C a" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
  using that pos_le_minus_divideC_eq [of "- c" a "- b"]
  by (metis neg_le_divideC_eq complex_vector.scale_minus_right)

lemma neg_less_minus_divideC_eq [field_simps]:
  "a < - (b /C c) ⟷ - b < c *C a" if "c < 0"
    for a b :: "'a :: ordered_complex_vector"
proof -
  have *: "- b = c *C a ⟷ b = - (c *C a)"
    by (metis add.inverse_inverse)
  from that neg_le_minus_divideC_eq [of c a b]
  show ?thesis by (auto simp add: le_less *)
qed

lemma neg_minus_divideC_le_eq [field_simps]:
  "- (b /C c) ≤ a ⟷ c *C a ≤ - b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
  using that pos_minus_divideC_le_eq [of "- c" "- b" a]
  by (metis Complex_Vector_Spaces0.neg_divideC_le_eq complex_vector.scale_minus_right)

lemma neg_minus_divideC_less_eq [field_simps]:
  "- (b /C c) < a ⟷ c *C a < - b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
  using that by (simp add: less_le_not_le neg_le_minus_divideC_eq neg_minus_divideC_le_eq)

lemma divideC_field_splits_simps_1 [field_split_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "a = b /C c ⟷ (if c = 0 then a = 0 else c *C a = b)"
  "b /C c = a ⟷ (if c = 0 then a = 0 else b = c *C a)"
  "a + b /C c = (if c = 0 then a else (c *C a + b) /C c)"
  "a /C c + b = (if c = 0 then b else (a + c *C b) /C c)"
  "a - b /C c = (if c = 0 then a else (c *C a - b) /C c)"
  "a /C c - b = (if c = 0 then - b else (a - c *C b) /C c)"
  "- (a /C c) + b = (if c = 0 then b else (- a + c *C b) /C c)"
  "- (a /C c) - b = (if c = 0 then - b else (- a - c *C b) /C c)"
  for a b :: "'a :: complex_vector"
  by (auto simp add: field_simps)

lemma divideC_field_splits_simps_2 [field_split_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
  "0 < c ⟹ a ≤ b /C c ⟷ (if c > 0 then c *C a ≤ b else if c < 0 then b ≤ c *C a else a ≤ 0)"
  "0 < c ⟹ a < b /C c ⟷ (if c > 0 then c *C a < b else if c < 0 then b < c *C a else a < 0)"
  "0 < c ⟹ b /C c ≤ a ⟷ (if c > 0 then b ≤ c *C a else if c < 0 then c *C a ≤ b else a ≥ 0)"
  "0 < c ⟹ b /C c < a ⟷ (if c > 0 then b < c *C a else if c < 0 then c *C a < b else a > 0)"
  "0 < c ⟹ a ≤ - (b /C c) ⟷ (if c > 0 then c *C a ≤ - b else if c < 0 then - b ≤ c *C a else a ≤ 0)"
  "0 < c ⟹ a < - (b /C c) ⟷ (if c > 0 then c *C a < - b else if c < 0 then - b < c *C a else a < 0)"
  "0 < c ⟹ - (b /C c) ≤ a ⟷ (if c > 0 then - b ≤ c *C a else if c < 0 then c *C a ≤ - b else a ≥ 0)"
  "0 < c ⟹ - (b /C c) < a ⟷ (if c > 0 then - b < c *C a else if c < 0 then c *C a < - b else a > 0)"
  for a b :: "'a :: ordered_complex_vector"
  by (clarsimp intro!: field_simps)+

lemma scaleC_nonneg_nonneg: "0 ≤ a ⟹ 0 ≤ x ⟹ 0 ≤ a *C x"
  for x :: "'a::ordered_complex_vector"
  using scaleC_left_mono [of 0 x a] by simp

lemma scaleC_nonneg_nonpos: "0 ≤ a ⟹ x ≤ 0 ⟹ a *C x ≤ 0"
  for x :: "'a::ordered_complex_vector"
  using scaleC_left_mono [of x 0 a] by simp

lemma scaleC_nonpos_nonneg: "a ≤ 0 ⟹ 0 ≤ x ⟹ a *C x ≤ 0"
  for x :: "'a::ordered_complex_vector"
  using scaleC_right_mono [of a 0 x] by simp

lemma split_scaleC_neg_le: "(0 ≤ a ∧ x ≤ 0) ∨ (a ≤ 0 ∧ 0 ≤ x) ⟹ a *C x ≤ 0"
  for x :: "'a::ordered_complex_vector"
  by (auto simp: scaleC_nonneg_nonpos scaleC_nonpos_nonneg)

lemma cle_add_iff1: "a *C e + c ≤ b *C e + d ⟷ (a - b) *C e + c ≤ d"
  for c d e :: "'a::ordered_complex_vector"
  by (simp add: algebra_simps)

lemma cle_add_iff2: "a *C e + c ≤ b *C e + d ⟷ c ≤ (b - a) *C e + d"
  for c d e :: "'a::ordered_complex_vector"
  by (simp add: algebra_simps)

lemma scaleC_left_mono_neg: "b ≤ a ⟹ c ≤ 0 ⟹ c *C a ≤ c *C b"
  for a b :: "'a::ordered_complex_vector"
  by (drule scaleC_left_mono [of _ _ "- c"], simp_all add: less_eq_complex_def)

lemma scaleC_right_mono_neg: "b ≤ a ⟹ c ≤ 0 ⟹ a *C c ≤ b *C c"
  for c :: "'a::ordered_complex_vector"
  by (drule scaleC_right_mono [of _ _ "- c"], simp_all)

lemma scaleC_nonpos_nonpos: "a ≤ 0 ⟹ b ≤ 0 ⟹ 0 ≤ a *C b"
  for b :: "'a::ordered_complex_vector"
  using scaleC_right_mono_neg [of a 0 b] by simp

lemma split_scaleC_pos_le: "(0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0) ⟹ 0 ≤ a *C b"
  for b :: "'a::ordered_complex_vector"
  by (auto simp: scaleC_nonneg_nonneg scaleC_nonpos_nonpos)

lemma zero_le_scaleC_iff:
  fixes b :: "'a::ordered_complex_vector"
  assumes "a ∈ ℝ" (* Not present in Real_Vector_Spaces.thy *)
  shows "0 ≤ a *C b ⟷ 0 < a ∧ 0 ≤ b ∨ a < 0 ∧ b ≤ 0 ∨ a = 0"
    (is "?lhs = ?rhs")
proof (cases "a = 0")
  case True
  then show ?thesis by simp
next
  case False
  show ?thesis
  proof
    assume ?lhs
    from ‹a ≠ 0› consider "a > 0" | "a < 0"
      by (metis assms complex_is_Real_iff less_complex_def less_eq_complex_def not_le order.not_eq_order_implies_strict that(1) zero_complex.sel(2))
    then show ?rhs
    proof cases
      case 1
      with ‹?lhs› have "inverse a *C 0 ≤ inverse a *C (a *C b)"
        by (metis complex_vector.scale_zero_right ordered_complex_vector_class.pos_le_divideC_eq)
      with 1 show ?thesis
        by simp
    next
      case 2
      with ‹?lhs› have "- inverse a *C 0 ≤ - inverse a *C (a *C b)"
        by (metis Complex_Vector_Spaces0.neg_le_minus_divideC_eq complex_vector.scale_zero_right neg_le_0_iff_le scaleC_left.minus)
      with 2 show ?thesis
        by simp
    qed
  next
    assume ?rhs
    then show ?lhs
      using less_imp_le split_scaleC_pos_le by auto
  qed
qed

lemma scaleC_le_0_iff:
  "a *C b ≤ 0 ⟷ 0 < a ∧ b ≤ 0 ∨ a < 0 ∧ 0 ≤ b ∨ a = 0"
  if "a ∈ ℝ" (* Not present in Real_Vector_Spaces *)
  for b::"'a::ordered_complex_vector"
  apply (insert zero_le_scaleC_iff [of "-a" b])
  using less_complex_def that by force


lemma scaleC_le_cancel_left: "c *C a ≤ c *C b ⟷ (0 < c ⟶ a ≤ b) ∧ (c < 0 ⟶ b ≤ a)"
  if "c ∈ ℝ" (* Not present in Real_Vector_Spaces *)
  for b :: "'a::ordered_complex_vector"
  by (smt (verit, ccfv_threshold) Complex_Vector_Spaces0.neg_divideC_le_eq complex_vector.scale_cancel_left complex_vector.scale_zero_right dual_order.eq_iff dual_order.trans ordered_complex_vector_class.pos_le_divideC_eq that zero_le_scaleC_iff)

lemma scaleC_le_cancel_left_pos: "0 < c ⟹ c *C a ≤ c *C b ⟷ a ≤ b"
  for b :: "'a::ordered_complex_vector"
  by (simp add: complex_is_Real_iff less_complex_def scaleC_le_cancel_left)

lemma scaleC_le_cancel_left_neg: "c < 0 ⟹ c *C a ≤ c *C b ⟷ b ≤ a"
  for b :: "'a::ordered_complex_vector"
  by (simp add: complex_is_Real_iff less_complex_def scaleC_le_cancel_left)

lemma scaleC_left_le_one_le: "0 ≤ x ⟹ a ≤ 1 ⟹ a *C x ≤ x"
  for x :: "'a::ordered_complex_vector" and a :: complex
  using scaleC_right_mono[of a 1 x] by simp

subsection ‹Complex normed vector spaces›

(* Classes dist, norm, sgn_div_norm, dist_norm, uniformity_dist
   defined in Real_Vector_Spaces are unchanged in the complex setting.
   No need to define them here. *)

class complex_normed_vector = complex_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
  real_normed_vector + (* Not present in Real_Normed_Vector *)
  assumes norm_scaleC [simp]: "norm (scaleC a x) = cmod a * norm x"
begin
(* lemma norm_ge_zero [simp]: "0 ≤ norm x" *) (* Not needed, included from real_normed_vector *)
end

class complex_normed_algebra = complex_algebra + complex_normed_vector +
  real_normed_algebra (* Not present in Real_Normed_Vector *)
  (* assumes norm_mult_ineq: "norm (x * y) ≤ norm x * norm y" *) (* Not needed, included from real_normed_algebra *)

class complex_normed_algebra_1 = complex_algebra_1 + complex_normed_algebra +
  real_normed_algebra_1 (* Not present in Real_Normed_Vector *)
  (* assumes norm_one [simp]: "norm 1 = 1" *) (* Not needed, included from real_normed_algebra_1 *)

lemma (in complex_normed_algebra_1) scaleC_power [simp]: "(scaleC x y) ^ n = scaleC (x^n) (y^n)"
  by (induct n) (simp_all add: mult_ac)

class complex_normed_div_algebra = complex_div_algebra + complex_normed_vector +
  real_normed_div_algebra (* Not present in Real_Normed_Vector *)
  (* assumes norm_mult: "norm (x * y) = norm x * norm y" *) (* Not needed, included from real_normed_div_algebra *)

class complex_normed_field = complex_field + complex_normed_div_algebra

subclass (in complex_normed_field) real_normed_field ..

instance complex_normed_div_algebra < complex_normed_algebra_1 ..

context complex_normed_vector begin
(* Inherited from real_normed_vector:
lemma norm_zero [simp]: "norm (0::'a) = 0"
lemma zero_less_norm_iff [simp]: "norm x > 0 ⟷ x ≠ 0"
lemma norm_not_less_zero [simp]: "¬ norm x < 0"
lemma norm_le_zero_iff [simp]: "norm x ≤ 0 ⟷ x = 0"
lemma norm_minus_cancel [simp]: "norm (- x) = norm x"
lemma norm_minus_commute: "norm (a - b) = norm (b - a)"
lemma dist_add_cancel [simp]: "dist (a + b) (a + c) = dist b c"
lemma dist_add_cancel2 [simp]: "dist (b + a) (c + a) = dist b c"
lemma norm_uminus_minus: "norm (- x - y) = norm (x + y)"
lemma norm_triangle_ineq2: "norm a - norm b ≤ norm (a - b)"
lemma norm_triangle_ineq3: "¦norm a - norm b¦ ≤ norm (a - b)"
lemma norm_triangle_ineq4: "norm (a - b) ≤ norm a + norm b"
lemma norm_triangle_le_diff: "norm x + norm y ≤ e ⟹ norm (x - y) ≤ e"
lemma norm_diff_ineq: "norm a - norm b ≤ norm (a + b)"
lemma norm_triangle_sub: "norm x ≤ norm y + norm (x - y)"
lemma norm_triangle_le: "norm x + norm y ≤ e ⟹ norm (x + y) ≤ e"
lemma norm_triangle_lt: "norm x + norm y < e ⟹ norm (x + y) < e"
lemma norm_add_leD: "norm (a + b) ≤ c ⟹ norm b ≤ norm a + c"
lemma norm_diff_triangle_ineq: "norm ((a + b) - (c + d)) ≤ norm (a - c) + norm (b - d)"
lemma norm_diff_triangle_le: "norm (x - z) ≤ e1 + e2"
  if "norm (x - y) ≤ e1"  "norm (y - z) ≤ e2"
lemma norm_diff_triangle_less: "norm (x - z) < e1 + e2"
  if "norm (x - y) < e1"  "norm (y - z) < e2"
lemma norm_triangle_mono:
  "norm a ≤ r ⟹ norm b ≤ s ⟹ norm (a + b) ≤ r + s"
lemma norm_sum: "norm (sum f A) ≤ (∑i∈A. norm (f i))"
  for f::"'b ⇒ 'a"
lemma sum_norm_le: "norm (sum f S) ≤ sum g S"
  if "⋀x. x ∈ S ⟹ norm (f x) ≤ g x"
  for f::"'b ⇒ 'a"
lemma abs_norm_cancel [simp]: "¦norm a¦ = norm a"
lemma sum_norm_bound:
  "norm (sum f S) ≤ of_nat (card S)*K"
  if "⋀x. x ∈ S ⟹ norm (f x) ≤ K"
  for f :: "'b ⇒ 'a"
lemma norm_add_less: "norm x < r ⟹ norm y < s ⟹ norm (x + y) < r + s"
*)
end

lemma dist_scaleC [simp]: "dist (x *C a) (y *C a) = ¦x - y¦ * norm a"
  for a :: "'a::complex_normed_vector"
  by (metis dist_scaleR scaleR_scaleC)

(* Inherited from real_normed_vector *)
(* lemma norm_mult_less: "norm x < r ⟹ norm y < s ⟹ norm (x * y) < r * s"
  for x y :: "'a::complex_normed_algebra" *)

lemma norm_of_complex [simp]: "norm (of_complex c :: 'a::complex_normed_algebra_1) = cmod c"
  by (simp add: of_complex_def)

(* Inherited from real_normed_vector:
lemma norm_numeral [simp]: "norm (numeral w::'a::complex_normed_algebra_1) = numeral w"
lemma norm_neg_numeral [simp]: "norm (- numeral w::'a::complex_normed_algebra_1) = numeral w"
lemma norm_of_complex_add1 [simp]: "norm (of_real x + 1 :: 'a :: complex_normed_div_algebra) = ¦x + 1¦"
lemma norm_of_complex_addn [simp]:
  "norm (of_real x + numeral b :: 'a :: complex_normed_div_algebra) = ¦x + numeral b¦"
lemma norm_of_int [simp]: "norm (of_int z::'a::complex_normed_algebra_1) = ¦of_int z¦"
lemma norm_of_nat [simp]: "norm (of_nat n::'a::complex_normed_algebra_1) = of_nat n"
lemma nonzero_norm_inverse: "a ≠ 0 ⟹ norm (inverse a) = inverse (norm a)"
  for a :: "'a::complex_normed_div_algebra"
lemma norm_inverse: "norm (inverse a) = inverse (norm a)"
  for a :: "'a::{complex_normed_div_algebra,division_ring}"
lemma nonzero_norm_divide: "b ≠ 0 ⟹ norm (a / b) = norm a / norm b"
  for a b :: "'a::complex_normed_field"
lemma norm_divide: "norm (a / b) = norm a / norm b"
  for a b :: "'a::{complex_normed_field,field}"
lemma norm_inverse_le_norm:
  fixes x :: "'a::complex_normed_div_algebra"
  shows "r ≤ norm x ⟹ 0 < r ⟹ norm (inverse x) ≤ inverse r"
lemma norm_power_ineq: "norm (x ^ n) ≤ norm x ^ n"
  for x :: "'a::complex_normed_algebra_1"
lemma norm_power: "norm (x ^ n) = norm x ^ n"
  for x :: "'a::complex_normed_div_algebra"
lemma norm_power_int: "norm (power_int x n) = power_int (norm x) n"
  for x :: "'a::complex_normed_div_algebra"
lemma power_eq_imp_eq_norm:
  fixes w :: "'a::complex_normed_div_algebra"
  assumes eq: "w ^ n = z ^ n" and "n > 0"
    shows "norm w = norm z"
lemma power_eq_1_iff:
  fixes w :: "'a::complex_normed_div_algebra"
  shows "w ^ n = 1 ⟹ norm w = 1 ∨ n = 0"
lemma norm_mult_numeral1 [simp]: "norm (numeral w * a) = numeral w * norm a"
  for a b :: "'a::{complex_normed_field,field}"
lemma norm_mult_numeral2 [simp]: "norm (a * numeral w) = norm a * numeral w"
  for a b :: "'a::{complex_normed_field,field}"
lemma norm_divide_numeral [simp]: "norm (a / numeral w) = norm a / numeral w"
  for a b :: "'a::{complex_normed_field,field}"
lemma square_norm_one:
  fixes x :: "'a::complex_normed_div_algebra"
  assumes "x2 = 1"
  shows "norm x = 1"
lemma norm_less_p1: "norm x < norm (of_real (norm x) + 1 :: 'a)"
  for x :: "'a::complex_normed_algebra_1"
lemma prod_norm: "prod (λx. norm (f x)) A = norm (prod f A)"
  for f :: "'a ⇒ 'b::{comm_semiring_1,complex_normed_div_algebra}"
lemma norm_prod_le:
  "norm (prod f A) ≤ (∏a∈A. norm (f a :: 'a :: {complex_normed_algebra_1,comm_monoid_mult}))"
lemma norm_prod_diff:
  fixes z w :: "'i ⇒ 'a::{complex_normed_algebra_1, comm_monoid_mult}"
  shows "(⋀i. i ∈ I ⟹ norm (z i) ≤ 1) ⟹ (⋀i. i ∈ I ⟹ norm (w i) ≤ 1) ⟹
    norm ((∏i∈I. z i) - (∏i∈I. w i)) ≤ (∑i∈I. norm (z i - w i))"
lemma norm_power_diff:
  fixes z w :: "'a::{complex_normed_algebra_1, comm_monoid_mult}"
  assumes "norm z ≤ 1" "norm w ≤ 1"
  shows "norm (z^m - w^m) ≤ m * norm (z - w)"
*)

lemma norm_of_complex_add1 [simp]: "norm (of_complex x + 1 :: 'a :: complex_normed_div_algebra) = cmod (x + 1)"
  by (metis norm_of_complex of_complex_1 of_complex_add)

lemma norm_of_complex_addn [simp]:
  "norm (of_complex x + numeral b :: 'a :: complex_normed_div_algebra) = cmod (x + numeral b)"
  by (metis norm_of_complex of_complex_add of_complex_numeral)

lemma norm_of_complex_diff [simp]:
  "norm (of_complex b - of_complex a :: 'a::complex_normed_algebra_1) ≤ cmod (b - a)"
  by (metis norm_of_complex of_complex_diff order_refl)

subsection ‹Metric spaces›

(* Class metric_space is already defined in Real_Vector_Spaces and does not need changing here *)

text ‹Every normed vector space is a metric space.›
(* Already follows from complex_normed_vector < real_normed_vector < metric_space *)
(* instance complex_normed_vector < metric_space *)

subsection ‹Class instances for complex numbers›

instantiation complex :: complex_normed_field
begin

instance
  apply intro_classes
  by (simp add: norm_mult)

end

declare uniformity_Abort[where 'a=complex, code]

lemma dist_of_complex [simp]: "dist (of_complex x :: 'a) (of_complex y) = dist x y"
  for a :: "'a::complex_normed_div_algebra"
  by (metis dist_norm norm_of_complex of_complex_diff)

declare [[code abort: "open :: complex set ⇒ bool"]]

(* As far as I can tell, there is no analogue to this for complex:
instance real :: order_topology
instance real :: linear_continuum_topology ..

lemmas open_complex_greaterThan = open_greaterThan[where 'a=complex]
lemmas open_complex_lessThan = open_lessThan[where 'a=complex]
lemmas open_complex_greaterThanLessThan = open_greaterThanLessThan[where 'a=complex]
*)

lemma closed_complex_atMost: ‹closed {..a::complex}›
proof -
  have ‹{..a} = Im -` {Im a} ∩ Re -` {..Re a}›
    by (auto simp: less_eq_complex_def)
  also have ‹closed …›
    by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
  finally show ?thesis
    by -
qed

lemma closed_complex_atLeast: ‹closed {a::complex..}›
proof -
  have ‹{a..} = Im -` {Im a} ∩ Re -` {Re a..}›
    by (auto simp: less_eq_complex_def)
  also have ‹closed …›
    by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
  finally show ?thesis
    by -
qed

lemma closed_complex_atLeastAtMost: ‹closed {a::complex .. b}›
proof (cases ‹Im a = Im b›)
  case True
  have ‹{a..b} = Im -` {Im a} ∩ Re -` {Re a..Re b}›
    by (auto simp add: less_eq_complex_def intro!: True)
  also have ‹closed …›
    by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
  finally show ?thesis
    by -
next
  case False
  then have *: ‹{a..b} = {}›
    using less_eq_complex_def by auto
  show ?thesis
    by (simp add: *)
qed

(* As far as I can tell, there is no analogue to this for complex:
instance real :: ordered_real_vector
  by standard (auto intro: mult_left_mono mult_right_mono)
*)

(* subsection ‹Extra type constraints› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* These are already configured in Real_Vector_Spaces:

text ‹Only allow term‹open› in class ‹topological_space›.›
setup ‹Sign.add_const_constraint
  (const_name‹open›, SOME typ‹'a::topological_space set ⇒ bool›)›

text ‹Only allow term‹uniformity› in class ‹uniform_space›.›
setup ‹Sign.add_const_constraint
  (const_name‹uniformity›, SOME typ‹('a::uniformity × 'a) filter›)›

text ‹Only allow term‹dist› in class ‹metric_space›.›
setup ‹Sign.add_const_constraint
  (const_name‹dist›, SOME typ‹'a::metric_space ⇒ 'a ⇒ real›)›

text ‹Only allow term‹norm› in class ‹complex_normed_vector›.›
setup ‹Sign.add_const_constraint
  (const_name‹norm›, SOME typ‹'a::complex_normed_vector ⇒ real›)›
*)

subsection ‹Sign function›

(* Inherited from real_normed_vector:
lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
  for x :: "'a::complex_normed_vector"
lemma sgn_zero [simp]: "sgn (0::'a::complex_normed_vector) = 0"
lemma sgn_zero_iff: "sgn x = 0 ⟷ x = 0"
  for x :: "'a::complex_normed_vector"
lemma sgn_minus: "sgn (- x) = - sgn x"
  for x :: "'a::complex_normed_vector"
lemma sgn_one [simp]: "sgn (1::'a::complex_normed_algebra_1) = 1"
lemma sgn_mult: "sgn (x * y) = sgn x * sgn y"
  for x y :: "'a::complex_normed_div_algebra"
hide_fact (open) sgn_mult
lemma norm_conv_dist: "norm x = dist x 0"
declare norm_conv_dist [symmetric, simp]
lemma dist_0_norm [simp]: "dist 0 x = norm x"
  for x :: "'a::complex_normed_vector"
lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: complex_normed_algebra_1) = of_int ¦m - n¦"
lemma dist_of_nat:
  "dist (of_nat m) (of_nat n :: 'a :: complex_normed_algebra_1) = of_int ¦int m - int n¦"
*)

lemma sgn_scaleC: "sgn (scaleC r x) = scaleC (sgn r) (sgn x)"
  for x :: "'a::complex_normed_vector"
  by (simp add: scaleR_scaleC sgn_div_norm ac_simps)

lemma sgn_of_complex: "sgn (of_complex r :: 'a::complex_normed_algebra_1) = of_complex (sgn r)"
  unfolding of_complex_def by (simp only: sgn_scaleC sgn_one)

lemma complex_sgn_eq: "sgn x = x / ¦x¦"
  for x :: complex
  by (simp add: abs_complex_def scaleR_scaleC sgn_div_norm divide_inverse)

lemma czero_le_sgn_iff [simp]: "0 ≤ sgn x ⟷ 0 ≤ x"
  for x :: complex
  using cmod_eq_Re divide_eq_0_iff less_eq_complex_def by auto

lemma csgn_le_0_iff [simp]: "sgn x ≤ 0 ⟷ x ≤ 0"
  for x :: complex
  by (smt (verit, best) czero_le_sgn_iff Im_sgn Re_sgn divide_eq_0_iff dual_order.eq_iff less_eq_complex_def sgn_zero_iff zero_complex.sel(1) zero_complex.sel(2))


subsection ‹Bounded Linear and Bilinear Operators›

lemma clinearI: "clinear f"
  if "⋀b1 b2. f (b1 + b2) = f b1 + f b2"
    "⋀r b. f (r *C b) = r *C f b"
  using that
  by unfold_locales (auto simp: algebra_simps)

lemma clinear_iff:
  "clinear f ⟷ (∀x y. f (x + y) = f x + f y) ∧ (∀c x. f (c *C x) = c *C f x)"
  (is "clinear f ⟷ ?rhs")
proof
  assume "clinear f"
  then interpret f: clinear f .
  show "?rhs"
    by (simp add: f.add f.scale complex_vector.linear_scale f.clinear_axioms)
next
  assume "?rhs"
  then show "clinear f" by (intro clinearI) auto
qed

lemmas clinear_scaleC_left = complex_vector.linear_scale_left
lemmas clinear_imp_scaleC = complex_vector.linear_imp_scale

corollary complex_clinearD:
  fixes f :: "complex ⇒ complex"
  assumes "clinear f" obtains c where "f = (*) c"
  by (rule clinear_imp_scaleC [OF assms]) (force simp: scaleC_conv_of_complex)

lemma clinear_times_of_complex: "clinear (λx. a * of_complex x)"
  by (auto intro!: clinearI simp: distrib_left)
    (metis mult_scaleC_right scaleC_conv_of_complex)

locale bounded_clinear = clinear f for f :: "'a::complex_normed_vector ⇒ 'b::complex_normed_vector" +
  assumes bounded: "∃K. ∀x. norm (f x) ≤ norm x * K"
begin

(* Not present in Real_Vector_Spaces. *)
sublocale real: bounded_linear
  ― ‹Gives access to all lemmas from locale‹bounded_linear› using prefix ‹real.››
  apply standard
  by (auto simp add: add scaleR_scaleC scale bounded)

lemmas pos_bounded = real.pos_bounded (* "∃K>0. ∀x. norm (f x) ≤ norm x * K" *)

(* Inherited from bounded_linear *)
lemmas nonneg_bounded = real.nonneg_bounded (* "∃K≥0. ∀x. norm (f x) ≤ norm x * K" *)

lemma clinear: "clinear f"
  by (fact local.clinear_axioms)

end

lemma bounded_clinear_intro:
  assumes "⋀x y. f (x + y) = f x + f y"
    and "⋀r x. f (scaleC r x) = scaleC r (f x)"
    and "⋀x. norm (f x) ≤ norm x * K"
  shows "bounded_clinear f"
  by standard (blast intro: assms)+

locale bounded_cbilinear =
  fixes prod :: "'a::complex_normed_vector ⇒ 'b::complex_normed_vector ⇒ 'c::complex_normed_vector"
    (infixl "**" 70)
  assumes add_left: "prod (a + a') b = prod a b + prod a' b"
    and add_right: "prod a (b + b') = prod a b + prod a b'"
    and scaleC_left: "prod (scaleC r a) b = scaleC r (prod a b)"
    and scaleC_right: "prod a (scaleC r b) = scaleC r (prod a b)"
    and bounded: "∃K. ∀a b. norm (prod a b) ≤ norm a * norm b * K"
begin

(* Not present in Real_Vector_Spaces. *)
sublocale real: bounded_bilinear
  ― ‹Gives access to all lemmas from locale‹bounded_bilinear› using prefix ‹real.››
  apply standard
  by (auto simp add: add_left add_right scaleR_scaleC scaleC_left scaleC_right bounded)

lemmas pos_bounded = real.pos_bounded (* "∃K>0. ∀a b. norm (a ** b) ≤ norm a * norm b * K" *)
lemmas nonneg_bounded = real.nonneg_bounded (* "∃K≥0. ∀a b. norm (a ** b) ≤ norm a * norm b * K" *)
lemmas additive_right = real.additive_right (* "additive (λb. prod a b)" *)
lemmas additive_left = real.additive_left (* "additive (λa. prod a b)" *)
lemmas zero_left = real.zero_left (* "prod 0 b = 0" *)
lemmas zero_right = real.zero_right (* "prod a 0 = 0" *)
lemmas minus_left = real.minus_left (* "prod (- a) b = - prod a b" *)
lemmas minus_right = real.minus_right (* "prod a (- b) = - prod a b" *)
lemmas diff_left = real.diff_left (* "prod (a - a') b = prod a b - prod a' b" *)
lemmas diff_right = real.diff_right (* "prod a (b - b') = prod a b - prod a b'" *)
lemmas sum_left = real.sum_left (* "prod (sum g S) x = sum ((λi. prod (g i) x)) S" *)
lemmas sum_right = real.sum_right (* "prod x (sum g S) = sum ((λi. (prod x (g i)))) S" *)
lemmas prod_diff_prod = real.prod_diff_prod (* "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" *)

lemma bounded_clinear_left: "bounded_clinear (λa. a ** b)"
proof -
  obtain K where "⋀a b. norm (a ** b) ≤ norm a * norm b * K"
    using pos_bounded by blast
  then show ?thesis
    by (rule_tac K="norm b * K" in bounded_clinear_intro) (auto simp: algebra_simps scaleC_left add_left)
qed

lemma bounded_clinear_right: "bounded_clinear (λb. a ** b)"
proof -
  obtain K where "⋀a b. norm (a ** b) ≤ norm a * norm b * K"
    using pos_bounded by blast
  then show ?thesis
    by (rule_tac K="norm a * K" in bounded_clinear_intro) (auto simp: algebra_simps scaleC_right add_right)
qed

lemma flip: "bounded_cbilinear (λx y. y ** x)"
proof
  show "∃K. ∀a b. norm (b ** a) ≤ norm a * norm b * K"
    by (metis bounded mult.commute)
qed (simp_all add: add_right add_left scaleC_right scaleC_left)

lemma comp1:
  assumes "bounded_clinear g"
  shows "bounded_cbilinear (λx. (**) (g x))"
proof
  interpret g: bounded_clinear g by fact
  show "⋀a a' b. g (a + a') ** b = g a ** b + g a' ** b"
    "⋀a b b'. g a ** (b + b') = g a ** b + g a ** b'"
    "⋀r a b. g (r *C a) ** b = r *C (g a ** b)"
    "⋀a r b. g a ** (r *C b) = r *C (g a ** b)"
    by (auto simp: g.add add_left add_right g.scaleC scaleC_left scaleC_right)
  have "bounded_bilinear (λa b. g a ** b)"
    using g.real.bounded_linear by (rule real.comp1)
  then show "∃K. ∀a b. norm (g a ** b) ≤ norm a * norm b * K"
    by (rule bounded_bilinear.bounded)
qed

lemma comp: "bounded_clinear f ⟹ bounded_clinear g ⟹ bounded_cbilinear (λx y. f x ** g y)"
  by (rule bounded_cbilinear.flip[OF bounded_cbilinear.comp1[OF bounded_cbilinear.flip[OF comp1]]])

end (* locale bounded_cbilinear *)

lemma bounded_clinear_ident[simp]: "bounded_clinear (λx. x)"
  by standard (auto intro!: exI[of _ 1])

lemma bounded_clinear_zero[simp]: "bounded_clinear (λx. 0)"
  by standard (auto intro!: exI[of _ 1])

lemma bounded_clinear_add:
  assumes "bounded_clinear f"
    and "bounded_clinear g"
  shows "bounded_clinear (λx. f x + g x)"
proof -
  interpret f: bounded_clinear f by fact
  interpret g: bounded_clinear g by fact
  show ?thesis
  proof
    from f.bounded obtain Kf where Kf: "norm (f x) ≤ norm x * Kf" for x
      by blast
    from g.bounded obtain Kg where Kg: "norm (g x) ≤ norm x * Kg" for x
      by blast
    show "∃K. ∀x. norm (f x + g x) ≤ norm x * K"
      using add_mono[OF Kf Kg]
      by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans)
  qed (simp_all add: f.add g.add f.scaleC g.scaleC scaleC_add_right)
qed

lemma bounded_clinear_minus:
  assumes "bounded_clinear f"
  shows "bounded_clinear (λx. - f x)"
proof -
  interpret f: bounded_clinear f by fact
  show ?thesis
    by unfold_locales (simp_all add: f.add f.scaleC f.bounded)
qed

lemma bounded_clinear_sub: "bounded_clinear f ⟹ bounded_clinear g ⟹ bounded_clinear (λx. f x - g x)"
  using bounded_clinear_add[of f "λx. - g x"] bounded_clinear_minus[of g]
  by (auto simp: algebra_simps)

lemma bounded_clinear_sum:
  fixes f :: "'i ⇒ 'a::complex_normed_vector ⇒ 'b::complex_normed_vector"
  shows "(⋀i. i ∈ I ⟹ bounded_clinear (f i)) ⟹ bounded_clinear (λx. ∑i∈I. f i x)"
  by (induct I rule: infinite_finite_induct) (auto intro!: bounded_clinear_add)

lemma bounded_clinear_compose:
  assumes "bounded_clinear f"
    and "bounded_clinear g"
  shows "bounded_clinear (λx. f (g x))"
proof
  interpret f: bounded_clinear f by fact
  interpret g: bounded_clinear g by fact
  show "f (g (x + y)) = f (g x) + f (g y)" for x y
    by (simp only: f.add g.add)
  show "f (g (scaleC r x)) = scaleC r (f (g x))" for r x
    by (simp only: f.scaleC g.scaleC)
  from f.pos_bounded obtain Kf where f: "⋀x. norm (f x) ≤ norm x * Kf" and Kf: "0 < Kf"
    by blast
  from g.pos_bounded obtain Kg where g: "⋀x. norm (g x) ≤ norm x * Kg"
    by blast
  show "∃K. ∀x. norm (f (g x)) ≤ norm x * K"
  proof (intro exI allI)
    fix x
    have "norm (f (g x)) ≤ norm (g x) * Kf"
      using f .
    also have "… ≤ (norm x * Kg) * Kf"
      using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
    also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
      by (rule mult.assoc)
    finally show "norm (f (g x)) ≤ norm x * (Kg * Kf)" .
  qed
qed

lemma bounded_cbilinear_mult: "bounded_cbilinear ((*) :: 'a ⇒ 'a ⇒ 'a::complex_normed_algebra)"
proof (rule bounded_cbilinear.intro)
  show "∃K. ∀a b::'a. norm (a * b) ≤ norm a * norm b * K"
    by (rule_tac x=1 in exI) (simp add: norm_mult_ineq)
qed (auto simp: algebra_simps)

lemma bounded_clinear_mult_left: "bounded_clinear (λx::'a::complex_normed_algebra. x * y)"
  using bounded_cbilinear_mult
  by (rule bounded_cbilinear.bounded_clinear_left)

lemma bounded_clinear_mult_right: "bounded_clinear (λy::'a::complex_normed_algebra. x * y)"
  using bounded_cbilinear_mult
  by (rule bounded_cbilinear.bounded_clinear_right)

lemmas bounded_clinear_mult_const =
  bounded_clinear_mult_left [THEN bounded_clinear_compose]

lemmas bounded_clinear_const_mult =
  bounded_clinear_mult_right [THEN bounded_clinear_compose]

lemma bounded_clinear_divide: "bounded_clinear (λx. x / y)"
  for y :: "'a::complex_normed_field"
  unfolding divide_inverse by (rule bounded_clinear_mult_left)

lemma bounded_cbilinear_scaleC: "bounded_cbilinear scaleC"
proof (rule bounded_cbilinear.intro)
  obtain K where K: ‹∀a (b::'a). norm b ≤ norm b * K›
    using less_eq_real_def by auto
  show "∃K. ∀a (b::'a). norm (a *C b) ≤ norm a * norm b * K"
    apply (rule exI[where x=K]) using K
    by (metis norm_scaleC)
qed (auto simp: algebra_simps)

lemma bounded_clinear_scaleC_left: "bounded_clinear (λc. scaleC c x)"
  using bounded_cbilinear_scaleC
  by (rule bounded_cbilinear.bounded_clinear_left)

lemma bounded_clinear_scaleC_right: "bounded_clinear (λx. scaleC c x)"
  using bounded_cbilinear_scaleC
  by (rule bounded_cbilinear.bounded_clinear_right)

lemmas bounded_clinear_scaleC_const =
  bounded_clinear_scaleC_left[THEN bounded_clinear_compose]

lemmas bounded_clinear_const_scaleC =
  bounded_clinear_scaleC_right[THEN bounded_clinear_compose]

lemma bounded_clinear_of_complex: "bounded_clinear (λr. of_complex r)"
  unfolding of_complex_def by (rule bounded_clinear_scaleC_left)

lemma complex_bounded_clinear: "bounded_clinear f ⟷ (∃c::complex. f = (λx. x * c))"
  for f :: "complex ⇒ complex"
proof -
  {
    fix x
    assume "bounded_clinear f"
    then interpret bounded_clinear f .
    from scaleC[of x 1] have "f x = x * f 1"
      by simp
  }
  then show ?thesis
    by (auto intro: exI[of _ "f 1"] bounded_clinear_mult_left)
qed

(* Inherited from real_normed_algebra_1 *)
(* instance complex_normed_algebra_1 ⊆ perfect_space *)

(* subsection ‹Filters and Limits on Metric Space› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* Not specific to real/complex *)
(* lemma (in metric_space) nhds_metric: "nhds x = (INF e∈{0 <..}. principal {y. dist y x < e})" *)
(* lemma (in metric_space) tendsto_iff: "(f ⤏ l) F ⟷ (∀e>0. eventually (λx. dist (f x) l < e) F)" *)
(* lemma tendsto_dist_iff: "((f ⤏ l) F) ⟷ (((λx. dist (f x) l) ⤏ 0) F)" *)
(* lemma (in metric_space) tendstoI [intro?]:
  "(⋀e. 0 < e ⟹ eventually (λx. dist (f x) l < e) F) ⟹ (f ⤏ l) F" *)
(* lemma (in metric_space) tendstoD: "(f ⤏ l) F ⟹ 0 < e ⟹ eventually (λx. dist (f x) l < e) F" *)
(* lemma (in metric_space) eventually_nhds_metric:
  "eventually P (nhds a) ⟷ (∃d>0. ∀x. dist x a < d ⟶ P x)" *)
(* lemma eventually_at: "eventually P (at a within S) ⟷ (∃d>0. ∀x∈S. x ≠ a ∧ dist x a < d ⟶ P x)"
  for a :: "'a :: metric_space" *)
(* lemma frequently_at: "frequently P (at a within S) ⟷ (∀d>0. ∃x∈S. x ≠ a ∧ dist x a < d ∧ P x)"
  for a :: "'a :: metric_space" *)
(* lemma eventually_at_le: "eventually P (at a within S) ⟷ (∃d>0. ∀x∈S. x ≠ a ∧ dist x a ≤ d ⟶ P x)"
  for a :: "'a::metric_space" *)

(* Does not work in complex case because it needs complex :: order_toplogy *)
(* lemma eventually_at_left_real: "a > (b :: real) ⟹ eventually (λx. x ∈ {b<..<a}) (at_left a)" *)
(* lemma eventually_at_right_real: "a < (b :: real) ⟹ eventually (λx. x ∈ {a<..<b}) (at_right a)" *)

(* Not specific to real/complex *)
(* lemma metric_tendsto_imp_tendsto:
  fixes a :: "'a :: metric_space"
    and b :: "'b :: metric_space"
  assumes f: "(f ⤏ a) F"
    and le: "eventually (λx. dist (g x) b ≤ dist (f x) a) F"
  shows "(g ⤏ b) F" *)

(* Not sure if this makes sense in the complex case *)
(* lemma filterlim_complex_sequentially: "LIM x sequentially. (of_nat x :: complex) :> at_top" *)

(* Not specific to real/complex *)
(* lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top" *)
(* lemma filterlim_floor_sequentially: "filterlim floor at_top at_top" *)

(* Not sure if this makes sense in the complex case *)
(* lemma filterlim_sequentially_iff_filterlim_real:
  "filterlim f sequentially F ⟷ filterlim (λx. real (f x)) at_top F" (is "?lhs = ?rhs") *)


subsubsection ‹Limits of Sequences›

(* Not specific to real/complex *)
(* lemma lim_sequentially: "X ⇢ L ⟷ (∀r>0. ∃no. ∀n≥no. dist (X n) L < r)"
  for L :: "'a::metric_space" *)
(* lemmas LIMSEQ_def = lim_sequentially  (*legacy binding*) *)
(* lemma LIMSEQ_iff_nz: "X ⇢ L ⟷ (∀r>0. ∃no>0. ∀n≥no. dist (X n) L < r)"
  for L :: "'a::metric_space" *)
(* lemma metric_LIMSEQ_I: "(⋀r. 0 < r ⟹ ∃no. ∀n≥no. dist (X n) L < r) ⟹ X ⇢ L"
  for L :: "'a::metric_space" *)
(* lemma metric_LIMSEQ_D: "X ⇢ L ⟹ 0 < r ⟹ ∃no. ∀n≥no. dist (X n) L < r"
  for L :: "'a::metric_space" *)
(* lemma LIMSEQ_norm_0:
  assumes  "⋀n::nat. norm (f n) < 1 / real (Suc n)"
  shows "f ⇢ 0" *)

(* subsubsection ‹Limits of Functions› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* Not specific to real/complex *)
(* lemma LIM_def: "f ─a→ L ⟷ (∀r > 0. ∃s > 0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r)"
  for a :: "'a::metric_space" and L :: "'b::metric_space" *)
(* lemma metric_LIM_I:
  "(⋀r. 0 < r ⟹ ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r) ⟹ f ─a→ L"
  for a :: "'a::metric_space" and L :: "'b::metric_space" *)
(* lemma metric_LIM_D: "f ─a→ L ⟹ 0 < r ⟹ ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r"
  for a :: "'a::metric_space" and L :: "'b::metric_space" *)
(* lemma metric_LIM_imp_LIM:
  fixes l :: "'a::metric_space"
    and m :: "'b::metric_space"
  assumes f: "f ─a→ l"
    and le: "⋀x. x ≠ a ⟹ dist (g x) m ≤ dist (f x) l"
  shows "g ─a→ m" *)
(* lemma metric_LIM_equal2:
  fixes a :: "'a::metric_space"
  assumes "g ─a→ l" "0 < R"
    and "⋀x. x ≠ a ⟹ dist x a < R ⟹ f x = g x"
  shows "f ─a→ l" *)
(* lemma metric_LIM_compose2:
  fixes a :: "'a::metric_space"
  assumes f: "f ─a→ b"
    and g: "g ─b→ c"
    and inj: "∃d>0. ∀x. x ≠ a ∧ dist x a < d ⟶ f x ≠ b"
  shows "(λx. g (f x)) ─a→ c" *)
(* lemma metric_isCont_LIM_compose2:
  fixes f :: "'a :: metric_space ⇒ _"
  assumes f [unfolded isCont_def]: "isCont f a"
    and g: "g ─f a→ l"
    and inj: "∃d>0. ∀x. x ≠ a ∧ dist x a < d ⟶ f x ≠ f a"
  shows "(λx. g (f x)) ─a→ l" *)


(* subsection ‹Complete metric spaces› *)
(* Everything is commented out, so we comment out the heading, too. *)

subsection ‹Cauchy sequences›

(* Not specific to real/complex *)
(* lemma (in metric_space) Cauchy_def: "Cauchy X = (∀e>0. ∃M. ∀m≥M. ∀n≥M. dist (X m) (X n) < e)" *)
(* lemma (in metric_space) Cauchy_altdef: "Cauchy f ⟷ (∀e>0. ∃M. ∀m≥M. ∀n>m. dist (f m) (f n) < e)" *)
(* lemma (in metric_space) Cauchy_altdef2: "Cauchy s ⟷ (∀e>0. ∃N::nat. ∀n≥N. dist(s n)(s N) < e)" (is "?lhs = ?rhs") *)
(* lemma (in metric_space) metric_CauchyI:
  "(⋀e. 0 < e ⟹ ∃M. ∀m≥M. ∀n≥M. dist (X m) (X n) < e) ⟹ Cauchy X" *)
(* lemma (in metric_space) CauchyI':
  "(⋀e. 0 < e ⟹ ∃M. ∀m≥M. ∀n>m. dist (X m) (X n) < e) ⟹ Cauchy X" *)
(* lemma (in metric_space) metric_CauchyD:
  "Cauchy X ⟹ 0 < e ⟹ ∃M. ∀m≥M. ∀n≥M. dist (X m) (X n) < e" *)
(* lemma (in metric_space) metric_Cauchy_iff2:
  "Cauchy X = (∀j. (∃M. ∀m ≥ M. ∀n ≥ M. dist (X m) (X n) < inverse(real (Suc j))))" *)

lemma cCauchy_iff2: "Cauchy X ⟷ (∀j. (∃M. ∀m ≥ M. ∀n ≥ M. cmod (X m - X n) < inverse (real (Suc j))))"
  by (simp only: metric_Cauchy_iff2 dist_complex_def)

(* Not specific to real/complex *)
(* lemma lim_1_over_n [tendsto_intros]: "((λn. 1 / of_nat n) ⤏ (0::'a::complex_normed_field)) sequentially" *)
(* lemma (in metric_space) complete_def:
  shows "complete S = (∀f. (∀n. f n ∈ S) ∧ Cauchy f ⟶ (∃l∈S. f ⇢ l))" *)
(* lemma (in metric_space) totally_bounded_metric:
  "totally_bounded S ⟷ (∀e>0. ∃k. finite k ∧ S ⊆ (⋃x∈k. {y. dist x y < e}))" *)

(* subsubsection ‹Cauchy Sequences are Convergent› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* Not specific to real/complex *)
(* class complete_space *)
(* lemma Cauchy_convergent_iff: "Cauchy X ⟷ convergent X"
  for X :: "nat ⇒ 'a::complete_space" *)

(* text ‹To prove that a Cauchy sequence converges, it suffices to show that a subsequence converges.› *)

(* Not specific to real/complex *)
(* lemma Cauchy_converges_subseq:
  fixes u::"nat ⇒ 'a::metric_space"
  assumes "Cauchy u"
    "strict_mono r"
    "(u ∘ r) ⇢ l"
  shows "u ⇢ l" *)

subsection ‹The set of complex numbers is a complete metric space›

text ‹
  Proof that Cauchy sequences converge based on the one from
  🌐‹http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html›
›

text ‹
  If sequence term‹X› is Cauchy, then its limit is the lub of
  term‹{r::real. ∃N. ∀n≥N. r < X n}›
›

lemma complex_increasing_LIMSEQ:
  fixes f :: "nat ⇒ complex"
  assumes inc: "⋀n. f n ≤ f (Suc n)"
    and bdd: "⋀n. f n ≤ l"
    and en: "⋀e. 0 < e ⟹ ∃n. l ≤ f n + e"
  shows "f ⇢ l"
proof -
  have ‹(λn. Re (f n)) ⇢ Re l›
    apply (rule increasing_LIMSEQ)
    using assms apply (auto simp: less_eq_complex_def less_complex_def)
    by (metis Im_complex_of_real Re_complex_of_real)
  moreover have ‹Im (f n) = Im l› for n
    using bdd by (auto simp: less_eq_complex_def)
  then have ‹(λn. Im (f n)) ⇢ Im l›
    by auto
  ultimately show ‹f ⇢ l›
    by (simp add: tendsto_complex_iff)
qed

lemma complex_Cauchy_convergent:
  fixes X :: "nat ⇒ complex"
  assumes X: "Cauchy X"
  shows "convergent X"
  using assms by (rule Cauchy_convergent)

instance complex :: complete_space
  by intro_classes (rule complex_Cauchy_convergent)

class cbanach = complex_normed_vector + complete_space

(* Not present in Real_Vector_Spaces *)
subclass (in cbanach) banach ..

instance complex :: banach ..

(* Don't know if this holds in the complex case *)
(* lemma tendsto_at_topI_sequentially:
  fixes f :: "complex ⇒ 'b::first_countable_topology"
  assumes *: "⋀X. filterlim X at_top sequentially ⟹ (λn. f (X n)) ⇢ y"
  shows "(f ⤏ y) at_top" *)
(* lemma tendsto_at_topI_sequentially_real:
  fixes f :: "real ⇒ real"
  assumes mono: "mono f"
    and limseq: "(λn. f (real n)) ⇢ y"
  shows "(f ⤏ y) at_top" *)

end