# Theory Euclidean_Space

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

section ‹Finite-Dimensional Inner Product Spaces›

theory Euclidean_Space
imports
L2_Norm
Inner_Product
Product_Vector
begin

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

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"
using assms by force

subsection ‹Type class of Euclidean spaces›

class euclidean_space = real_inner +
fixes Basis :: "'a set"
assumes nonempty_Basis [simp]: "Basis ≠ {}"
assumes finite_Basis [simp]: "finite Basis"
assumes inner_Basis:
"⟦u ∈ Basis; v ∈ Basis⟧ ⟹ inner u v = (if u = v then 1 else 0)"
assumes euclidean_all_zero_iff:
"(∀u∈Basis. inner x u = 0) ⟷ (x = 0)"

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

lemma (in euclidean_space) norm_Basis[simp]: "u ∈ Basis ⟹ norm u = 1"
unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)

lemma (in euclidean_space) inner_same_Basis[simp]: "u ∈ Basis ⟹ inner u u = 1"

lemma (in euclidean_space) inner_not_same_Basis: "u ∈ Basis ⟹ v ∈ Basis ⟹ u ≠ v ⟹ inner u v = 0"

lemma (in euclidean_space) sgn_Basis: "u ∈ Basis ⟹ sgn u = u"
unfolding sgn_div_norm by (simp add: scaleR_one)

lemma inner_sum_Basis[simp]: "i ∈ Basis ⟹ inner (∑Basis) i = 1"
by (simp add: inner_sum_left sum.If_cases inner_Basis)

lemma (in euclidean_space) Basis_zero [simp]: "0 ∉ Basis"
proof
assume "0 ∈ Basis" thus "False"
using inner_Basis [of 0 0] by simp
qed

lemma (in euclidean_space) nonzero_Basis: "u ∈ Basis ⟹ u ≠ 0"
by clarsimp

lemma (in euclidean_space) SOME_Basis: "(SOME i. i ∈ Basis) ∈ Basis"
by (metis ex_in_conv nonempty_Basis someI_ex)

lemma norm_some_Basis [simp]: "norm (SOME i. i ∈ Basis) = 1"

lemma (in euclidean_space) inner_sum_left_Basis[simp]:
"b ∈ Basis ⟹ inner (∑i∈Basis. f i *⇩R i) b = f b"

lemma (in euclidean_space) euclidean_eqI:
assumes b: "⋀b. b ∈ Basis ⟹ inner x b = inner y b" shows "x = y"
proof -
from b have "∀b∈Basis. inner (x - y) b = 0"
then show "x = y"
qed

lemma (in euclidean_space) euclidean_eq_iff:
"x = y ⟷ (∀b∈Basis. inner x b = inner y b)"
by (auto intro: euclidean_eqI)

lemma (in euclidean_space) euclidean_representation_sum:
"(∑i∈Basis. f i *⇩R i) = b ⟷ (∀i∈Basis. f i = inner b i)"
by (subst euclidean_eq_iff) simp

lemma (in euclidean_space) euclidean_representation_sum':
"b = (∑i∈Basis. f i *⇩R i) ⟷ (∀i∈Basis. f i = inner b i)"

lemma (in euclidean_space) euclidean_representation: "(∑b∈Basis. inner x b *⇩R b) = x"
unfolding euclidean_representation_sum by simp

lemma (in euclidean_space) euclidean_inner: "inner x y = (∑b∈Basis. (inner x b) * (inner y b))"
by (subst (1 2) euclidean_representation [symmetric])

lemma (in euclidean_space) choice_Basis_iff:
fixes P :: "'a ⇒ real ⇒ bool"
shows "(∀i∈Basis. ∃x. P i x) ⟷ (∃x. ∀i∈Basis. P i (inner x i))"
unfolding bchoice_iff
proof safe
fix f assume "∀i∈Basis. P i (f i)"
then show "∃x. ∀i∈Basis. P i (inner x i)"
by (auto intro!: exI[of _ "∑i∈Basis. f i *⇩R i"])
qed auto

lemma (in euclidean_space) bchoice_Basis_iff:
fixes P :: "'a ⇒ real ⇒ bool"
shows "(∀i∈Basis. ∃x∈A. P i x) ⟷ (∃x. ∀i∈Basis. inner x i ∈ A ∧ P i (inner x i))"

lemma (in euclidean_space) euclidean_representation_sum_fun:
"(λx. ∑b∈Basis. inner (f x) b *⇩R b) = f"
by (rule ext) (simp add: euclidean_representation_sum)

