src/HOL/Multivariate_Analysis/Euclidean_Space.thy
author huffman
Mon, 05 Jul 2010 09:12:35 -0700
changeset 37731 8c6bfe10a4ae
parent 37664 2946b8f057df
child 37737 243ea7885e05
permissions -rw-r--r--
section -> subsection
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35253
68dd8b51c6b8 tuned headers;
wenzelm
parents: 35172
diff changeset
     1
(*  Title:      Library/Multivariate_Analysis/Euclidean_Space.thy
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     2
    Author:     Amine Chaieb, University of Cambridge
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     3
*)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     4
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     5
header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     6
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     7
theory Euclidean_Space
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     8
imports
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
     9
  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
37647
a5400b94d2dd minimize dependencies on Numeral_Type
huffman
parents: 37646
diff changeset
    10
  Infinite_Set
36623
d26348b667f2 Moved Convex theory to library.
hoelzl
parents: 36596
diff changeset
    11
  Inner_Product L2_Norm Convex
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    12
uses "positivstellensatz.ML" ("normarith.ML")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    13
begin
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    14
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
    15
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
    16
  by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    17
37606
b47dd044a1f1 inner_simps is not enough, need also local facts
haftmann
parents: 37489
diff changeset
    18
notation inner (infix "\<bullet>" 70)
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
    19
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    20
subsection {* A connectedness or intermediate value lemma with several applications. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    21
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    22
lemma connected_real_lemma:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    23
  fixes f :: "real \<Rightarrow> 'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    24
  assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    25
  and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    26
  and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    27
  and e2: "\<forall>y \<in> e2. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    28
  and e12: "~(\<exists>x \<ge> a. x <= b \<and> f x \<in> e1 \<and> f x \<in> e2)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    29
  shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    30
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    31
  let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    32
  have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    33
  have Sub: "\<exists>y. isUb UNIV ?S y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    34
    apply (rule exI[where x= b])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    35
    using ab fb e12 by (auto simp add: isUb_def setle_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    36
  from reals_complete[OF Se Sub] obtain l where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    37
    l: "isLub UNIV ?S l"by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    38
  have alb: "a \<le> l" "l \<le> b" using l ab fa fb e12
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    39
    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    40
    by (metis linorder_linear)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    41
  have ale1: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> e1" using l
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    42
    apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    43
    by (metis linorder_linear not_le)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    44
    have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    45
    have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    46
    have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    47
    {assume le2: "f l \<in> e2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    48
      from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    49
      hence lap: "l - a > 0" using alb by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    50
      from e2[rule_format, OF le2] obtain e where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    51
        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    52
      from dst[OF alb e(1)] obtain d where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    53
        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    54
      have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" using lap d(1)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    55
        apply ferrack by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    56
      then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    57
      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    58
      from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    59
      moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    60
      have "f (l - d') \<in> e1" using ale1[rule_format, of "l -d'"] d' by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    61
      ultimately have False using e12 alb d' by auto}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    62
    moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    63
    {assume le1: "f l \<in> e1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    64
    from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    65
      hence blp: "b - l > 0" using alb by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    66
      from e1[rule_format, OF le1] obtain e where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    67
        e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    68
      from dst[OF alb e(1)] obtain d where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    69
        d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    70
      have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    71
      then obtain d' where d': "d' > 0" "d' < d" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    72
      from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    73
      hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    74
      with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    75
      with l d' have False
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    76
        by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    77
    ultimately show ?thesis using alb by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    78
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    79
36431
340755027840 move definitions and theorems for type real^1 to separate theory file
huffman
parents: 36365
diff changeset
    80
text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    81
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    82
lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    83
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    84
  have "(x + 1/2)^2 + 3/4 > 0" using zero_le_power2[of "x+1/2"] by arith
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
    85
  thus ?thesis by (simp add: field_simps power2_eq_square)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    86
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    87
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    88
lemma square_continuous: "0 < (e::real) ==> \<exists>d. 0 < d \<and> (\<forall>y. abs(y - x) < d \<longrightarrow> abs(y * y - x * x) < e)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    89
  using isCont_power[OF isCont_ident, of 2, unfolded isCont_def LIM_eq, rule_format, of e x] apply (auto simp add: power2_eq_square)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    90
  apply (rule_tac x="s" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    91
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    92
  apply (erule_tac x=y in allE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    93
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    94
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    95
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    96
lemma real_le_lsqrt: "0 <= x \<Longrightarrow> 0 <= y \<Longrightarrow> x <= y^2 ==> sqrt x <= y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    97
  using real_sqrt_le_iff[of x "y^2"] by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    98
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
    99
lemma real_le_rsqrt: "x^2 \<le> y \<Longrightarrow> x \<le> sqrt y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   100
  using real_sqrt_le_mono[of "x^2" y] by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   101
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   102
lemma real_less_rsqrt: "x^2 < y \<Longrightarrow> x < sqrt y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   103
  using real_sqrt_less_mono[of "x^2" y] by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   104
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   105
lemma sqrt_even_pow2: assumes n: "even n"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   106
  shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   107
proof-
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   108
  from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   109
  from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   110
    by (simp only: power_mult[symmetric] mult_commute)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   111
  then show ?thesis  using m by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   112
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   113
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   114
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   115
  apply (cases "x = 0", simp_all)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   116
  using sqrt_divide_self_eq[of x]
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   117
  apply (simp add: inverse_eq_divide field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   118
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   119
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   120
text{* Hence derive more interesting properties of the norm. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   121
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   122
(* FIXME: same as norm_scaleR
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   123
lemma norm_mul[simp]: "norm(a *\<^sub>R x) = abs(a) * norm x"
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   124
  by (simp add: norm_vector_def setL2_right_distrib abs_mult)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   125
*)
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   126
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   127
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   128
  by (simp add: setL2_def power2_eq_square)
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   129
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   130
lemma norm_cauchy_schwarz:
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   131
  shows "inner x y <= norm x * norm y"
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   132
  using Cauchy_Schwarz_ineq2[of x y] by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   133
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   134
lemma norm_cauchy_schwarz_abs:
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   135
  shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   136
  by (rule Cauchy_Schwarz_ineq2)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   137
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   138
lemma norm_triangle_sub:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   139
  fixes x y :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   140
  shows "norm x \<le> norm y  + norm (x - y)"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   141
  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   142
34291
4e896680897e finite annotation on cartesian product is now implicit.
hoelzl
parents: 34289
diff changeset
   143
lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   144
  by (rule abs_norm_cancel)
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   145
lemma real_abs_sub_norm: "\<bar>norm x - norm y\<bar> <= norm(x - y)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   146
  by (rule norm_triangle_ineq3)
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   147
lemma norm_le: "norm(x) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   148
  by (simp add: norm_eq_sqrt_inner) 
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   149
lemma norm_lt: "norm(x) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   150
  by (simp add: norm_eq_sqrt_inner)
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   151
lemma norm_eq: "norm(x) = norm (y) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   152
  apply(subst order_eq_iff) unfolding norm_le by auto
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   153
lemma norm_eq_1: "norm(x) = 1 \<longleftrightarrow> x \<bullet> x = 1"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   154
  unfolding norm_eq_sqrt_inner by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   155
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   156
text{* Squaring equations and inequalities involving norms.  *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   157
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   158
lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   159
  by (simp add: norm_eq_sqrt_inner)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   160
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   161
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   162
  by (auto simp add: norm_eq_sqrt_inner)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   163
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   164
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   165
proof
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   166
  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   167
  then have "\<bar>x\<bar>\<twosuperior> \<le> \<bar>y\<bar>\<twosuperior>" by (rule power_mono, simp)
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   168
  then show "x\<twosuperior> \<le> y\<twosuperior>" by simp
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   169
next
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   170
  assume "x\<twosuperior> \<le> y\<twosuperior>"
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   171
  then have "sqrt (x\<twosuperior>) \<le> sqrt (y\<twosuperior>)" by (rule real_sqrt_le_mono)
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   172
  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   173
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   174
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   175
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   176
  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   177
  using norm_ge_zero[of x]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   178
  apply arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   179
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   180
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   181
lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   182
  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   183
  using norm_ge_zero[of x]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   184
  apply arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   185
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   186
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   187
lemma norm_lt_square: "norm(x) < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a^2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   188
  by (metis not_le norm_ge_square)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   189
lemma norm_gt_square: "norm(x) > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a^2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   190
  by (metis norm_le_square not_less)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   191
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   192
text{* Dot product in terms of the norm rather than conversely. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   193
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   194
lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left 
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   195
inner.scaleR_left inner.scaleR_right
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   196
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   197
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   198
  unfolding power2_norm_eq_inner inner_simps inner_commute by auto 
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   199
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   200
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   201
  unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   202
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   203
text{* Equality of vectors in terms of @{term "op \<bullet>"} products.    *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   204
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   205
lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   206
proof
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   207
  assume ?lhs then show ?rhs by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   208
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   209
  assume ?rhs
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   210
  then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   211
  hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   212
  then have "(x - y) \<bullet> (x - y) = 0" by (simp add: field_simps inner_simps inner_commute)
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   213
  then show "x = y" by (simp)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   214
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   215
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   216
subsection{* General linear decision procedure for normed spaces. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   217
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   218
lemma norm_cmul_rule_thm:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   219
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   220
  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   221
  unfolding norm_scaleR
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   222
  apply (erule mult_mono1)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   223
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   224
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   225
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   226
  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   227
lemma norm_add_rule_thm:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   228
  fixes x1 x2 :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   229
  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   230
  by (rule order_trans [OF norm_triangle_ineq add_mono])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   231
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34964
diff changeset
   232
lemma ge_iff_diff_ge_0: "(a::'a::linordered_ring) \<ge> b == a - b \<ge> 0"
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   233
  by (simp add: field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   234
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   235
lemma pth_1:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   236
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   237
  shows "x == scaleR 1 x" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   238
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   239
lemma pth_2:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   240
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   241
  shows "x - y == x + -y" by (atomize (full)) simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   242
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   243
lemma pth_3:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   244
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   245
  shows "- x == scaleR (-1) x" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   246
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   247
lemma pth_4:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   248
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   249
  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   250
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   251
lemma pth_5:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   252
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   253
  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   254
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   255
lemma pth_6:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   256
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   257
  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   258
  by (simp add: scaleR_right_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   259
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   260
lemma pth_7:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   261
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   262
  shows "0 + x == x" and "x + 0 == x" by simp_all
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   263
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   264
lemma pth_8:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   265
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   266
  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   267
  by (simp add: scaleR_left_distrib)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   268
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   269
lemma pth_9:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   270
  fixes x :: "'a::real_normed_vector" shows
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   271
  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   272
  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   273
  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   274
  by (simp_all add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   275
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   276
lemma pth_a:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   277
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   278
  shows "scaleR 0 x + y == y" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   279
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   280
lemma pth_b:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   281
  fixes x :: "'a::real_normed_vector" shows
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   282
  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   283
  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   284
  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   285
  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   286
  by (simp_all add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   287
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   288
lemma pth_c:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   289
  fixes x :: "'a::real_normed_vector" shows
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   290
  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   291
  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   292
  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   293
  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   294
  by (simp_all add: algebra_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   295
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   296
lemma pth_d:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   297
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   298
  shows "x + 0 == x" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   299
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   300
lemma norm_imp_pos_and_ge:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   301
  fixes x :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   302
  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   303
  by atomize auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   304
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   305
lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   306
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   307
lemma norm_pths:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   308
  fixes x :: "'a::real_normed_vector" shows
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   309
  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   310
  "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   311
  using norm_ge_zero[of "x - y"] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   312
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   313
use "normarith.ML"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   314
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   315
method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   316
*} "Proves simple linear statements about vector norms"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   317
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   318
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   319
text{* Hence more metric properties. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   320
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   321
lemma dist_triangle_alt:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   322
  fixes x y z :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   323
  shows "dist y z <= dist x y + dist x z"
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   324
by (rule dist_triangle3)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   325
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   326
lemma dist_pos_lt:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   327
  fixes x y :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   328
  shows "x \<noteq> y ==> 0 < dist x y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   329
by (simp add: zero_less_dist_iff)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   330
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   331
lemma dist_nz:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   332
  fixes x y :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   333
  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   334
by (simp add: zero_less_dist_iff)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   335
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   336
lemma dist_triangle_le:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   337
  fixes x y z :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   338
  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   339
by (rule order_trans [OF dist_triangle2])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   340
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   341
lemma dist_triangle_lt:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   342
  fixes x y z :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   343
  shows "dist x z + dist y z < e ==> dist x y < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   344
by (rule le_less_trans [OF dist_triangle2])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   345
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   346
lemma dist_triangle_half_l:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   347
  fixes x1 x2 y :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   348
  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   349
by (rule dist_triangle_lt [where z=y], simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   350
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   351
lemma dist_triangle_half_r:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   352
  fixes x1 x2 y :: "'a::metric_space"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   353
  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   354
by (rule dist_triangle_half_l, simp_all add: dist_commute)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   355
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   356
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   357
lemma norm_triangle_half_r:
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   358
  shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
36587
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 36586
diff changeset
   359
  using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   360
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   361
lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" 
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   362
  shows "norm (x - x') < e"
36587
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 36586
diff changeset
   363
  using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]]
534418d8d494 remove redundant lemma vector_dist_norm
huffman
parents: 36586
diff changeset
   364
  unfolding dist_norm[THEN sym] .
35172
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   365
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   366
lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   367
  by (metis order_trans norm_triangle_ineq)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   368
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   369
lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   370
  by (metis basic_trans_rules(21) norm_triangle_ineq)
579dd5570f96 Added integration to Multivariate-Analysis (upto FTC)
himmelma
parents: 35150
diff changeset
   371
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   372
lemma dist_triangle_add:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   373
  fixes x y x' y' :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   374
  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   375
  by norm
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   376
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   377
lemma dist_triangle_add_half:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   378
  fixes x x' y y' :: "'a::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   379
  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   380
  by norm
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   381
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   382
lemma setsum_clauses:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   383
  shows "setsum f {} = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   384
  and "finite S \<Longrightarrow> setsum f (insert x S) =
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   385
                 (if x \<in> S then setsum f S else f x + setsum f S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   386
  by (auto simp add: insert_absorb)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   387
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   388
lemma setsum_norm:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   389
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   390
  assumes fS: "finite S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   391
  shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   392
proof(induct rule: finite_induct[OF fS])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   393
  case 1 thus ?case by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   394
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   395
  case (2 x S)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   396
  from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   397
  also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   398
    using "2.hyps" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   399
  finally  show ?case  using "2.hyps" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   400
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   401
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   402
lemma setsum_norm_le:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   403
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   404
  assumes fS: "finite S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   405
  and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   406
  shows "norm (setsum f S) \<le> setsum g S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   407
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   408
  from fg have "setsum (\<lambda>x. norm(f x)) S <= setsum g S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   409
    by - (rule setsum_mono, simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   410
  then show ?thesis using setsum_norm[OF fS, of f] fg
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   411
    by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   412
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   413
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   414
lemma setsum_norm_bound:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   415
  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   416
  assumes fS: "finite S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   417
  and K: "\<forall>x \<in> S. norm (f x) \<le> K"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   418
  shows "norm (setsum f S) \<le> of_nat (card S) * K"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   419
  using setsum_norm_le[OF fS K] setsum_constant[symmetric]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   420
  by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   421
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   422
lemma setsum_group:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   423
  assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   424
  shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   425
  apply (subst setsum_image_gen[OF fS, of g f])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   426
  apply (rule setsum_mono_zero_right[OF fT fST])
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   427
  by (auto intro: setsum_0')
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   428
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   429
lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   430
  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   431
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   432
lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   433
  apply(induct rule: finite_induct) by(auto simp add: inner_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   434
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   435
lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   436
proof
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   437
  assume "\<forall>x. x \<bullet> y = x \<bullet> z"
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   438
  hence "\<forall>x. x \<bullet> (y - z) = 0" by (simp add: inner_simps)
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   439
  hence "(y - z) \<bullet> (y - z) = 0" ..
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   440
  thus "y = z" by simp
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   441
qed simp
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   442
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   443
lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = y"
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   444
proof
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   445
  assume "\<forall>z. x \<bullet> z = y \<bullet> z"
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   446
  hence "\<forall>z. (x - y) \<bullet> z = 0" by (simp add: inner_simps)
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   447
  hence "(x - y) \<bullet> (x - y) = 0" ..
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   448
  thus "x = y" by simp
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   449
qed simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   450
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   451
subsection{* Orthogonality. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   452
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   453
context real_inner
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   454
begin
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   455
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   456
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   457
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   458
lemma orthogonal_clauses:
36588
8175a688c5e3 generalize orthogonal_clauses
huffman
parents: 36587
diff changeset
   459
  "orthogonal a 0"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   460
  "orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   461
  "orthogonal a x \<Longrightarrow> orthogonal a (-x)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   462
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   463
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   464
  "orthogonal 0 a"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   465
  "orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   466
  "orthogonal x a \<Longrightarrow> orthogonal (-x) a"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   467
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   468
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
37606
b47dd044a1f1 inner_simps is not enough, need also local facts
haftmann
parents: 37489
diff changeset
   469
  unfolding orthogonal_def inner_simps inner_add_left inner_add_right inner_diff_left inner_diff_right (*FIXME*) by auto
b47dd044a1f1 inner_simps is not enough, need also local facts
haftmann
parents: 37489
diff changeset
   470
 
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   471
end
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   472
36585
f2faab7b46e7 generalize some euclidean space lemmas
huffman
parents: 36581
diff changeset
   473
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
35542
8f97d8caabfd replaced \<bullet> with inner
himmelma
parents: 35541
diff changeset
   474
  by (simp add: orthogonal_def inner_commute)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   475
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   476
subsection{* Linear functions. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   477
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   478
definition
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   479
  linear :: "('a::real_vector \<Rightarrow> 'b::real_vector) \<Rightarrow> bool" where
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   480
  "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *\<^sub>R x) = c *\<^sub>R f x)"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   481
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   482
lemma linearI: assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
33714
eb2574ac4173 Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents: 33270
diff changeset
   483
  shows "linear f" using assms unfolding linear_def by auto
eb2574ac4173 Added new lemmas to Euclidean Space by Robert Himmelmann
hoelzl
parents: 33270
diff changeset
   484
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   485
lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. c *\<^sub>R f x)"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   486
  by (simp add: linear_def algebra_simps)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   487
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   488
lemma linear_compose_neg: "linear f ==> linear (\<lambda>x. -(f(x)))"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   489
  by (simp add: linear_def)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   490
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   491
lemma linear_compose_add: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   492
  by (simp add: linear_def algebra_simps)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   493
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   494
lemma linear_compose_sub: "linear f \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   495
  by (simp add: linear_def algebra_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   496
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   497
lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   498
  by (simp add: linear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   499
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   500
lemma linear_id: "linear id" by (simp add: linear_def id_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   501
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   502
lemma linear_zero: "linear (\<lambda>x. 0)" by (simp add: linear_def)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   503
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   504
lemma linear_compose_setsum:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   505
  assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a)"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   506
  shows "linear(\<lambda>x. setsum (\<lambda>a. f a x) S)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   507
  using lS
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   508
  apply (induct rule: finite_induct[OF fS])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   509
  by (auto simp add: linear_zero intro: linear_compose_add)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   510
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   511
lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   512
  unfolding linear_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   513
  apply clarsimp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   514
  apply (erule allE[where x="0::'a"])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   515
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   516
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   517
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   518
lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   519
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   520
lemma linear_neg: "linear f ==> f (-x) = - f x"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   521
  using linear_cmul [where c="-1"] by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   522
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   523
lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   524
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   525
lemma linear_sub: "linear f ==> f(x - y) = f x - f y"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   526
  by (simp add: diff_def linear_add linear_neg)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   527
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   528
lemma linear_setsum:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   529
  assumes lf: "linear f" and fS: "finite S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   530
  shows "f (setsum g S) = setsum (f o g) S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   531
proof (induct rule: finite_induct[OF fS])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   532
  case 1 thus ?case by (simp add: linear_0[OF lf])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   533
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   534
  case (2 x F)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   535
  have "f (setsum g (insert x F)) = f (g x + setsum g F)" using "2.hyps"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   536
    by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   537
  also have "\<dots> = f (g x) + f (setsum g F)" using linear_add[OF lf] by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   538
  also have "\<dots> = setsum (f o g) (insert x F)" using "2.hyps" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   539
  finally show ?case .
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   540
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   541
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   542
lemma linear_setsum_mul:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   543
  assumes lf: "linear f" and fS: "finite S"
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   544
  shows "f (setsum (\<lambda>i. c i *\<^sub>R v i) S) = setsum (\<lambda>i. c i *\<^sub>R f (v i)) S"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   545
  using linear_setsum[OF lf fS, of "\<lambda>i. c i *\<^sub>R v i" , unfolded o_def]
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   546
  linear_cmul[OF lf] by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   547
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   548
lemma linear_injective_0:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   549
  assumes lf: "linear f"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   550
  shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   551
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   552
  have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)" by (simp add: inj_on_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   553
  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x - f y = 0 \<longrightarrow> x - y = 0)" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   554
  also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x - y) = 0 \<longrightarrow> x - y = 0)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   555
    by (simp add: linear_sub[OF lf])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   556
  also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   557
  finally show ?thesis .
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   558
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   559
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   560
subsection{* Bilinear functions. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   561
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   562
definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   563
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   564
lemma bilinear_ladd: "bilinear h ==> h (x + y) z = (h x z) + (h y z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   565
  by (simp add: bilinear_def linear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   566
lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   567
  by (simp add: bilinear_def linear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   568
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   569
lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   570
  by (simp add: bilinear_def linear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   571
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   572
lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   573
  by (simp add: bilinear_def linear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   574
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   575
lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   576
  by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   577
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   578
lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   579
  by (simp only: scaleR_minus1_left [symmetric] bilinear_rmul)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   580
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   581
lemma  (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   582
  using add_imp_eq[of x y 0] by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   583
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   584
lemma bilinear_lzero:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   585
  assumes bh: "bilinear h" shows "h 0 x = 0"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   586
  using bilinear_ladd[OF bh, of 0 0 x]
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   587
    by (simp add: eq_add_iff field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   588
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   589
lemma bilinear_rzero:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   590
  assumes bh: "bilinear h" shows "h x 0 = 0"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   591
  using bilinear_radd[OF bh, of x 0 0 ]
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   592
    by (simp add: eq_add_iff field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   593
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   594
lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   595
  by (simp  add: diff_def bilinear_ladd bilinear_lneg)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   596
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   597
lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   598
  by (simp  add: diff_def bilinear_radd bilinear_rneg)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   599
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   600
lemma bilinear_setsum:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   601
  assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   602
  shows "h (setsum f S) (setsum g T) = setsum (\<lambda>(i,j). h (f i) (g j)) (S \<times> T) "
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   603
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   604
  have "h (setsum f S) (setsum g T) = setsum (\<lambda>x. h (f x) (setsum g T)) S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   605
    apply (rule linear_setsum[unfolded o_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   606
    using bh fS by (auto simp add: bilinear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   607
  also have "\<dots> = setsum (\<lambda>x. setsum (\<lambda>y. h (f x) (g y)) T) S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   608
    apply (rule setsum_cong, simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   609
    apply (rule linear_setsum[unfolded o_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   610
    using bh fT by (auto simp add: bilinear_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   611
  finally show ?thesis unfolding setsum_cartesian_product .
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   612
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   613
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   614
subsection{* Adjoints. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   615
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   616
definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   617
36596
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   618
lemma adjoint_unique:
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   619
  assumes "\<forall>x y. inner (f x) y = inner x (g y)"
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   620
  shows "adjoint f = g"
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   621
unfolding adjoint_def
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   622
proof (rule some_equality)
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   623
  show "\<forall>x y. inner (f x) y = inner x (g y)" using assms .
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   624
next
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   625
  fix h assume "\<forall>x y. inner (f x) y = inner x (h y)"
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   626
  hence "\<forall>x y. inner x (g y) = inner x (h y)" using assms by simp
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   627
  hence "\<forall>x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right)
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   628
  hence "\<forall>y. inner (g y - h y) (g y - h y) = 0" by simp
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   629
  hence "\<forall>y. h y = g y" by simp
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   630
  thus "h = g" by (simp add: ext)
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   631
qed
5ef18d433634 generalize lemma adjoint_unique; simplify some proofs
huffman
parents: 36595
diff changeset
   632
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   633
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   634
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   635
subsection{* Interlude: Some properties of real sets *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   636
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   637
lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   638
  shows "\<forall>n \<ge> m. d n < e m"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   639
  using prems apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   640
  apply (erule_tac x="n" in allE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   641
  apply (erule_tac x="n" in allE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   642
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   643
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   644
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   645
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   646
lemma infinite_enumerate: assumes fS: "infinite S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   647
  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   648
unfolding subseq_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   649
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   650
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   651
lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   652
apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   653
apply (rule_tac x="d/2" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   654
apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   655
done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   656
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   657
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   658
lemma triangle_lemma:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   659
  assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   660
  shows "x <= y + z"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   661
proof-
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   662
  have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   663
  with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   664
  from y z have yz: "y + z \<ge> 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   665
  from power2_le_imp_le[OF th yz] show ?thesis .
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   666
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   667
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   668
text {* TODO: move to NthRoot *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   669
lemma sqrt_add_le_add_sqrt:
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   670
  assumes x: "0 \<le> x" and y: "0 \<le> y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   671
  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   672
apply (rule power2_le_imp_le)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   673
apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   674
apply (simp add: mult_nonneg_nonneg x y)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   675
apply (simp add: add_nonneg_nonneg x y)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   676
done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   677
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   678
subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   679
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   680
definition hull :: "'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   681
  "S hull s = Inter {t. t \<in> S \<and> s \<subseteq> t}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   682
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   683
lemma hull_same: "s \<in> S \<Longrightarrow> S hull s = s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   684
  unfolding hull_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   685
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   686
lemma hull_in: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) \<in> S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   687
unfolding hull_def subset_iff by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   688
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   689
lemma hull_eq: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) = s \<longleftrightarrow> s \<in> S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   690
using hull_same[of s S] hull_in[of S s] by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   691
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   692
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   693
lemma hull_hull: "S hull (S hull s) = S hull s"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   694
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   695
34964
4e8be3c04d37 Replaced vec1 and dest_vec1 by abbreviation.
hoelzl
parents: 34915
diff changeset
   696
lemma hull_subset[intro]: "s \<subseteq> (S hull s)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   697
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   698
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   699
lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   700
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   701
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   702
lemma hull_antimono: "S \<subseteq> T ==> (T hull s) \<subseteq> (S hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   703
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   704
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   705
lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> t \<in> S ==> (S hull s) \<subseteq> t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   706
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   707
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   708
lemma subset_hull: "t \<in> S ==> S hull s \<subseteq> t \<longleftrightarrow>  s \<subseteq> t"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   709
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   710
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   711
lemma hull_unique: "s \<subseteq> t \<Longrightarrow> t \<in> S \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> t' \<in> S ==> t \<subseteq> t')
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   712
           ==> (S hull s = t)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   713
unfolding hull_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   714
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   715
lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   716
  using hull_minimal[of S "{x. P x}" Q]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   717
  by (auto simp add: subset_eq Collect_def mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   718
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   719
lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S" by (metis hull_subset subset_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   720
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   721
lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   722
unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   723
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   724
lemma hull_union: assumes T: "\<And>T. T \<subseteq> S ==> Inter T \<in> S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   725
  shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   726
apply rule
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   727
apply (rule hull_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   728
unfolding Un_subset_iff
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   729
apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   730
apply (rule hull_minimal)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   731
apply (metis hull_union_subset)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   732
apply (metis hull_in T)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   733
done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   734
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   735
lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> (S hull (insert a s) = S hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   736
  unfolding hull_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   737
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   738
lemma hull_redundant: "a \<in> (S hull s) ==> (S hull (insert a s) = S hull s)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   739
by (metis hull_redundant_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   740
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   741
text{* Archimedian properties and useful consequences. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   742
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   743
lemma real_arch_simple: "\<exists>n. x <= real (n::nat)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   744
  using reals_Archimedean2[of x] apply auto by (rule_tac x="Suc n" in exI, auto)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   745
lemmas real_arch_lt = reals_Archimedean2
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   746
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   747
lemmas real_arch = reals_Archimedean3
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   748
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   749
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   750
  using reals_Archimedean
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   751
  apply (auto simp add: field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   752
  apply (subgoal_tac "inverse (real n) > 0")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   753
  apply arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   754
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   755
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   756
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   757
lemma real_pow_lbound: "0 <= x ==> 1 + real n * x <= (1 + x) ^ n"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   758
proof(induct n)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   759
  case 0 thus ?case by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   760
next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   761
  case (Suc n)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   762
  hence h: "1 + real n * x \<le> (1 + x) ^ n" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   763
  from h have p: "1 \<le> (1 + x) ^ n" using Suc.prems by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   764
  from h have "1 + real n * x + x \<le> (1 + x) ^ n + x" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   765
  also have "\<dots> \<le> (1 + x) ^ Suc n" apply (subst diff_le_0_iff_le[symmetric])
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   766
    apply (simp add: field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   767
    using mult_left_mono[OF p Suc.prems] by simp
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   768
  finally show ?case  by (simp add: real_of_nat_Suc field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   769
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   770
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   771
lemma real_arch_pow: assumes x: "1 < (x::real)" shows "\<exists>n. y < x^n"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   772
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   773
  from x have x0: "x - 1 > 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   774
  from real_arch[OF x0, rule_format, of y]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   775
  obtain n::nat where n:"y < real n * (x - 1)" by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   776
  from x0 have x00: "x- 1 \<ge> 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   777
  from real_pow_lbound[OF x00, of n] n
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   778
  have "y < x^n" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   779
  then show ?thesis by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   780
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   781
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   782
lemma real_arch_pow2: "\<exists>n. (x::real) < 2^ n"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   783
  using real_arch_pow[of 2 x] by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   784
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   785
lemma real_arch_pow_inv: assumes y: "(y::real) > 0" and x1: "x < 1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   786
  shows "\<exists>n. x^n < y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   787
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   788
  {assume x0: "x > 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   789
    from x0 x1 have ix: "1 < 1/x" by (simp add: field_simps)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   790
    from real_arch_pow[OF ix, of "1/y"]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   791
    obtain n where n: "1/y < (1/x)^n" by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   792
    then
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   793
    have ?thesis using y x0 by (auto simp add: field_simps power_divide) }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   794
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   795
  {assume "\<not> x > 0" with y x1 have ?thesis apply auto by (rule exI[where x=1], auto)}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   796
  ultimately show ?thesis by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   797
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   798
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   799
lemma forall_pos_mono: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n::nat. n \<noteq> 0 ==> P(inverse(real n))) \<Longrightarrow> (\<And>e. 0 < e ==> P e)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   800
  by (metis real_arch_inv)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   801
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   802
lemma forall_pos_mono_1: "(\<And>d e::real. d < e \<Longrightarrow> P d ==> P e) \<Longrightarrow> (\<And>n. P(inverse(real (Suc n)))) ==> 0 < e ==> P e"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   803
  apply (rule forall_pos_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   804
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   805
  apply (atomize)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   806
  apply (erule_tac x="n - 1" in allE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   807
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   808
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   809
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   810
lemma real_archimedian_rdiv_eq_0: assumes x0: "x \<ge> 0" and c: "c \<ge> 0" and xc: "\<forall>(m::nat)>0. real m * x \<le> c"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   811
  shows "x = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   812
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   813
  {assume "x \<noteq> 0" with x0 have xp: "x > 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   814
    from real_arch[OF xp, rule_format, of c] obtain n::nat where n: "c < real n * x"  by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   815
    with xc[rule_format, of n] have "n = 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   816
    with n c have False by simp}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   817
  then show ?thesis by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   818
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   819
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
   820
subsection {* Geometric progression *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   821
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   822
lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   823
  (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   824
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   825
  {assume x1: "x = 1" hence ?thesis by simp}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   826
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   827
  {assume x1: "x\<noteq>1"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   828
    hence x1': "x - 1 \<noteq> 0" "1 - x \<noteq> 0" "x - 1 = - (1 - x)" "- (1 - x) \<noteq> 0" by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   829
    from geometric_sum[OF x1, of "Suc n", unfolded x1']
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   830
    have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   831
      unfolding atLeastLessThanSuc_atLeastAtMost
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   832
      using x1' apply (auto simp only: field_simps)
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   833
      apply (simp add: field_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   834
      done
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   835
    then have ?thesis by (simp add: field_simps) }
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   836
  ultimately show ?thesis by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   837
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   838
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   839
lemma sum_gp_multiplied: assumes mn: "m <= n"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   840
  shows "((1::'a::{field}) - x) * setsum (op ^ x) {m..n} = x^m - x^ Suc n"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   841
  (is "?lhs = ?rhs")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   842
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   843
  let ?S = "{0..(n - m)}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   844
  from mn have mn': "n - m \<ge> 0" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   845
  let ?f = "op + m"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   846
  have i: "inj_on ?f ?S" unfolding inj_on_def by auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   847
  have f: "?f ` ?S = {m..n}"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   848
    using mn apply (auto simp add: image_iff Bex_def) by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   849
  have th: "op ^ x o op + m = (\<lambda>i. x^m * x^i)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   850
    by (rule ext, simp add: power_add power_mult)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   851
  from setsum_reindex[OF i, of "op ^ x", unfolded f th setsum_right_distrib[symmetric]]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   852
  have "?lhs = x^m * ((1 - x) * setsum (op ^ x) {0..n - m})" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   853
  then show ?thesis unfolding sum_gp_basic using mn
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   854
    by (simp add: field_simps power_add[symmetric])
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   855
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   856
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   857
lemma sum_gp: "setsum (op ^ (x::'a::{field})) {m .. n} =
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   858
   (if n < m then 0 else if x = 1 then of_nat ((n + 1) - m)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   859
                    else (x^ m - x^ (Suc n)) / (1 - x))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   860
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   861
  {assume nm: "n < m" hence ?thesis by simp}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   862
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   863
  {assume "\<not> n < m" hence nm: "m \<le> n" by arith
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   864
    {assume x: "x = 1"  hence ?thesis by simp}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   865
    moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   866
    {assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   867
      from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   868
    ultimately have ?thesis by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   869
  }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   870
  ultimately show ?thesis by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   871
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   872
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   873
lemma sum_gp_offset: "setsum (op ^ (x::'a::{field})) {m .. m+n} =
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   874
  (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   875
  unfolding sum_gp[of x m "m + n"] power_Suc
36350
bc7982c54e37 dropped group_simps, ring_simps, field_eq_simps
haftmann
parents: 36336
diff changeset
   876
  by (simp add: field_simps power_add)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   877
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   878
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   879
subsection{* A bit of linear algebra. *}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   880
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   881
definition (in real_vector)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   882
  subspace :: "'a set \<Rightarrow> bool" where
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   883
  "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in> S. \<forall>y \<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in>S. c *\<^sub>R x \<in>S )"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   884
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   885
definition (in real_vector) "span S = (subspace hull S)"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   886
definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S - {a}))"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   887
abbreviation (in real_vector) "independent s == ~(dependent s)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   888
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
   889
text {* Closure properties of subspaces. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   890
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   891
lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   892
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   893
lemma (in real_vector) subspace_0: "subspace S ==> 0 \<in> S" by (metis subspace_def)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   894
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   895
lemma (in real_vector) subspace_add: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S ==> x + y \<in> S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   896
  by (metis subspace_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   897
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   898
lemma (in real_vector) subspace_mul: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> c *\<^sub>R x \<in> S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   899
  by (metis subspace_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   900
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   901
lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   902
  by (metis scaleR_minus1_left subspace_mul)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   903
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   904
lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   905
  by (metis diff_def subspace_add subspace_neg)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   906
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   907
lemma (in real_vector) subspace_setsum:
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   908
  assumes sA: "subspace A" and fB: "finite B"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   909
  and f: "\<forall>x\<in> B. f x \<in> A"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   910
  shows "setsum f B \<in> A"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   911
  using  fB f sA
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   912
  apply(induct rule: finite_induct[OF fB])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   913
  by (simp add: subspace_def sA, auto simp add: sA subspace_add)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   914
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   915
lemma subspace_linear_image:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   916
  assumes lf: "linear f" and sS: "subspace S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   917
  shows "subspace(f ` S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   918
  using lf sS linear_0[OF lf]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   919
  unfolding linear_def subspace_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   920
  apply (auto simp add: image_iff)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   921
  apply (rule_tac x="x + y" in bexI, auto)
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   922
  apply (rule_tac x="c *\<^sub>R x" in bexI, auto)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   923
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   924
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   925
lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \<in> S}"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   926
  by (auto simp add: subspace_def linear_def linear_0[of f])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   927
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   928
lemma subspace_trivial: "subspace {0}"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   929
  by (simp add: subspace_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   930
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   931
lemma (in real_vector) subspace_inter: "subspace A \<Longrightarrow> subspace B ==> subspace (A \<inter> B)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   932
  by (simp add: subspace_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   933
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   934
lemma (in real_vector) span_mono: "A \<subseteq> B ==> span A \<subseteq> span B"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   935
  by (metis span_def hull_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   936
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   937
lemma (in real_vector) subspace_span: "subspace(span S)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   938
  unfolding span_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   939
  apply (rule hull_in[unfolded mem_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   940
  apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   941
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   942
  apply (erule_tac x="X" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   943
  apply (simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   944
  apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   945
  apply (erule_tac x="X" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   946
  apply (erule_tac x="X" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   947
  apply (erule_tac x="X" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   948
  apply (clarsimp simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   949
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   950
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   951
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   952
  apply (erule_tac x="X" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   953
  apply (erule_tac x="X" in ballE)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   954
  apply (simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   955
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   956
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   957
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   958
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   959
lemma (in real_vector) span_clauses:
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   960
  "a \<in> S ==> a \<in> span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   961
  "0 \<in> span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   962
  "x\<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   963
  "x \<in> span S \<Longrightarrow> c *\<^sub>R x \<in> span S"
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   964
  by (metis span_def hull_subset subset_eq)
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
   965
     (metis subspace_span subspace_def)+
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   966
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   967
lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   968
  and P: "subspace P" and x: "x \<in> span S" shows "P x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   969
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   970
  from SP have SP': "S \<subseteq> P" by (simp add: mem_def subset_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   971
  from P have P': "P \<in> subspace" by (simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   972
  from x hull_minimal[OF SP' P', unfolded span_def[symmetric]]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   973
  show "P x" by (metis mem_def subset_eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   974
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   975
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   976
lemma span_empty[simp]: "span {} = {0}"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   977
  apply (simp add: span_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   978
  apply (rule hull_unique)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   979
  apply (auto simp add: mem_def subspace_def)
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
   980
  unfolding mem_def[of "0::'a", symmetric]
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   981
  apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   982
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   983
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   984
lemma (in real_vector) independent_empty[intro]: "independent {}"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   985
  by (simp add: dependent_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   986
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   987
lemma dependent_single[simp]:
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   988
  "dependent {x} \<longleftrightarrow> x = 0"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   989
  unfolding dependent_def by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   990
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   991
lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A ==> independent B"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   992
  apply (clarsimp simp add: dependent_def span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   993
  apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   994
  apply force
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   995
  apply (rule span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   996
  apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   997
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
   998
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
   999
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow>  subspace B \<Longrightarrow> span A = B"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1000
  by (metis order_antisym span_def hull_minimal mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1001
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1002
lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1003
  and P: "subspace P" shows "\<forall>x \<in> span S. P x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1004
  using span_induct SP P by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1005
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1006
inductive (in real_vector) span_induct_alt_help for S:: "'a \<Rightarrow> bool"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1007
  where
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1008
  span_induct_alt_help_0: "span_induct_alt_help S 0"
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1009
  | span_induct_alt_help_S: "x \<in> S \<Longrightarrow> span_induct_alt_help S z \<Longrightarrow> span_induct_alt_help S (c *\<^sub>R x + z)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1010
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1011
lemma span_induct_alt':
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1012
  assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" shows "\<forall>x \<in> span S. h x"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1013
proof-
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1014
  {fix x:: "'a" assume x: "span_induct_alt_help S x"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1015
    have "h x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1016
      apply (rule span_induct_alt_help.induct[OF x])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1017
      apply (rule h0)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1018
      apply (rule hS, assumption, assumption)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1019
      done}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1020
  note th0 = this
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1021
  {fix x assume x: "x \<in> span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1022
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1023
    have "span_induct_alt_help S x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1024
      proof(rule span_induct[where x=x and S=S])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1025
        show "x \<in> span S" using x .
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1026
      next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1027
        fix x assume xS : "x \<in> S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1028
          from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1029
          show "span_induct_alt_help S x" by simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1030
        next
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1031
        have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1032
        moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1033
        {fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1034
          from h
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1035
          have "span_induct_alt_help S (x + y)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1036
            apply (induct rule: span_induct_alt_help.induct)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1037
            apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1038
            unfolding add_assoc
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1039
            apply (rule span_induct_alt_help_S)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1040
            apply assumption
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1041
            apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1042
            done}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1043
        moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1044
        {fix c x assume xt: "span_induct_alt_help S x"
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1045
          then have "span_induct_alt_help S (c *\<^sub>R x)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1046
            apply (induct rule: span_induct_alt_help.induct)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1047
            apply (simp add: span_induct_alt_help_0)
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1048
            apply (simp add: scaleR_right_distrib)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1049
            apply (rule span_induct_alt_help_S)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1050
            apply assumption
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1051
            apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1052
            done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1053
        }
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1054
        ultimately show "subspace (span_induct_alt_help S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1055
          unfolding subspace_def mem_def Ball_def by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1056
      qed}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1057
  with th0 show ?thesis by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1058
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1059
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1060
lemma span_induct_alt:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1061
  assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" and x: "x \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1062
  shows "h x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1063
using span_induct_alt'[of h S] h0 hS x by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1064
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
  1065
text {* Individual closure properties. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1066
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1067
lemma (in real_vector) span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1068
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1069
lemma (in real_vector) span_0: "0 \<in> span S" by (metis subspace_span subspace_0)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1070
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1071
lemma (in real_vector) dependent_0: assumes "0\<in>A" shows "dependent A"
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1072
  unfolding dependent_def apply(rule_tac x=0 in bexI)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1073
  using assms span_0 by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1074
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1075
lemma (in real_vector) span_add: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1076
  by (metis subspace_add subspace_span)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1077
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1078
lemma (in real_vector) span_mul: "x \<in> span S ==> (c *\<^sub>R x) \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1079
  by (metis subspace_span subspace_mul)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1080
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1081
lemma span_neg: "x \<in> span S ==> - x \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1082
  by (metis subspace_neg subspace_span)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1083
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1084
lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S ==> x - y \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1085
  by (metis subspace_span subspace_sub)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1086
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1087
lemma (in real_vector) span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S"
36362
06475a1547cb fix lots of looping simp calls and other warnings
huffman
parents: 36336
diff changeset
  1088
  by (rule subspace_setsum, rule subspace_span)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1089
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1090
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1091
  apply (auto simp only: span_add span_sub)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1092
  apply (subgoal_tac "(x + y) - x \<in> span S", simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1093
  by (simp only: span_add span_sub)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1094
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
  1095
text {* Mapping under linear image. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1096
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1097
lemma span_linear_image: assumes lf: "linear f"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1098
  shows "span (f ` S) = f ` (span S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1099
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1100
  {fix x
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1101
    assume x: "x \<in> span (f ` S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1102
    have "x \<in> f ` span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1103
      apply (rule span_induct[where x=x and S = "f ` S"])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1104
      apply (clarsimp simp add: image_iff)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1105
      apply (frule span_superset)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1106
      apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1107
      apply (simp only: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1108
      apply (rule subspace_linear_image[OF lf])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1109
      apply (rule subspace_span)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1110
      apply (rule x)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1111
      done}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1112
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1113
  {fix x assume x: "x \<in> span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1114
    have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_ext)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1115
      unfolding mem_def Collect_def ..
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1116
    have "f x \<in> span (f ` S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1117
      apply (rule span_induct[where S=S])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1118
      apply (rule span_superset)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1119
      apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1120
      apply (subst th0)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1121
      apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1122
      apply (rule x)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1123
      done}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1124
  ultimately show ?thesis by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1125
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1126
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
  1127
text {* The key breakdown property. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1128
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1129
lemma span_breakdown:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1130
  assumes bS: "b \<in> S" and aS: "a \<in> span S"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1131
  shows "\<exists>k. a - k *\<^sub>R b \<in> span (S - {b})" (is "?P a")
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1132
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1133
  {fix x assume xS: "x \<in> S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1134
    {assume ab: "x = b"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1135
      then have "?P x"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1136
        apply simp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1137
        apply (rule exI[where x="1"], simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1138
        by (rule span_0)}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1139
    moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1140
    {assume ab: "x \<noteq> b"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1141
      then have "?P x"  using xS
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1142
        apply -
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1143
        apply (rule exI[where x=0])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1144
        apply (rule span_superset)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1145
        by simp}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1146
    ultimately have "?P x" by blast}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1147
  moreover have "subspace ?P"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1148
    unfolding subspace_def
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1149
    apply auto
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1150
    apply (simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1151
    apply (rule exI[where x=0])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1152
    using span_0[of "S - {b}"]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1153
    apply (simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1154
    apply (clarsimp simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1155
    apply (rule_tac x="k + ka" in exI)
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1156
    apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1157
    apply (simp only: )
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1158
    apply (rule span_add[unfolded mem_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1159
    apply assumption+
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1160
    apply (simp add: algebra_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1161
    apply (clarsimp simp add: mem_def)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1162
    apply (rule_tac x= "c*k" in exI)
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1163
    apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1164
    apply (simp only: )
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1165
    apply (rule span_mul[unfolded mem_def])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1166
    apply assumption
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1167
    by (simp add: algebra_simps)
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1168
  ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1169
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1170
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1171
lemma span_breakdown_eq:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1172
  "x \<in> span (insert a S) \<longleftrightarrow> (\<exists>k. (x - k *\<^sub>R a) \<in> span S)" (is "?lhs \<longleftrightarrow> ?rhs")
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1173
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1174
  {assume x: "x \<in> span (insert a S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1175
    from x span_breakdown[of "a" "insert a S" "x"]
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1176
    have ?rhs apply clarsimp
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1177
      apply (rule_tac x= "k" in exI)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1178
      apply (rule set_rev_mp[of _ "span (S - {a})" _])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1179
      apply assumption
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1180
      apply (rule span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1181
      apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1182
      done}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1183
  moreover
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1184
  { fix k assume k: "x - k *\<^sub>R a \<in> span S"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1185
    have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by simp
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1186
    have "(x - k *\<^sub>R a) + k *\<^sub>R a \<in> span (insert a S)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1187
      apply (rule span_add)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1188
      apply (rule set_rev_mp[of _ "span S" _])
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1189
      apply (rule k)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1190
      apply (rule span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1191
      apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1192
      apply (rule span_mul)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1193
      apply (rule span_superset)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1194
      apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1195
      done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1196
    then have ?lhs using eq by metis}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1197
  ultimately show ?thesis by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1198
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1199
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
  1200
text {* Hence some "reversal" results. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1201
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1202
lemma in_span_insert:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1203
  assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1204
  shows "b \<in> span (insert a S)"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1205
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1206
  from span_breakdown[of b "insert b S" a, OF insertI1 a]
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1207
  obtain k where k: "a - k*\<^sub>R b \<in> span (S - {b})" by auto
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1208
  {assume k0: "k = 0"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1209
    with k have "a \<in> span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1210
      apply (simp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1211
      apply (rule set_rev_mp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1212
      apply assumption
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1213
      apply (rule span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1214
      apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1215
      done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1216
    with na  have ?thesis by blast}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1217
  moreover
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1218
  {assume k0: "k \<noteq> 0"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1219
    have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by simp
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1220
    from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b"
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1221
      by (simp add: algebra_simps)
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1222
    from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \<in> span (S - {b})"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1223
      by (rule span_mul)
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1224
    hence th: "(1/k) *\<^sub>R a - b \<in> span (S - {b})"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1225
      unfolding eq' .
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1226
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1227
    from k
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1228
    have ?thesis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1229
      apply (subst eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1230
      apply (rule span_sub)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1231
      apply (rule span_mul)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1232
      apply (rule span_superset)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1233
      apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1234
      apply (rule set_rev_mp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1235
      apply (rule th)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1236
      apply (rule span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1237
      using na by blast}
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1238
  ultimately show ?thesis by blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1239
qed
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1240
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1241
lemma in_span_delete:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1242
  assumes a: "a \<in> span S"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1243
  and na: "a \<notin> span (S-{b})"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1244
  shows "b \<in> span (insert a (S - {b}))"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1245
  apply (rule in_span_insert)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1246
  apply (rule set_rev_mp)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1247
  apply (rule a)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1248
  apply (rule span_mono)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1249
  apply blast
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1250
  apply (rule na)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1251
  done
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1252
36666
1ea81fc5227a convert comments to 'text' blocks
huffman
parents: 36623
diff changeset
  1253
text {* Transitivity property. *}
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1254
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1255
lemma span_trans:
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1256
  assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1257
  shows "y \<in> span S"
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1258
proof-
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1259
  from span_breakdown[of x "insert x S" y, OF insertI1 y]
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36592
diff changeset
  1260
  obtain k where k: "y -k*\<^sub>R x \<in> span (S - {x})" by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36778
diff changeset
  1261
  have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by simp
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1262
  show ?thesis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1263
    apply (subst eq)
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents:
diff changeset
  1264
    apply (rule span_add)
2083bde13ce1 distinguished session for multivariate analysis
himmelma