Theory Euclidean_Space

theory Euclidean_Space
imports L2_Norm Product_Vector
(*  Title:      HOL/Multivariate_Analysis/Euclidean_Space.thy
Author: Johannes Hölzl, TU München
Author: Brian Huffman, Portland State University

header {* Finite-Dimensional Inner Product Spaces *}

theory Euclidean_Space

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

abbreviation dimension :: "('a::euclidean_space) itself => nat" where
"dimension TYPE('a) ≡ card (Basis :: 'a set)"

syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")

translations "DIM('t)" == "CONST dimension (TYPE('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"
by (simp add: inner_Basis)

lemma (in euclidean_space) inner_not_same_Basis: "u ∈ Basis ==> v ∈ Basis ==> u ≠ v ==> inner u v = 0"
by (simp add: inner_Basis)

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

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

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 (in euclidean_space) inner_setsum_left_Basis[simp]:
"b ∈ Basis ==> inner (∑i∈Basis. f i *R i) b = f b"
by (simp add: inner_setsum_left inner_Basis if_distrib setsum_cases)

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"
by (simp add: inner_diff_left)
then show "x = y"
by (simp add: euclidean_all_zero_iff)

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_setsum:
"(∑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: "(∑b∈Basis. inner x b *R b) = x"
unfolding euclidean_representation_setsum by simp

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 DIM_positive: "0 < DIM('a::euclidean_space)"
by (simp add: card_gt_0_iff)

subsection {* Subclass relationships *}

instance euclidean_space perfect_space
fix x :: 'a show "¬ open {x}"
assume "open {x}"
then obtain e where "0 < e" and e: "∀y. dist y x < e --> y = x"
unfolding open_dist by fast
def 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

subsection {* Class instances *}

subsubsection {* Type @{typ real} *}

instantiation real :: euclidean_space

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

by default auto


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

subsubsection {* Type @{typ complex} *}

instantiation complex :: euclidean_space

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

by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)


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

subsubsection {* Type @{typ "'a × 'b"} *}

instantiation prod :: (euclidean_space, euclidean_space) euclidean_space

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

instance proof
show "(Basis :: ('a × 'b) set) ≠ {}"
unfolding Basis_prod_def by simp
show "finite (Basis :: ('a × 'b) set)"
unfolding Basis_prod_def by simp
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: split_if_asm)
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)

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="op +"] inj_onI)