# 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

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])+

(* 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"

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"

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"

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)

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"

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 ∈ ℂ"

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

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

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)"
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¦"
"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 "x⇧2 = 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)

"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›.›
(\<^const_name>‹open›, SOME \<^typ>‹'a::topological_space set ⇒ bool›)›

text ‹Only allow \<^term>‹uniformity› in class ‹uniform_space›.›
(\<^const_name>‹uniformity›, SOME \<^typ>‹('a::uniformity × 'a) filter›)›

text ‹Only allow \<^term>‹dist› in class ‹metric_space›.›
(\<^const_name>‹dist›, SOME \<^typ>‹'a::metric_space ⇒ 'a ⇒ real›)›

text ‹Only allow \<^term>‹norm› in class ‹complex_normed_vector›.›
(\<^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)

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)"
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])

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

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