Theory Complex_Euclidean_Space0

```(*  Title:      HOL/Analysis/Euclidean_Space.thy
Author:     Johannes Hölzl, TU München
Author:     Brian Huffman, Portland State University
*)

section ‹‹Complex_Euclidean_Space0› -- Finite-Dimensional Inner Product Spaces›

theory Complex_Euclidean_Space0
imports
"HOL-Analysis.L2_Norm"
"Complex_Inner_Product"
"HOL-Analysis.Product_Vector"
"HOL-Library.Rewrite"
begin

(* subsection✐‹tag unimportant› ‹Interlude: Some properties of real sets› *)

(* Complex analogue not needed *)
(* lemma seq_mono_lemma:
assumes "∀(n::nat) ≥ m. (d n :: real) < e n"
and "∀n ≥ m. e n ≤ e m"
shows "∀n ≥ m. d n < e m" *)

subsection ‹Type class of Euclidean spaces›

class ceuclidean_space = complex_inner +
fixes CBasis :: "'a set"
assumes nonempty_CBasis [simp]: "CBasis ≠ {}"
assumes finite_CBasis [simp]: "finite CBasis"
assumes cinner_CBasis:
"⟦u ∈ CBasis; v ∈ CBasis⟧ ⟹ cinner u v = (if u = v then 1 else 0)"
assumes ceuclidean_all_zero_iff:
"(∀u∈CBasis. cinner x u = 0) ⟷ (x = 0)"

syntax "_type_cdimension" :: "type ⇒ nat"  ("(1CDIM/(1'(_')))")
syntax_consts "_type_cdimension" ⇌ card
translations "CDIM('a)" ⇀ "CONST card (CONST CBasis :: 'a set)"
typed_print_translation ‹
[(\<^const_syntax>‹card›,
fn ctxt => fn _ => fn [Const (\<^const_syntax>‹CBasis›, Type (\<^type_name>‹set›, [T]))] =>
Syntax.const \<^syntax_const>‹_type_cdimension› \$ Syntax_Phases.term_of_typ ctxt T)]
›

lemma (in ceuclidean_space) norm_CBasis[simp]: "u ∈ CBasis ⟹ norm u = 1"
unfolding norm_eq_sqrt_cinner by (simp add: cinner_CBasis)

lemma (in ceuclidean_space) cinner_same_CBasis[simp]: "u ∈ CBasis ⟹ cinner u u = 1"

lemma (in ceuclidean_space) cinner_not_same_CBasis: "u ∈ CBasis ⟹ v ∈ CBasis ⟹ u ≠ v ⟹ cinner u v = 0"

lemma (in ceuclidean_space) sgn_CBasis: "u ∈ CBasis ⟹ sgn u = u"
unfolding sgn_div_norm by (simp add: scaleR_one)

lemma (in ceuclidean_space) CBasis_zero [simp]: "0 ∉ CBasis"
proof
assume "0 ∈ CBasis" thus "False"
using cinner_CBasis [of 0 0] by simp
qed

lemma (in ceuclidean_space) nonzero_CBasis: "u ∈ CBasis ⟹ u ≠ 0"
by clarsimp

lemma (in ceuclidean_space) SOME_CBasis: "(SOME i. i ∈ CBasis) ∈ CBasis"
by (metis ex_in_conv nonempty_CBasis someI_ex)

lemma norm_some_CBasis [simp]: "norm (SOME i. i ∈ CBasis) = 1"

lemma (in ceuclidean_space) cinner_sum_left_CBasis[simp]:
"b ∈ CBasis ⟹ cinner (∑i∈CBasis. f i *⇩C i) b = cnj (f b)"

(* Not present in Euclidean_Space *)
(* lemma (in ceuclidean_space) cinner_sum_right_CBasis[simp]:
"b ∈ CBasis ⟹ cinner b (∑i∈CBasis. f i *⇩C i) = f b"
by (metis (mono_tags, lifting) cinner_commute cinner_sum_left_CBasis comm_monoid_add_class.sum.cong complex_cnj_cnj) *)

lemma (in ceuclidean_space) ceuclidean_eqI:
assumes b: "⋀b. b ∈ CBasis ⟹ cinner x b = cinner y b" shows "x = y"
proof -
from b have "∀b∈CBasis. cinner (x - y) b = 0"
then show "x = y"
qed

lemma (in ceuclidean_space) ceuclidean_eq_iff:
"x = y ⟷ (∀b∈CBasis. cinner x b = cinner y b)"
by (auto intro: ceuclidean_eqI)

lemma (in ceuclidean_space) ceuclidean_representation_sum:
"(∑i∈CBasis. f i *⇩C i) = b ⟷ (∀i∈CBasis. f i = cnj (cinner b i))"
apply (subst ceuclidean_eq_iff)
apply simp by (metis complex_cnj_cnj cinner_commute)

lemma (in ceuclidean_space) ceuclidean_representation_sum':
"b = (∑i∈CBasis. f i *⇩C i) ⟷ (∀i∈CBasis. f i = cinner i b)"
apply (metis ceuclidean_representation_sum cinner_commute)
by (metis local.ceuclidean_representation_sum local.cinner_commute)

lemma (in ceuclidean_space) ceuclidean_representation: "(∑b∈CBasis. cinner b x *⇩C b) = x"
unfolding ceuclidean_representation_sum
using local.cinner_commute by blast

lemma (in ceuclidean_space) ceuclidean_cinner: "cinner x y = (∑b∈CBasis. cinner x b * cnj (cinner y b))"
apply (subst (1 2) ceuclidean_representation [symmetric])
apply (simp add: cinner_sum_right cinner_CBasis ac_simps)
by (metis local.cinner_commute mult.commute)

lemma (in ceuclidean_space) choice_CBasis_iff:
fixes P :: "'a ⇒ complex ⇒ bool"
shows "(∀i∈CBasis. ∃x. P i x) ⟷ (∃x. ∀i∈CBasis. P i (cinner x i))"
unfolding bchoice_iff
proof safe
fix f assume "∀i∈CBasis. P i (f i)"
then show "∃x. ∀i∈CBasis. P i (cinner x i)"
by (auto intro!: exI[of _ "∑i∈CBasis. cnj (f i) *⇩C i"])
qed auto

lemma (in ceuclidean_space) bchoice_CBasis_iff:
fixes P :: "'a ⇒ complex ⇒ bool"
shows "(∀i∈CBasis. ∃x∈A. P i x) ⟷ (∃x. ∀i∈CBasis. cinner x i ∈ A ∧ P i (cinner x i))"

lemma (in ceuclidean_space) ceuclidean_representation_sum_fun:
"(λx. ∑b∈CBasis. cinner b (f x) *⇩C b) = f"
apply (rule ext)
by (meson local.cinner_commute)

lemma euclidean_isCont:
assumes "⋀b. b ∈ CBasis ⟹ isCont (λx. (cinner b (f x)) *⇩C b) x"
shows "isCont f x"
apply (subst ceuclidean_representation_sum_fun [symmetric])
apply (rule isCont_sum)
by (blast intro: assms)

lemma CDIM_positive [simp]: "0 < CDIM('a::ceuclidean_space)"

lemma CDIM_ge_Suc0 [simp]: "Suc 0 ≤ card CBasis"
by (meson CDIM_positive Suc_leI)

lemma sum_cinner_CBasis_scaleC [simp]:
fixes f :: "'a::ceuclidean_space ⇒ 'b::complex_vector"
assumes "b ∈ CBasis" shows "(∑i∈CBasis. (cinner i b) *⇩C f i) = f b"

lemma sum_cinner_CBasis_eq [simp]:
assumes "b ∈ CBasis" shows "(∑i∈CBasis. (cinner i b) * f i) = f b"

lemma sum_if_cinner [simp]:
assumes "i ∈ CBasis" "j ∈ CBasis"
shows "cinner (∑k∈CBasis. if k = i then f i *⇩C i else g k *⇩C k) j = (if j=i then cnj (f j) else cnj (g j))"
proof (cases "i=j")
case True
with assms show ?thesis
by (auto simp: cinner_sum_left if_distrib [of "λx. cinner x j"] cinner_CBasis cong: if_cong)
next
case False
have "(∑k∈CBasis. cinner (if k = i then f i *⇩C i else g k *⇩C k) j) =
(∑k∈CBasis. if k = j then cnj (g k) else 0)"
apply (rule sum.cong)
using False assms by (auto simp: cinner_CBasis)
also have "... = cnj (g j)"
using assms by auto
finally show ?thesis
using False by (auto simp: cinner_sum_left)
qed

lemma norm_le_componentwise:
"(⋀b. b ∈ CBasis ⟹ cmod(cinner x b) ≤ cmod(cinner y b)) ⟹ norm x ≤ norm y"
apply (auto simp: cnorm_le ceuclidean_cinner [of x x] ceuclidean_cinner [of y y] power2_eq_square intro!: sum_mono)
by (smt (verit, best) mult.commute sum.cong)

lemma CBasis_le_norm: "b ∈ CBasis ⟹ cmod (cinner x b) ≤ norm x"
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp

lemma norm_bound_CBasis_le: "b ∈ CBasis ⟹ norm x ≤ e ⟹ cmod (inner x b) ≤ e"
by (metis inner_commute mult.left_neutral norm_CBasis norm_of_real order_trans real_inner_class.Cauchy_Schwarz_ineq2)

lemma norm_bound_CBasis_lt: "b ∈ CBasis ⟹ norm x < e ⟹ cmod (inner x b) < e"
by (metis inner_commute le_less_trans mult.left_neutral norm_CBasis norm_of_real real_inner_class.Cauchy_Schwarz_ineq2)

lemma cnorm_le_l1: "norm x ≤ (∑b∈CBasis. cmod (cinner x b))"
apply (subst ceuclidean_representation[of x, symmetric])
apply (rule order_trans[OF norm_sum])
apply (auto intro!: sum_mono)
by (metis cinner_commute complex_inner_1_left complex_inner_class.Cauchy_Schwarz_ineq2 mult.commute mult.left_neutral norm_one)

(* Maybe it holds in the complex case but the proof does not adapt trivially *)
(* lemma csum_norm_allsubsets_bound:
fixes f :: "'a ⇒ 'n::ceuclidean_space"
assumes fP: "finite P"
and fPs: "⋀Q. Q ⊆ P ⟹ norm (sum f Q) ≤ e"
shows "(∑x∈P. norm (f x)) ≤ 2 * real CDIM('n) * e" *)

(* subsection✐‹tag unimportant› ‹Subclass relationships› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* If we include this, instantiation prod :: (ceuclidean_space, ceuclidean_space) ceuclidean_space below fails *)
(* instance ceuclidean_space ⊆ perfect_space
proof
fix x :: 'a show "¬ open {x}"
proof
assume "open {x}"
then obtain e where "0 < e" and e: "∀y. dist y x < e ⟶ y = x"
unfolding open_dist by fast
define y where "y = x + scaleR (e/2) (SOME b. b ∈ CBasis)"
have [simp]: "(SOME b. b ∈ CBasis) ∈ CBasis"
by (rule someI_ex) (auto simp: ex_in_conv)
from ‹0 < e› have "y ≠ x"
unfolding y_def by (auto intro!: nonzero_CBasis)
from ‹0 < e› have "dist y x < e"
unfolding y_def by (simp add: dist_norm)
from ‹y ≠ x› and ‹dist y x < e› show "False"
using e by simp
qed
qed *)

subsection ‹Class instances›

subsubsection✐‹tag unimportant› ‹Type \<^typ>‹complex››

(* No analogue *)
(* instantiation real :: ceuclidean_space *)

instantiation complex :: ceuclidean_space
begin

definition
[simp]: "CBasis = {1::complex}"

instance
by standard auto

end

lemma CDIM_complex[simp]: "CDIM(complex) = 1"
by simp

(* lemma CDIM_complex[simp]: "DIM(complex) = 2"
lemma complex_CBasis_1 [iff]: "(1::complex) ∈ CBasis"
lemma complex_CBasis_i [iff]: "𝗂 ∈ CBasis" *)

subsubsection✐‹tag unimportant› ‹Type \<^typ>‹'a × 'b››

(* Already done in Complex_Inner_Product *)
(* instantiation prod :: (complex_inner, complex_inner) complex_inner begin
definition cinner_prod_def:
"cinner x y = cinner (fst x) (fst y) + cinner (snd x) (snd y)"
instance …
end
*)

lemma cinner_Pair [simp]: "cinner (a, b) (c, d) = cinner a c + cinner b d"
unfolding cinner_prod_def by simp

lemma cinner_Pair_0: "cinner x (0, b) = cinner (snd x) b" "cinner x (a, 0) = cinner (fst x) a"
by (cases x, simp)+

instantiation prod :: (ceuclidean_space, ceuclidean_space) ceuclidean_space
begin

definition
"CBasis = (λu. (u, 0)) ` CBasis ∪ (λv. (0, v)) ` CBasis"

lemma sum_CBasis_prod_eq:
fixes f::"('a*'b)⇒('a*'b)"
shows "sum f CBasis = sum (λi. f (i, 0)) CBasis + sum (λi. f (0, i)) CBasis"
proof -
have "inj_on (λu. (u::'a, 0::'b)) CBasis" "inj_on (λu. (0::'a, u::'b)) CBasis"
by (auto intro!: inj_onI Pair_inject)
thus ?thesis
unfolding CBasis_prod_def
by (subst sum.union_disjoint) (auto simp: CBasis_prod_def sum.reindex)
qed

instance proof
show "(CBasis :: ('a × 'b) set) ≠ {}"
unfolding CBasis_prod_def by simp
next
show "finite (CBasis :: ('a × 'b) set)"
unfolding CBasis_prod_def by simp
next
fix u v :: "'a × 'b"
assume "u ∈ CBasis" and "v ∈ CBasis"
thus "cinner u v = (if u = v then 1 else 0)"
unfolding CBasis_prod_def cinner_prod_def
by (auto simp add: cinner_CBasis split: if_split_asm)
next
fix x :: "'a × 'b"
show "(∀u∈CBasis. cinner x u = 0) ⟷ x = 0"
unfolding CBasis_prod_def ball_Un ball_simps
by (simp add: cinner_prod_def prod_eq_iff ceuclidean_all_zero_iff)
qed

lemma CDIM_prod[simp]: "CDIM('a × 'b) = CDIM('a) + CDIM('b)"
unfolding CBasis_prod_def
by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="(+)"] inj_onI)

end

subsection ‹Locale instances›

lemma finite_dimensional_vector_space_euclidean:
"finite_dimensional_vector_space (*⇩C) CBasis"
proof unfold_locales
show "finite (CBasis::'a set)" by (metis finite_CBasis)
show "complex_vector.independent (CBasis::'a set)"
unfolding complex_vector.dependent_def cdependent_raw_def[symmetric]
apply (subst complex_vector.span_finite)
apply simp
apply clarify
apply (drule_tac f="cinner a" in arg_cong)
by (simp add: cinner_CBasis cinner_sum_right eq_commute)
show "module.span (*⇩C) CBasis = UNIV"
unfolding complex_vector.span_finite [OF finite_CBasis] cspan_raw_def[symmetric]
by (auto intro!: ceuclidean_representation[symmetric])
qed

interpretation ceucl: finite_dimensional_vector_space "scaleC :: complex => 'a => 'a::ceuclidean_space" "CBasis"
rewrites "module.dependent (*⇩C) = cdependent"
and "module.representation (*⇩C) = crepresentation"
and "module.subspace (*⇩C) = csubspace"
and "module.span (*⇩C) = cspan"
and "vector_space.extend_basis (*⇩C) = cextend_basis"
and "vector_space.dim (*⇩C) = cdim"
and "Vector_Spaces.linear (*⇩C) (*⇩C) = clinear"
and "Vector_Spaces.linear (*) (*⇩C) = clinear"
and "finite_dimensional_vector_space.dimension CBasis = CDIM('a)"
(* and "dimension = CDIM('a)" *) (* This line leads to a type error. Not sure why *)
by (auto simp add: cdependent_raw_def crepresentation_raw_def
csubspace_raw_def cspan_raw_def cextend_basis_raw_def cdim_raw_def clinear_def
complex_scaleC_def[abs_def]
finite_dimensional_vector_space.dimension_def
intro!: finite_dimensional_vector_space.dimension_def
finite_dimensional_vector_space_euclidean)

interpretation ceucl: finite_dimensional_vector_space_pair_1
"scaleC::complex⇒'a::ceuclidean_space⇒'a" CBasis
"scaleC::complex⇒'b::complex_vector ⇒ 'b"
by unfold_locales

interpretation ceucl?: finite_dimensional_vector_space_prod scaleC scaleC CBasis CBasis
rewrites "Basis_pair = CBasis"
and "module_prod.scale (*⇩C) (*⇩C) = (scaleC::_⇒_⇒('a × 'b))"
proof -
show "finite_dimensional_vector_space_prod (*⇩C) (*⇩C) CBasis CBasis"
by unfold_locales
interpret finite_dimensional_vector_space_prod "(*⇩C)" "(*⇩C)" "CBasis::'a set" "CBasis::'b set"
by fact
show "Basis_pair = CBasis"
unfolding Basis_pair_def CBasis_prod_def by auto
show "module_prod.scale (*⇩C) (*⇩C) = scaleC"
by (fact module_prod_scale_eq_scaleC)
qed

end
```