new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Fri Dec 22 21:00:07 2017 +0000
@@ -1851,9 +1851,35 @@
using field_differentiable_def has_field_derivative_powr_right by blast
lemma holomorphic_on_powr_right [holomorphic_intros]:
- "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
- unfolding holomorphic_on_def field_differentiable_def
- by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
+ assumes "f holomorphic_on s"
+ shows "(\<lambda>z. w powr (f z)) holomorphic_on s"
+proof (cases "w = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ with assms show ?thesis
+ unfolding holomorphic_on_def field_differentiable_def
+ by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
+qed
+
+lemma holomorphic_on_divide_gen [holomorphic_intros]:
+ assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
+shows "(\<lambda>z. f z / g z) holomorphic_on s"
+proof (cases "\<exists>z\<in>s. g z = 0")
+ case True
+ with 0 have "g z = 0" if "z \<in> s" for z
+ using that by blast
+ then show ?thesis
+ using g holomorphic_transform by auto
+next
+ case False
+ with 0 have "g z \<noteq> 0" if "z \<in> s" for z
+ using that by blast
+ with holomorphic_on_divide show ?thesis
+ using f g by blast
+qed
lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Fri Dec 22 21:00:07 2017 +0000
@@ -175,6 +175,9 @@
lemma abs_summable_on_normI: "f abs_summable_on A \<Longrightarrow> (\<lambda>x. norm (f x)) abs_summable_on A"
by simp
+lemma abs_summable_complex_of_real [simp]: "(\<lambda>n. complex_of_real (f n)) abs_summable_on A \<longleftrightarrow> f abs_summable_on A"
+ by (simp add: abs_summable_on_def complex_of_real_integrable_eq)
+
lemma abs_summable_on_comparison_test:
assumes "g abs_summable_on A"
assumes "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> norm (g x)"
@@ -227,6 +230,23 @@
"f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))"
by (subst abs_summable_on_nat_iff) auto
+lemma nat_abs_summable_on_comparison_test:
+ fixes f :: "nat \<Rightarrow> 'a :: {banach, second_countable_topology}"
+ assumes "g abs_summable_on I"
+ assumes "\<And>n. \<lbrakk>n\<ge>N; n \<in> I\<rbrakk> \<Longrightarrow> norm (f n) \<le> g n"
+ shows "f abs_summable_on I"
+ using assms by (fastforce simp add: abs_summable_on_nat_iff intro: summable_comparison_test')
+
+lemma abs_summable_comparison_test_ev:
+ assumes "g abs_summable_on I"
+ assumes "eventually (\<lambda>x. x \<in> I \<longrightarrow> norm (f x) \<le> g x) sequentially"
+ shows "f abs_summable_on I"
+ by (metis (no_types, lifting) nat_abs_summable_on_comparison_test eventually_at_top_linorder assms)
+
+lemma abs_summable_on_Cauchy:
+ "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. (\<Sum>x = m..<n. norm (f x)) < e)"
+ by (simp add: abs_summable_on_nat_iff' summable_Cauchy sum_nonneg)
+
lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A"
unfolding abs_summable_on_def by (rule integrable_count_space)
--- a/src/HOL/Groups_Big.thy Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Groups_Big.thy Fri Dec 22 21:00:07 2017 +0000
@@ -495,12 +495,12 @@
end
-text \<open>Now: lot's of fancy syntax. First, @{term "sum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
+text \<open>Now: lots of fancy syntax. First, @{term "sum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
syntax (ASCII)
- "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(3SUM _:_./ _)" [0, 51, 10] 10)
+ "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(3SUM (_/:_)./ _)" [0, 51, 10] 10)
syntax
- "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
+ "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>(_/\<in>_)./ _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST sum (\<lambda>i. b) A"
@@ -1062,9 +1062,9 @@
end
syntax (ASCII)
- "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD (_/:_)./ _)" [0, 51, 10] 10)
syntax
- "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>(_/\<in>_)./ _)" [0, 51, 10] 10)
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
--- a/src/HOL/Series.thy Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Series.thy Fri Dec 22 21:00:07 2017 +0000
@@ -564,6 +564,9 @@
lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
+lemma summable_inverse_divide: "summable (inverse \<circ> f) \<Longrightarrow> summable (\<lambda>n. c / f n)"
+ by (auto dest: summable_mult [of _ c] simp: field_simps)
+
lemma sums_mult_D: "(\<lambda>n. c * f n) sums a \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> f sums (a/c)"
using sums_mult_iff by fastforce
@@ -657,31 +660,52 @@
text \<open>Cauchy-type criterion for convergence of series (c.f. Harrison).\<close>
-lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e)"
+lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e)" (is "_ = ?rhs")
for f :: "nat \<Rightarrow> 'a::banach"
- apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff)
- apply safe
- apply (drule spec)
- apply (drule (1) mp)
- apply (erule exE)
- apply (rule_tac x="M" in exI)
- apply clarify
- apply (rule_tac x="m" and y="n" in linorder_le_cases)
- apply (frule (1) order_trans)
- apply (drule_tac x="n" in spec)
- apply (drule (1) mp)
- apply (drule_tac x="m" in spec)
- apply (drule (1) mp)
- apply (simp_all add: sum_diff [symmetric])
- apply (drule spec)
- apply (drule (1) mp)
- apply (erule exE)
- apply (rule_tac x="N" in exI)
- apply clarify
- apply (rule_tac x="m" and y="n" in linorder_le_cases)
- apply (subst norm_minus_commute)
- apply (simp_all add: sum_diff [symmetric])
- done
+proof
+ assume f: "summable f"
+ show ?rhs
+ proof clarify
+ fix e :: real
+ assume "0 < e"
+ then obtain M where M: "\<And>m n. \<lbrakk>m\<ge>M; n\<ge>M\<rbrakk> \<Longrightarrow> norm (sum f {..<m} - sum f {..<n}) < e"
+ using f by (force simp add: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff)
+ have "norm (sum f {m..<n}) < e" if "m \<ge> M" for m n
+ proof (cases m n rule: linorder_class.le_cases)
+ assume "m \<le> n"
+ then show ?thesis
+ by (metis (mono_tags, hide_lams) M atLeast0LessThan order_trans sum_diff_nat_ivl that zero_le)
+ next
+ assume "n \<le> m"
+ then show ?thesis
+ by (simp add: \<open>0 < e\<close>)
+ qed
+ then show "\<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e"
+ by blast
+ qed
+next
+ assume r: ?rhs
+ then show "summable f"
+ unfolding summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff
+ proof clarify
+ fix e :: real
+ assume "0 < e"
+ with r obtain N where N: "\<And>m n. m \<ge> N \<Longrightarrow> norm (sum f {m..<n}) < e"
+ by blast
+ have "norm (sum f {..<m} - sum f {..<n}) < e" if "m\<ge>N" "n\<ge>N" for m n
+ proof (cases m n rule: linorder_class.le_cases)
+ assume "m \<le> n"
+ then show ?thesis
+ by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff norm_minus_commute \<open>m\<ge>N\<close>)
+ next
+ assume "n \<le> m"
+ then show ?thesis
+ by (metis Groups_Big.sum_diff N finite_lessThan lessThan_minus_lessThan lessThan_subset_iff \<open>n\<ge>N\<close>)
+ qed
+ then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (sum f {..<m} - sum f {..<n}) < e"
+ by blast
+ qed
+qed
context
fixes f :: "nat \<Rightarrow> 'a::banach"
@@ -708,23 +732,32 @@
text \<open>Comparison tests.\<close>
-lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f"
- apply (simp add: summable_Cauchy)
- apply safe
- apply (drule_tac x="e" in spec)
- apply safe
- apply (rule_tac x = "N + Na" in exI)
- apply safe
- apply (rotate_tac 2)
- apply (drule_tac x = m in spec)
- apply auto
- apply (rotate_tac 2)
- apply (drule_tac x = n in spec)
- apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
- apply (rule norm_sum)
- apply (rule_tac y = "sum g {m..<n}" in order_le_less_trans)
- apply (auto intro: sum_mono simp add: abs_less_iff)
- done
+lemma summable_comparison_test:
+ assumes fg: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n" and g: "summable g"
+ shows "summable f"
+proof -
+ obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> norm (f n) \<le> g n"
+ using assms by blast
+ show ?thesis
+ proof (clarsimp simp add: summable_Cauchy)
+ fix e :: real
+ assume "0 < e"
+ then obtain Ng where Ng: "\<And>m n. m \<ge> Ng \<Longrightarrow> norm (sum g {m..<n}) < e"
+ using g by (fastforce simp: summable_Cauchy)
+ with N have "norm (sum f {m..<n}) < e" if "m\<ge>max N Ng" for m n
+ proof -
+ have "norm (sum f {m..<n}) \<le> sum g {m..<n}"
+ using N that by (force intro: sum_norm_le)
+ also have "... \<le> norm (sum g {m..<n})"
+ by simp
+ also have "... < e"
+ using Ng that by auto
+ finally show ?thesis .
+ qed
+ then show "\<exists>N. \<forall>m\<ge>N. \<forall>n. norm (sum f {m..<n}) < e"
+ by blast
+ qed
+qed
lemma summable_comparison_test_ev:
"eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
--- a/src/HOL/Set.thy Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Set.thy Fri Dec 22 21:00:07 2017 +0000
@@ -44,9 +44,9 @@
"{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
syntax (ASCII)
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{_ :/ _./ _})")
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/: _)./ _})")
syntax
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{_ \<in>/ _./ _})")
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/\<in> _)./ _})")
translations
"{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
@@ -187,21 +187,21 @@
where "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)" \<comment> "bounded existential quantifiers"
syntax (ASCII)
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3EX! _:_./ _)" [0, 0, 10] 10)
- "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST _:_./ _)" [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3ALL (_/:_)./ _)" [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3EX (_/:_)./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3EX! (_/:_)./ _)" [0, 0, 10] 10)
+ "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST (_/:_)./ _)" [0, 0, 10] 10)
syntax (input)
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3! _:_./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3? _:_./ _)" [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3?! _:_./ _)" [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3! (_/:_)./ _)" [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3? (_/:_)./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3?! (_/:_)./ _)" [0, 0, 10] 10)
syntax
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
- "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>(_/\<in>_)./ _)" [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>(_/\<in>_)./ _)" [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
+ "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
translations
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
--- a/src/HOL/Transcendental.thy Thu Dec 21 22:56:51 2017 +0100
+++ b/src/HOL/Transcendental.thy Fri Dec 22 21:00:07 2017 +0000
@@ -2522,7 +2522,7 @@
by (simp add: powr_def exp_minus [symmetric])
lemma powr_minus_divide: "x powr (- a) = 1/(x powr a)"
- for x a :: real
+ for a x :: "'a::{ln,real_normed_field}"
by (simp add: divide_inverse powr_minus)
lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"