lemma euclidean_isCont:
assumes "⋀b. b ∈ Basis ⟹ isCont (λx. (inner (f x) b) *⇩R b) x"
shows "isCont f x"
apply (subst euclidean_representation_sum_fun [symmetric])
apply (rule isCont_sum)
apply (blast intro: assms)
done

lemma DIM_positive [simp]: "0 < DIM('a::euclidean_space)"

lemma DIM_ge_Suc0 [simp]: "Suc 0 ≤ card Basis"
by (meson DIM_positive Suc_leI)

lemma sum_inner_Basis_scaleR [simp]:
fixes f :: "'a::euclidean_space ⇒ 'b::real_vector"
assumes "b ∈ Basis" shows "(∑i∈Basis. (inner i b) *⇩R f i) = f b"

lemma sum_inner_Basis_eq [simp]:
assumes "b ∈ Basis" shows "(∑i∈Basis. (inner i b) * f i) = f b"

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

lemma norm_le_componentwise:
"(⋀b. b ∈ Basis ⟹ abs(inner x b) ≤ abs(inner y b)) ⟹ norm x ≤ norm y"
by (auto simp: norm_le euclidean_inner [of x x] euclidean_inner [of y y] abs_le_square_iff power2_eq_square intro!: sum_mono)

lemma Basis_le_norm: "b ∈ Basis ⟹ ¦inner x b¦ ≤ norm x"
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp

lemma norm_bound_Basis_le: "b ∈ Basis ⟹ norm x ≤ e ⟹ ¦inner x b¦ ≤ e"
by (metis Basis_le_norm order_trans)

lemma norm_bound_Basis_lt: "b ∈ Basis ⟹ norm x < e ⟹ ¦inner x b¦ < e"
by (metis Basis_le_norm le_less_trans)

lemma norm_le_l1: "norm x ≤ (∑b∈Basis. ¦inner x b¦)"
apply (subst euclidean_representation[of x, symmetric])
apply (rule order_trans[OF norm_sum])
apply (auto intro!: sum_mono)
done

lemma sum_norm_allsubsets_bound:
fixes f :: "'a ⇒ 'n::euclidean_space"
assumes fP: "finite P"
and fPs: "⋀Q. Q ⊆ P ⟹ norm (sum f Q) ≤ e"
shows "(∑x∈P. norm (f x)) ≤ 2 * real DIM('n) * e"
proof -
have "(∑x∈P. norm (f x)) ≤ (∑x∈P. ∑b∈Basis. ¦inner (f x) b¦)"
by (rule sum_mono) (rule norm_le_l1)
also have "(∑x∈P. ∑b∈Basis. ¦inner (f x) b¦) = (∑b∈Basis. ∑x∈P. ¦inner (f x) b¦)"
by (rule sum.swap)
also have "… ≤ of_nat (card (Basis :: 'n set)) * (2 * e)"
proof (rule sum_bounded_above)
fix i :: 'n
assume i: "i ∈ Basis"
have "norm (∑x∈P. ¦inner (f x) i¦) ≤
norm (inner (∑x∈P ∩ - {x. inner (f x) i < 0}. f x) i) + norm (inner (∑x∈P ∩ {x. inner (f x) i < 0}. f x) i)"
by (simp add: abs_real_def sum.If_cases[OF fP] sum_negf norm_triangle_ineq4 inner_sum_left
del: real_norm_def)
also have "… ≤ e + e"
unfolding real_norm_def
by (intro add_mono norm_bound_Basis_le i fPs) auto
finally show "(∑x∈P. ¦inner (f x) i¦) ≤ 2*e" by simp
qed
also have "… = 2 * real DIM('n) * e" by simp
finally show ?thesis .
qed

subsection✐‹tag unimportant› ‹Subclass relationships›

instance euclidean_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 ∈ Basis)"
have [simp]: "(SOME b. b ∈ Basis) ∈ Basis"
by (rule someI_ex) (auto simp: ex_in_conv)
from ‹0 < e› have "y ≠ x"
unfolding y_def by (auto intro!: nonzero_Basis)
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>‹real››

instantiation real :: euclidean_space
begin

definition
[simp]: "Basis = {1::real}"

instance
by standard auto

end

lemma DIM_real[simp]: "DIM(real) = 1"
by simp

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

instantiation complex :: euclidean_space
begin

definition Basis_complex_def: "Basis = {1, 𝗂}"

instance
by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)

