Quelle  Euclidean_Space.thy   Sprache: Isabelle

(*  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"  (‹(‹indent=1 notation=‹mixfix type dimension››DIM/(1'(_')))›)
syntax_consts "_type_dimension" ⇌ card
translations "DIM('a)" ⇀ "CONST card (CONST Basis :: 'a set)"
typed_print_translation ‹
  [(🍋‹card›,
    fn ctxt => fn _ => fn [Const (🍋‹Basis›, Type (🍋‹set›, [T]))] =>
      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"
  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 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"
  using local.inner_same_Basis by fastforce

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"
  by (simp add: SOME_Basis)

lemma (in euclidean_space) inner_sum_left_Basis[simp]:
    "b \ Basis \ inner (\i\Basis. f i *\<^sub>R i) b = f b"
  by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.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_sum:
  "(\i\Basis. f i *\<^sub>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 *\<^sub>R i) \ (\i\Basis. f i = inner b i)"
  by (auto simp add: euclidean_representation_sum[symmetric])

lemma (in euclidean_space) euclidean_representation: "(\b\Basis. inner x b *\<^sub>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])
    (simp add: inner_sum_right inner_Basis ac_simps)

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 *\<^sub>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))"
by (simp add: choice_Basis_iff Bex_def)

lemma (in euclidean_space) euclidean_representation_sum_fun:
    "(\x. \b\Basis. inner (f x) b *\<^sub>R b) = f"
  by (force simp: euclidean_representation_sum)

lemma euclidean_isCont:
  assumes "\b. b \ Basis \ isCont (\x. (inner (f x) b) *\<^sub>R b) x"
  shows "isCont f x"
proof -
  have "isCont (\x. \b\Basis. inner (f x) b *\<^sub>R b) x"
    by (simp add: assms)
  then show ?thesis
    by (simp add: euclidean_representation)
qed

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

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) *\<^sub>R f i) = f b"
  by (simp add: comm_monoid_add_class.sum.remove [OF finite_Basis assms]
         assms inner_not_same_Basis comm_monoid_add_class.sum.neutral)

lemma sum_inner_Basis_eq [simp]:
  assumes "b \ Basis" shows "(\i\Basis. (inner i b) * f i) = f b"
  by (simp add: comm_monoid_add_class.sum.remove [OF finite_Basis assms]
         assms inner_not_same_Basis comm_monoid_add_class.sum.neutral)

lemma sum_if_inner [simp]:
  assumes "i \ Basis" "j \ Basis"
    shows "inner (\k\Basis. if k = i then f i *\<^sub>R i else g k *\<^sub>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 *\<^sub>R i else g k *\<^sub>R k) j) =
        (∑k∈Basis. if k = j then g k else 0)"
    using False assms
    by (intro sum.cong) (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\)"
  by (metis (no_types, lifting) order.refl euclidean_representation mult.right_neutral
      norm_Basis norm_scaleR sum_norm_le)

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 🍋‹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 🍋‹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"
  by (simp add: Basis_complex_def)

lemma complex_Basis_i [iff]: "\ \ Basis"
  by (simp add: Basis_complex_def)

subsubsection🍋‹tag unimportant› ‹Type 🍋‹'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
    by (simp add: inner_commute)
  show "inner (x + y) z = inner x z + inner y z"
    unfolding inner_prod_def
    by (simp add: inner_add_left)
  show "inner (scaleR r x) y = r * inner x y"
    unfolding inner_prod_def
    by (simp add: distrib_left)
  show "0 \ inner x x"
    unfolding inner_prod_def
    by (intro add_nonneg_nonneg inner_ge_zero)
  show "inner x x = 0 \ x = 0"
    unfolding inner_prod_def prod_eq_iff
    by (simp add: add_nonneg_eq_0_iff)
  show "norm x = sqrt (inner x x)"
    unfolding norm_prod_def inner_prod_def
    by (simp add: power2_norm_eq_inner)
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 (*\<^sub>R) Basis"
proof unfold_locales
  show "finite (Basis::'a set)" by (metis finite_Basis)
  have "\a::'a. \u. \a \ Basis; a = (\v\Basis - {a}. u v *\<^sub>R v)\ \ False"
    apply (drule_tac f="inner a" in arg_cong)
    apply (simp add: inner_Basis inner_sum_right eq_commute)
    done
  then
  show "real_vector.independent (Basis::'a set)"
    unfolding dependent_def dependent_raw_def[symmetric]
    by (subst span_finite) auto
  show "module.span (*\<^sub>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 (*\<^sub>R) = dependent"
    and "module.representation (*\<^sub>R) = representation"
    and "module.subspace (*\<^sub>R) = subspace"
    and "module.span (*\<^sub>R) = span"
    and "vector_space.extend_basis (*\<^sub>R) = extend_basis"
    and "vector_space.dim (*\<^sub>R) = dim"
    and "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
    and "Vector_Spaces.linear (*) (*\<^sub>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)

declare card_set [code] 🍋‹Restore code equation after global interpretation›

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 (*\<^sub>R) (*\<^sub>R) = (scaleR::_\_\('a \ 'b))"
proof -
  show "finite_dimensional_vector_space_prod (*\<^sub>R) (*\<^sub>R) Basis Basis"
    by unfold_locales
  interpret finite_dimensional_vector_space_prod "(*\<^sub>R)" "(*\<^sub>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 (*\<^sub>R) (*\<^sub>R) = scaleR"
    by (fact module_prod_scale_eq_scaleR)
qed

end