--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Apr 06 19:16:34 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Apr 06 19:35:35 2014 +0200
@@ -27,7 +27,7 @@
lemma square_continuous:
fixes e :: real
- shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. abs (y - x) < d \<longrightarrow> abs (y * y - x * x) < e)"
+ shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
using isCont_power[OF isCont_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
apply (auto simp add: power2_eq_square)
apply (rule_tac x="s" in exI)
@@ -221,10 +221,12 @@
"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)"
(is "linear f \<longleftrightarrow> ?rhs")
proof
- assume "linear f" then interpret f: linear f .
+ assume "linear f"
+ then interpret f: linear f .
show "?rhs" by (simp add: f.add f.scaleR)
next
- assume "?rhs" then show "linear f" by unfold_locales simp_all
+ assume "?rhs"
+ then show "linear f" by unfold_locales simp_all
qed
lemma linear_compose_cmul: "linear f \<Longrightarrow> linear (\<lambda>x. c *\<^sub>R f x)"
@@ -255,7 +257,11 @@
case True
then show ?thesis
using lS by induct (simp_all add: linear_zero linear_compose_add)
-qed (simp add: linear_zero)
+next
+ case False
+ then show ?thesis
+ by (simp add: linear_zero)
+qed
lemma linear_0: "linear f \<Longrightarrow> f 0 = 0"
unfolding linear_iff
@@ -283,7 +289,11 @@
case True
then show ?thesis
by induct (simp_all add: linear_0 [OF f] linear_add [OF f])
-qed (simp add: linear_0 [OF f])
+next
+ case False
+ then show ?thesis
+ by (simp add: linear_0 [OF f])
+qed
lemma linear_setsum_mul:
assumes lin: "linear f"
@@ -401,7 +411,7 @@
*}
lemma adjoint_works:
- fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
shows "x \<bullet> adjoint f y = f x \<bullet> y"
proof -
@@ -423,21 +433,21 @@
qed
lemma adjoint_clauses:
- fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
shows "x \<bullet> adjoint f y = f x \<bullet> y"
and "adjoint f y \<bullet> x = y \<bullet> f x"
by (simp_all add: adjoint_works[OF lf] inner_commute)
lemma adjoint_linear:
- fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
shows "linear (adjoint f)"
by (simp add: lf linear_iff euclidean_eq_iff[where 'a='n] euclidean_eq_iff[where 'a='m]
adjoint_clauses[OF lf] inner_distrib)
lemma adjoint_adjoint:
- fixes f:: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
shows "adjoint (adjoint f) = f"
by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
@@ -462,7 +472,7 @@
unfolding subseq_def
using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
-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)"
+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)"
apply auto
apply (rule_tac x="d/2" in exI)
apply auto
@@ -476,7 +486,7 @@
and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
shows "x \<le> y + z"
proof -
- have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 *y * z + z\<^sup>2"
+ have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
using z y by (simp add: mult_nonneg_nonneg)
with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
by (simp add: power2_eq_square field_simps)
@@ -546,16 +556,16 @@
apply (metis hull_in T)
done
-lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> (S hull (insert a s) = S hull s)"
+lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
unfolding hull_def by blast
-lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> (S hull (insert a s) = S hull s)"
+lemma hull_redundant: "a \<in> (S hull s) \<Longrightarrow> S hull (insert a s) = S hull s"
by (metis hull_redundant_eq)
subsection {* Archimedean properties and useful consequences *}
-lemma real_arch_simple: "\<exists>n. x \<le> real (n::nat)"
+lemma real_arch_simple: "\<exists>n::nat. x \<le> real n"
unfolding real_of_nat_def by (rule ex_le_of_nat)
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
@@ -647,7 +657,7 @@
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"
+ and xc: "\<forall>(m::nat) > 0. real m * x \<le> c"
shows "x = 0"
proof (rule ccontr)
assume "x \<noteq> 0"
@@ -665,7 +675,7 @@
subsection{* A bit of linear algebra. *}
definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
- where "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 )"
+ where "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)"
definition (in real_vector) "span S = (subspace hull S)"
definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
@@ -797,7 +807,7 @@
shows "\<forall>x \<in> span S. P x"
using span_induct SP P by blast
-inductive_set (in real_vector) span_induct_alt_help for S:: "'a set"
+inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
where
span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
| span_induct_alt_help_S:
@@ -919,7 +929,7 @@
lemma span_linear_image:
assumes lf: "linear f"
- shows "span (f ` S) = f ` (span S)"
+ shows "span (f ` S) = f ` span S"
proof (rule span_unique)
show "f ` S \<subseteq> f ` span S"
by (intro image_mono span_inc)
@@ -1414,7 +1424,7 @@
done
lemma setsum_norm_allsubsets_bound:
- fixes f:: "'a \<Rightarrow> 'n::euclidean_space"
+ fixes f :: "'a \<Rightarrow> 'n::euclidean_space"
assumes fP: "finite P"
and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
shows "(\<Sum>x\<in>P. norm (f x)) \<le> 2 * real DIM('n) * e"
@@ -1429,7 +1439,8 @@
assume i: "i \<in> Basis"
have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
norm ((\<Sum>x\<in>P \<inter> - {x. f x \<bullet> i < 0}. f x) \<bullet> i) + norm ((\<Sum>x\<in>P \<inter> {x. f x \<bullet> i < 0}. f x) \<bullet> i)"
- by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left del: real_norm_def)
+ by (simp add: abs_real_def setsum_cases[OF fP] setsum_negf norm_triangle_ineq4 inner_setsum_left
+ del: real_norm_def)
also have "\<dots> \<le> e + e"
unfolding real_norm_def
by (intro add_mono norm_bound_Basis_le i fPs) auto
@@ -1444,7 +1455,7 @@
subsection {* Linearity and Bilinearity continued *}
lemma linear_bounded:
- fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
proof
@@ -1496,7 +1507,7 @@
qed
lemma linear_bounded_pos:
- fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
proof -
@@ -1508,7 +1519,7 @@
qed
lemma bounded_linearI':
- fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<And>x y. f (x + y) = f x + f y"
and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
shows "bounded_linear f"
@@ -1516,7 +1527,7 @@
by (rule linearI[OF assms])
lemma bilinear_bounded:
- fixes h:: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
+ fixes h :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'k::real_normed_vector"
assumes bh: "bilinear h"
shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof (clarify intro!: exI[of _ "\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)"])
@@ -1582,7 +1593,7 @@
qed
lemma bilinear_bounded_pos:
- fixes h:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
assumes bh: "bilinear h"
shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof -
@@ -1602,7 +1613,8 @@
using independent_span_bound[OF finite_Basis, of S] by auto
lemma dependent_biggerset:
- "(finite (S::('a::euclidean_space) set) \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
+ fixes S :: "'a::euclidean_space set"
+ shows "(finite S \<Longrightarrow> card S > DIM('a)) \<Longrightarrow> dependent S"
by (metis independent_bound not_less)
text {* Hence we can create a maximal independent subset. *}
@@ -1816,7 +1828,7 @@
by (metis dim_span dim_subset)
lemma span_eq_dim:
- fixes S:: "'a::euclidean_space set"
+ fixes S :: "'a::euclidean_space set"
shows "span S = span T \<Longrightarrow> dim S = dim T"
by (metis dim_span)
@@ -2003,7 +2015,7 @@
lemma span_not_univ_orthogonal:
fixes S :: "'a::euclidean_space set"
assumes sU: "span S \<noteq> UNIV"
- shows "\<exists>(a::'a). a \<noteq>0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
+ shows "\<exists>a::'a. a \<noteq> 0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
proof -
from sU obtain a where a: "a \<notin> span S"
by blast
@@ -2066,7 +2078,7 @@
lemma lowdim_subset_hyperplane:
fixes S :: "'a::euclidean_space set"
assumes d: "dim S < DIM('a)"
- shows "\<exists>(a::'a). a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
+ shows "\<exists>a::'a. a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
proof -
{
assume "span S = UNIV"
@@ -2382,7 +2394,8 @@
qed
lemma linear_eq_stdbasis:
- assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> _)"
+ fixes f :: "'a::euclidean_space \<Rightarrow> _"
+ assumes lf: "linear f"
and lg: "linear g"
and fg: "\<forall>b\<in>Basis. f b = g b"
shows "f = g"
@@ -2429,18 +2442,19 @@
text {* Detailed theorems about left and right invertibility in general case. *}
lemma linear_injective_left_inverse:
- fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes lf: "linear f" and fi: "inj f"
- shows "\<exists>g. linear g \<and> g o f = id"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes lf: "linear f"
+ and fi: "inj f"
+ shows "\<exists>g. linear g \<and> g \<circ> f = id"
proof -
from linear_independent_extend[OF independent_injective_image, OF independent_Basis, OF lf fi]
- obtain h:: "'b \<Rightarrow> 'a" where h: "linear h" "\<forall>x \<in> f ` Basis. h x = inv f x"
+ obtain h :: "'b \<Rightarrow> 'a" where h: "linear h" "\<forall>x \<in> f ` Basis. h x = inv f x"
by blast
from h(2) have th: "\<forall>i\<in>Basis. (h \<circ> f) i = id i"
using inv_o_cancel[OF fi, unfolded fun_eq_iff id_def o_def]
by auto
from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]
- have "h o f = id" .
+ have "h \<circ> f = id" .
then show ?thesis
using h(1) by blast
qed
@@ -2449,15 +2463,15 @@
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes lf: "linear f"
and sf: "surj f"
- shows "\<exists>g. linear g \<and> f o g = id"
+ shows "\<exists>g. linear g \<and> f \<circ> g = id"
proof -
from linear_independent_extend[OF independent_Basis[where 'a='b],of "inv f"]
- obtain h:: "'b \<Rightarrow> 'a" where h: "linear h" "\<forall>x\<in>Basis. h x = inv f x"
+ obtain h :: "'b \<Rightarrow> 'a" where h: "linear h" "\<forall>x\<in>Basis. h x = inv f x"
by blast
- from h(2) have th: "\<forall>i\<in>Basis. (f o h) i = id i"
+ from h(2) have th: "\<forall>i\<in>Basis. (f \<circ> h) i = id i"
using sf by (auto simp add: surj_iff_all)
from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
- have "f o h = id" .
+ have "f \<circ> h = id" .
then show ?thesis
using h(1) by blast
qed
@@ -2465,7 +2479,7 @@
text {* An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective. *}
lemma linear_injective_imp_surjective:
- fixes f::"'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes lf: "linear f"
and fi: "inj f"
shows "surj f"
@@ -2617,7 +2631,7 @@
by (simp add: fun_eq_iff o_def id_def)
lemma linear_injective_isomorphism:
- fixes f::"'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes lf: "linear f"
and fi: "inj f"
shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
@@ -2687,22 +2701,22 @@
subsection {* Infinity norm *}
-definition "infnorm (x::'a::euclidean_space) = Sup {abs (x \<bullet> b) |b. b \<in> Basis}"
+definition "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
lemma infnorm_set_image:
fixes x :: "'a::euclidean_space"
- shows "{abs (x \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs (x \<bullet> i)) ` Basis"
+ shows "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} = (\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
by blast
lemma infnorm_Max:
fixes x :: "'a::euclidean_space"
- shows "infnorm x = Max ((\<lambda>i. abs (x \<bullet> i)) ` Basis)"
+ shows "infnorm x = Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis)"
by (simp add: infnorm_def infnorm_set_image cSup_eq_Max del: Sup_image_eq)
lemma infnorm_set_lemma:
fixes x :: "'a::euclidean_space"
- shows "finite {abs (x \<bullet> i) |i. i \<in> Basis}"
- and "{abs (x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
+ shows "finite {\<bar>x \<bullet> i\<bar> |i. i \<in> Basis}"
+ and "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} \<noteq> {}"
unfolding infnorm_set_image
by auto
@@ -2750,7 +2764,7 @@
lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
proof -
- have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny <= n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
+ have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
by arith
from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
@@ -2767,7 +2781,7 @@
shows "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm x"
by (simp add: infnorm_Max)
-lemma infnorm_mul: "infnorm (a *\<^sub>R x) = abs a * infnorm x"
+lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \<bar>a\<bar> * infnorm x"
unfolding infnorm_Max
proof (safe intro!: Max_eqI)
let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
@@ -2876,11 +2890,11 @@
qed
lemma norm_cauchy_schwarz_abs_eq:
- "abs (x \<bullet> y) = norm x * norm y \<longleftrightarrow>
+ "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow>
norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"
(is "?lhs \<longleftrightarrow> ?rhs")
proof -
- have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a"
+ have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> \<bar>x\<bar> = a \<longleftrightarrow> x = a \<or> x = - a"
by arith
have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
by simp
@@ -2945,7 +2959,7 @@
apply (rule exI[where x="- 1"], simp)
done
-lemma collinear_lemma: "collinear {0,x,y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
+lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof -
{
@@ -2990,7 +3004,7 @@
ultimately show ?thesis by blast
qed
-lemma norm_cauchy_schwarz_equal: "abs (x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
+lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
unfolding norm_cauchy_schwarz_abs_eq
apply (cases "x=0", simp_all add: collinear_2)
apply (cases "y=0", simp_all add: collinear_2 insert_commute)