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

section ‹Finite-Dimensional Inner Product Spaces›

theory Euclidean_Space
imports
  L2_Norm
  "~~/src/HOL/Library/Inner_Product"
  "~~/src/HOL/Library/Product_Vector"
begin

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"
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 (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 comm_monoid_add_class.setsum.If_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)
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_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_setsum':
  "b = (∑i∈Basis. f i *R i) ⟷ (∀i∈Basis. f i = inner b i)"
  by (auto simp add: euclidean_representation_setsum[symmetric])

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 (in euclidean_space) euclidean_representation_setsum_fun: 
    "(λx. ∑b∈Basis. inner (f x) b *R b) = f"
  by (rule ext) (simp add: euclidean_representation_setsum)

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

lemma DIM_positive: "0 < DIM('a::euclidean_space)"
  by (simp add: card_gt_0_iff)

subsection ‹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
    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
  qed
qed

subsection ‹Class instances›

subsubsection ‹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 ‹Type @{typ complex}›

instantiation complex :: euclidean_space
begin

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

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

subsubsection ‹Type @{typ "'a × 'b"}›

instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
begin

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

lemma setsum_Basis_prod_eq:
  fixes f::"('a*'b)⇒('a*'b)"
  shows "setsum f Basis = setsum (λi. f (i, 0)) Basis + setsum (λ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 setsum.union_disjoint) (auto simp: Basis_prod_def setsum.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="op +"] inj_onI)

end

end