author Manuel Eberl Tue, 17 Jul 2018 12:23:37 +0200 changeset 68651 16d98ef49a2c parent 68650 7538b5f301ea child 68653 5a5146c3a35b
tagged
--- a/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 18 17:01:12 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jul 17 12:23:37 2018 +0200
@@ -9,7 +9,7 @@
imports Topology_Euclidean_Space Complex_Transcendental
begin

-subsection\<open>Preliminaries\<close>
+subsection%unimportant \<open>Preliminaries\<close>

lemma sum_le_prod:
fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
@@ -54,17 +54,18 @@

subsection\<open>Definitions and basic properties\<close>

-definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
+definition%important raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"

text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
-definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
+definition%important
+  has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"

-definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
+definition%important convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
"convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p"

-definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
+definition%important prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
(binder "\<Prod>" 10)
where "prodinf f = (THE p. f has_prod p)"

@@ -146,7 +147,7 @@

subsection\<open>Absolutely convergent products\<close>

-definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
+definition%important abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
"abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"

lemma abs_convergent_prodI:
@@ -220,7 +221,7 @@
by (rule_tac x=0 in exI) auto
qed

-lemma convergent_prod_iff_convergent:
+lemma%important 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"
@@ -367,7 +368,7 @@
qed
qed

-lemma abs_convergent_prod_conv_summable:
+theorem abs_convergent_prod_conv_summable:
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"
shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i - 1))"
by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)
@@ -396,6 +397,8 @@
thus ?thesis by eventually_elim auto
qed

+subsection%unimportant \<open>Ignoring initial segments\<close>
+
lemma convergent_prod_offset:
assumes "convergent_prod (\<lambda>n. f (n + m))"
shows   "convergent_prod f"
@@ -411,7 +414,6 @@
shows   "abs_convergent_prod f"
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)

-subsection\<open>Ignoring initial segments\<close>

lemma raw_has_prod_ignore_initial_segment:
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
@@ -447,7 +449,7 @@
using raw_has_prod_def that by blast
qed

-corollary convergent_prod_ignore_initial_segment:
+corollary%unimportant convergent_prod_ignore_initial_segment:
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
assumes "convergent_prod f"
shows   "convergent_prod (\<lambda>n. f (n + m))"
@@ -458,20 +460,22 @@
apply (auto simp add: raw_has_prod_def add_ac)
done

-corollary convergent_prod_ignore_nonzero_segment:
+corollary%unimportant 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. raw_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:
+corollary%unimportant 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
by (rule convergent_prod_ignore_initial_segment)

-lemma abs_convergent_prod_imp_convergent_prod:
+subsection\<open>More elementary properties\<close>
+
+theorem abs_convergent_prod_imp_convergent_prod:
fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"
assumes "abs_convergent_prod f"
shows   "convergent_prod f"
@@ -599,8 +603,6 @@
with L show ?thesis by (auto simp: prod_defs)
qed

-subsection\<open>More elementary properties\<close>
-
lemma raw_has_prod_cases:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
assumes "raw_has_prod f M p"
@@ -758,7 +760,7 @@
qed
qed

-corollary has_prod_0:
+corollary%unimportant has_prod_0:
fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
assumes "\<And>n. f n = 1"
shows "f has_prod 1"
@@ -851,7 +853,7 @@
by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent
convergent_prod_to_zero_iff raw_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"
+theorem 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"
@@ -871,7 +873,7 @@

end

-subsection \<open>Infinite products on ordered, topological monoids\<close>
+subsection%unimportant \<open>Infinite products on ordered topological monoids\<close>

lemma LIMSEQ_prod_0:
fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
@@ -1072,7 +1074,7 @@
using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast

-subsection \<open>Infinite products on topological spaces\<close>
+subsection%unimportant \<open>Infinite products on topological spaces\<close>

context
fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
@@ -1173,7 +1175,7 @@

end

-subsection \<open>Infinite summability on real normed fields\<close>
+subsection%unimportant \<open>Infinite summability on real normed fields\<close>

context
fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
@@ -1328,7 +1330,7 @@
by (simp add: ac_simps)
qed

-corollary has_prod_iff_shift':
+corollary%unimportant has_prod_iff_shift':
assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a"
by (simp add: assms has_prod_iff_shift)
@@ -1430,7 +1432,7 @@

end

