--- a/src/HOL/Analysis/Determinants.thy Thu May 10 18:17:43 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy Thu May 10 18:17:55 2018 +0200
@@ -77,7 +77,7 @@
}
then show ?thesis
unfolding det_def
- by (subst sum_permutations_inverse) (blast intro: sum.cong elim: )
+ by (subst sum_permutations_inverse) (blast intro: sum.cong)
qed
lemma det_lowerdiagonal:
@@ -91,7 +91,7 @@
have fU: "finite ?U"
by simp
have id0: "{id} \<subseteq> ?PU"
- by (auto simp add: permutes_id)
+ by (auto simp: permutes_id)
have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
proof
fix p
@@ -118,7 +118,7 @@
have fU: "finite ?U"
by simp
have id0: "{id} \<subseteq> ?PU"
- by (auto simp add: permutes_id)
+ by (auto simp: permutes_id)
have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
proof
fix p
@@ -145,7 +145,7 @@
have fU: "finite ?U" by simp
from finite_permutations[OF fU] have fPU: "finite ?PU" .
have id0: "{id} \<subseteq> ?PU"
- by (auto simp add: permutes_id)
+ by (auto simp: permutes_id)
have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
proof
fix p
@@ -250,8 +250,8 @@
have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x"
by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq
permutation_permutes permutation_swap_id sign_compose x)
- also have "... = - sign x" using sign_tjk by simp
- also have "... \<noteq> sign x" unfolding sign_def by simp
+ also have "\<dots> = - sign x" using sign_tjk by simp
+ also have "\<dots> \<noteq> sign x" unfolding sign_def by simp
finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2"
using x by force+
}
@@ -274,9 +274,9 @@
have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))
\<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}"
unfolding g_S1 by (rule sum.reindex[OF inj_g])
- also have "... = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
- unfolding o_def by (rule sum.cong, auto simp add: tjk_eq)
- also have "... = sum (\<lambda>p. - ?f p) ?S1"
+ also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
+ unfolding o_def by (rule sum.cong, auto simp: tjk_eq)
+ also have "\<dots> = sum (\<lambda>p. - ?f p) ?S1"
proof (rule sum.cong, auto)
fix x assume x: "x permutes ?U"
and even_x: "evenperm x"
@@ -289,14 +289,14 @@
= - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))"
by auto
qed
- also have "...= - sum ?f ?S1" unfolding sum_negf ..
+ also have "\<dots>= - sum ?f ?S1" unfolding sum_negf ..
finally have *: "sum ?f ?S2 = - sum ?f ?S1" .
have "det A = (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))"
unfolding det_def ..
- also have "...= sum ?f ?S1 + sum ?f ?S2"
+ also have "\<dots>= sum ?f ?S1 + sum ?f ?S2"
by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto)
- also have "...= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
- also have "...= 0" by simp
+ also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
+ also have "\<dots>= 0" by simp
finally show "det A = 0" by simp
qed
@@ -309,7 +309,7 @@
lemma det_zero_row:
fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
- by (force simp add: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
+ by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
lemma det_zero_column:
fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
@@ -376,7 +376,7 @@
have kU: "?U = insert k ?Uk"
by blast
have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
- by (auto simp: )
+ by auto
have Uk: "finite ?Uk" "k \<notin> ?Uk"
by auto
have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
@@ -475,7 +475,7 @@
proof (cases "\<forall>i j. i \<noteq> j \<longrightarrow> row i A \<noteq> row j A")
case True
with i have "vec.span (rows A - {row i A}) \<subseteq> vec.span {row j A |j. j \<noteq> i}"
- by (auto simp add: rows_def intro!: vec.span_mono)
+ by (auto simp: rows_def intro!: vec.span_mono)
then have "- row i A \<in> vec.span {row j A|j. j \<noteq> i}"
by (meson i subsetCE vec.span_neg)
from det_row_span[OF this]
@@ -515,17 +515,16 @@
have *: "{f. \<forall>i. f i = i} = {id}"
by auto
show ?case
- by (auto simp add: *)
+ by (auto simp: *)
next
case (Suc k)
let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>{1..k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)})"
have "?S = {f. (\<forall>i\<in>{1.. Suc k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. Suc k} \<longrightarrow> f i = i)}"
- apply (auto simp add: image_iff)
+ apply (auto simp: image_iff)
apply (rename_tac f)
apply (rule_tac x="f (Suc k)" in bexI)
- apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI)
- apply auto
+ apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI, auto)
done
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
show ?case
@@ -736,7 +735,7 @@
by blast
have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
unfolding sum_cmul using c ci
- by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
+ by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}"
unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum)
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n"
@@ -789,7 +788,7 @@
show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
proof (intro exI conjI)
show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
- by (simp add:)
+ by simp
show "(( *v) B) \<circ> f = id"
unfolding o_def
by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
@@ -817,7 +816,7 @@
show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
proof (intro exI conjI)
show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
- by (simp add: )
+ by simp
show "f \<circ> ( *v) B = id"
using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
by (metis (no_types, hide_lams))
@@ -967,7 +966,7 @@
lemma orthogonal_transformation_compose:
"\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
- by (auto simp add: orthogonal_transformation_def linear_compose)
+ by (auto simp: orthogonal_transformation_def linear_compose)
lemma orthogonal_transformation_neg:
"orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
@@ -1018,8 +1017,7 @@
using oA oB
unfolding orthogonal_matrix matrix_transpose_mul
apply (subst matrix_mul_assoc)
- apply (subst matrix_mul_assoc[symmetric])
- apply (simp add: )
+ apply (subst matrix_mul_assoc[symmetric], simp)
done
lemma orthogonal_transformation_matrix:
@@ -1081,8 +1079,7 @@
have th0: "x * x - 1 = (x - 1) * (x + 1)"
by (simp add: field_simps)
have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
- apply (subst eq_iff_diff_eq_0)
- apply simp
+ apply (subst eq_iff_diff_eq_0, simp)
done
have "x * x = 1 \<longleftrightarrow> x * x - 1 = 0"
by simp
@@ -1199,7 +1196,7 @@
proof -
obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
and "independent S" "card S = CARD('n)" "span S = UNIV"
- using vector_in_orthonormal_basis assms by (force simp: )
+ using vector_in_orthonormal_basis assms by force
then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
@@ -1349,7 +1346,7 @@
"norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
using z
- by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+ by (auto simp: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
by (simp add: dist_norm)
}
--- a/src/HOL/Analysis/Infinite_Products.thy Thu May 10 18:17:43 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Thu May 10 18:17:55 2018 +0200
@@ -75,8 +75,33 @@
lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
by (simp add: gen_has_prod_def)
+lemma gen_has_prod_eq_0:
+ fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+ assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m"
+ shows "p = 0"
+proof -
+ have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n
+ by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff)
+ have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0"
+ by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)
+ with p show ?thesis
+ unfolding gen_has_prod_def
+ using LIMSEQ_unique by blast
+qed
+
lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))"
by (simp add: has_prod_def)
+
+lemma has_prod_unique2:
+ fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+ assumes "f has_prod a" "f has_prod b" shows "a = b"
+ using assms
+ by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique)
+
+lemma has_prod_unique:
+ fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}"
+ shows "f has_prod s \<Longrightarrow> s = prodinf f"
+ by (simp add: has_prod_unique2 prodinf_def the_equality)
lemma convergent_prod_altdef:
fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
@@ -176,14 +201,14 @@
next
assume ?rhs then show ?lhs
unfolding prod_defs
- by (rule_tac x="0" in exI) (auto simp: )
+ by (rule_tac x=0 in exI) auto
qed
lemma convergent_prod_iff_convergent:
fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
assumes "\<And>i. f i \<noteq> 0"
shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
- by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
+ by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
lemma abs_convergent_prod_altdef:
@@ -385,7 +410,14 @@
unfolding prod_defs by blast
qed
-lemma abs_convergent_prod_ignore_initial_segment:
+corollary convergent_prod_ignore_nonzero_segment:
+ fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
+ assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
+ shows "\<exists>p. gen_has_prod f M p"
+ using convergent_prod_ignore_initial_segment [OF f]
+ by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))
+
+corollary abs_convergent_prod_ignore_initial_segment:
assumes "abs_convergent_prod f"
shows "abs_convergent_prod (\<lambda>n. f (n + m))"
using assms unfolding abs_convergent_prod_def
@@ -519,15 +551,13 @@
with L show ?thesis by (auto simp: prod_defs)
qed
-lemma convergent_prod_offset_0:
+lemma gen_has_prod_cases:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
- assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
- shows "\<exists>p. gen_has_prod f 0 p"
- using assms
- unfolding convergent_prod_def
-proof (clarsimp simp: prod_defs)
- fix M p
- assume "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
+ assumes "gen_has_prod f M p"
+ obtains i where "i<M" "f i = 0" | p where "gen_has_prod f 0 p"
+proof -
+ have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
+ using assms unfolding gen_has_prod_def by blast+
then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
by (metis tendsto_mult_left)
moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
@@ -536,17 +566,24 @@
by auto
then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
by simp (subst prod.union_disjoint; force)
- also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
+ also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
finally show ?thesis by metis
qed
ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
by (auto intro: LIMSEQ_offset [where k=M])
- then show "\<exists>p. (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
- using \<open>p \<noteq> 0\<close> assms
- by (rule_tac x="prod f {..<M} * p" in exI) auto
+ then have "gen_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
+ using \<open>p \<noteq> 0\<close> assms that by (auto simp: gen_has_prod_def)
+ then show thesis
+ using that by blast
qed
+corollary convergent_prod_offset_0:
+ fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
+ assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
+ shows "\<exists>p. gen_has_prod f 0 p"
+ using assms convergent_prod_def gen_has_prod_cases by blast
+
lemma prodinf_eq_lim:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
@@ -579,7 +616,7 @@
case (elim n)
then have "{..n} = {..<N} \<union> {N..n}"
by auto
- also have "prod f ... = prod f {..<N} * prod f {N..n}"
+ also have "prod f \<dots> = prod f {..<N} * prod f {N..n}"
by (intro prod.union_disjoint) auto
also from N have "prod f {N..n} = prod g {N..n}"
by (intro prod.cong) simp_all
@@ -619,7 +656,7 @@
have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
proof (rule prod.mono_neutral_right)
show "N \<subseteq> {..n + Suc (Max N)}"
- by (auto simp add: le_Suc_eq trans_le_add2)
+ by (auto simp: le_Suc_eq trans_le_add2)
show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
using f by blast
qed auto
@@ -650,7 +687,7 @@
show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}"
using le_Suc_ex by fastforce
qed (auto simp: inj_on_def)
- also have "... = ?q"
+ also have "\<dots> = ?q"
by (rule prod.mono_neutral_right)
(use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
finally show ?thesis .
@@ -714,5 +751,71 @@
shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
+context
+ fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
+begin
+
+lemma convergent_prod_imp_has_prod:
+ assumes "convergent_prod f"
+ shows "\<exists>p. f has_prod p"
+proof -
+ obtain M p where p: "gen_has_prod f M p"
+ using assms convergent_prod_def by blast
+ then have "p \<noteq> 0"
+ using gen_has_prod_nonzero by blast
+ with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i
+ using gen_has_prod_eq_0 that by blast
+ define C where "C = (\<Prod>n<M. f n)"
+ show ?thesis
+ proof (cases "\<forall>n\<le>M. f n \<noteq> 0")
+ case True
+ then have "C \<noteq> 0"
+ by (simp add: C_def)
+ then show ?thesis
+ by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)
+ next
+ case False
+ let ?N = "GREATEST n. f n = 0"
+ have 0: "f ?N = 0"
+ using fnz False
+ by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)
+ have "f i \<noteq> 0" if "i > ?N" for i
+ by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)
+ then have "\<exists>p. gen_has_prod f (Suc ?N) p"
+ using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)
+ then show ?thesis
+ unfolding has_prod_def using 0 by blast
+ qed
+qed
+
+lemma convergent_prod_has_prod [intro]:
+ shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)"
+ unfolding prodinf_def
+ by (metis convergent_prod_imp_has_prod has_prod_unique theI')
+
+lemma convergent_prod_LIMSEQ:
+ shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f"
+ by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent
+ convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
+
+lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
+proof
+ assume "f has_prod x"
+ then show "convergent_prod f \<and> prodinf f = x"
+ apply safe
+ using convergent_prod_def has_prod_def apply blast
+ using has_prod_unique by blast
+qed auto
+
+lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f"
+ by (auto simp: has_prod_iff convergent_prod_has_prod)
+
+lemma prodinf_finite:
+ assumes N: "finite N"
+ and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
+ shows "prodinf f = (\<Prod>n\<in>N. f n)"
+ using has_prod_finite[OF assms, THEN has_prod_unique] by simp
end
+
+end