end

lemma DIM_complex[simp]: "DIM(complex) = 2"
unfolding Basis_complex_def by simp

lemma complex_Basis_1 [iff]: "(1::complex) ∈ Basis"

lemma complex_Basis_i [iff]: "𝗂 ∈ Basis"

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

instantiation prod :: (real_inner, real_inner) real_inner
begin

definition inner_prod_def:
"inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"

lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
unfolding inner_prod_def by simp

instance
proof
fix r :: real
fix x y z :: "'a::real_inner × 'b::real_inner"
show "inner x y = inner y x"
unfolding inner_prod_def
show "inner (x + y) z = inner x z + inner y z"
unfolding inner_prod_def
show "inner (scaleR r x) y = r * inner x y"
unfolding inner_prod_def
show "0 ≤ inner x x"
unfolding inner_prod_def
show "inner x x = 0 ⟷ x = 0"
unfolding inner_prod_def prod_eq_iff
show "norm x = sqrt (inner x x)"
unfolding norm_prod_def inner_prod_def
qed

end

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

instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
begin

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

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

instance proof
show "(Basis :: ('a × 'b) set) ≠ {}"
unfolding Basis_prod_def by simp
next
show "finite (Basis :: ('a × 'b) set)"
unfolding Basis_prod_def by simp
next
fix u v :: "'a × 'b"
assume "u ∈ Basis" and "v ∈ Basis"
thus "inner u v = (if u = v then 1 else 0)"
unfolding Basis_prod_def inner_prod_def
by (auto simp add: inner_Basis split: if_split_asm)
next
fix x :: "'a × 'b"
show "(∀u∈Basis. inner x u = 0) ⟷ x = 0"
unfolding Basis_prod_def ball_Un ball_simps
by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
qed

lemma DIM_prod[simp]: "DIM('a × 'b) = DIM('a) + DIM('b)"
unfolding Basis_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 (*⇩R) Basis"
proof unfold_locales
show "finite (Basis::'a set)" by (metis finite_Basis)
show "real_vector.independent (Basis::'a set)"
unfolding dependent_def dependent_raw_def[symmetric]
apply (subst span_finite)
apply simp
apply clarify
apply (drule_tac f="inner a" in arg_cong)
apply (simp add: inner_Basis inner_sum_right eq_commute)
done
show "module.span (*⇩R) Basis = UNIV"
unfolding span_finite [OF finite_Basis] span_raw_def[symmetric]
by (auto intro!: euclidean_representation[symmetric])
qed

interpretation eucl?: finite_dimensional_vector_space "scaleR :: real => 'a => 'a::euclidean_space" "Basis"
rewrites "module.dependent (*⇩R) = dependent"
and "module.representation (*⇩R) = representation"
and "module.subspace (*⇩R) = subspace"
and "module.span (*⇩R) = span"
and "vector_space.extend_basis (*⇩R) = extend_basis"
and "vector_space.dim (*⇩R) = dim"
and "Vector_Spaces.linear (*⇩R) (*⇩R) = linear"
and "Vector_Spaces.linear (*) (*⇩R) = linear"
and "finite_dimensional_vector_space.dimension Basis = DIM('a)"
and "dimension = DIM('a)"
by (auto simp add: dependent_raw_def representation_raw_def
subspace_raw_def span_raw_def extend_basis_raw_def dim_raw_def linear_def
real_scaleR_def[abs_def]
finite_dimensional_vector_space.dimension_def
intro!: finite_dimensional_vector_space.dimension_def
finite_dimensional_vector_space_euclidean)

interpretation eucl?: finite_dimensional_vector_space_pair_1
"scaleR::real⇒'a::euclidean_space⇒'a" Basis
"scaleR::real⇒'b::real_vector ⇒ 'b"
by unfold_locales

interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
rewrites "Basis_pair = Basis"
and "module_prod.scale (*⇩R) (*⇩R) = (scaleR::_⇒_⇒('a × 'b))"
proof -
show "finite_dimensional_vector_space_prod (*⇩R) (*⇩R) Basis Basis"
by unfold_locales
interpret finite_dimensional_vector_space_prod "(*⇩R)" "(*⇩R)" "Basis::'a set" "Basis::'b set"
by fact
show "Basis_pair = Basis"
unfolding Basis_pair_def Basis_prod_def by auto
show "module_prod.scale (*⇩R) (*⇩R) = scaleR"
by (fact module_prod_scale_eq_scaleR)
qed

end
```