-lemma convergent_prod_iff_summable_real:
+theorem convergent_prod_iff_summable_real:
fixes a :: "nat \<Rightarrow> real"
assumes "\<And>n. a n > 0"
shows "convergent_prod (\<lambda>k. 1 + a k) \<longleftrightarrow> summable a" (is "?lhs = ?rhs")
@@ -1556,7 +1558,7 @@
by (simp add: "0" f less_0_prodinf suminf_ln_real)

-lemma Ln_prodinf_complex:
+theorem Ln_prodinf_complex:
fixes z :: "nat \<Rightarrow> complex"
assumes z: "\<And>j. z j \<noteq> 0" and \<xi>: "\<xi> \<noteq> 0"
shows "((\<lambda>n. \<Prod>j\<le>n. z j) \<longlonglongrightarrow> \<xi>) \<longleftrightarrow> (\<exists>k. (\<lambda>n. (\<Sum>j\<le>n. Ln (z j))) \<longlonglongrightarrow> Ln \<xi> + of_int k * (of_real(2*pi) * \<i>))" (is "?lhs = ?rhs")
@@ -1769,7 +1771,7 @@
using convergent_prod_def assms convergent_prod_iff_summable_complex by blast

-subsection\<open>Embeddings from the reals into some complete real normed field\<close>
+subsection%unimportant \<open>Embeddings from the reals into some complete real normed field\<close>

lemma tendsto_eq_of_real_lim:
assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Jul 18 17:01:12 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Tue Jul 17 12:23:37 2018 +0200
@@ -86,14 +86,14 @@

-definition abs_summable_on ::
+definition%important abs_summable_on ::
"('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
(infix "abs'_summable'_on" 50)
where
"f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"

-definition infsetsum ::
+definition%important infsetsum ::
"('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
where
"infsetsum f A = lebesgue_integral (count_space A) f"
@@ -553,7 +553,7 @@
(insert assms, auto simp: bij_betw_def)
qed

-lemma infsetsum_reindex:
+theorem infsetsum_reindex:
assumes "inj_on g A"
shows   "infsetsum f (g  A) = infsetsum (\<lambda>x. f (g x)) A"
by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
@@ -607,7 +607,7 @@
unfolding abs_summable_on_def infsetsum_def
by (rule Bochner_Integration.integral_norm_bound)

-lemma infsetsum_Sigma:
+theorem infsetsum_Sigma:
fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
assumes [simp]: "countable A" and "\<And>i. countable (B i)"
assumes summable: "f abs_summable_on (Sigma A B)"
@@ -692,7 +692,7 @@
finally show ?thesis .
qed

-lemma abs_summable_on_Sigma_iff:
+theorem abs_summable_on_Sigma_iff:
assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
shows   "f abs_summable_on Sigma A B \<longleftrightarrow>
(\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
@@ -783,7 +783,7 @@
by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
norm_infsetsum_bound)

-lemma infsetsum_prod_PiE:
+theorem infsetsum_prod_PiE:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
--- a/src/HOL/Analysis/Jordan_Curve.thy	Wed Jul 18 17:01:12 2018 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Jul 17 12:23:37 2018 +0200
@@ -6,7 +6,6 @@

theory Jordan_Curve
imports Arcwise_Connected Further_Topology
-
begin

subsection\<open>Janiszewski's theorem\<close>
@@ -114,8 +113,8 @@

theorem Janiszewski:
-  fixes a b::complex
-  assumes "compact S" "closed T" and conST: "connected(S \<inter> T)"
+  fixes a b :: complex
+  assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
shows "connected_component (- (S \<union> T)) a b"
proof -
@@ -166,6 +165,7 @@
using Janiszewski [OF ST]
by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)

+
subsection\<open>The Jordan Curve theorem\<close>

lemma exists_double_arc:
@@ -219,7 +219,7 @@
qed

-theorem Jordan_curve:
+theorem%unimportant Jordan_curve:
fixes c :: "real \<Rightarrow> complex"
assumes "simple_path c" and loop: "pathfinish c = pathstart c"
obtains inner outer where
@@ -389,7 +389,7 @@
qed

-corollary Jordan_disconnected:
+corollary%unimportant Jordan_disconnected:
fixes c :: "real \<Rightarrow> complex"
assumes "simple_path c" "pathfinish c = pathstart c"
shows "\<not> connected(- path_image c)"`