# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1531823017 -7200
# Node ID 16d98ef49a2cadd8f6cfd75561c23a453cd0929a
# Parent  7538b5f301ea2d0540ed58affa286a64dce4c713
tagged

diff -r 7538b5f301ea -r 16d98ef49a2c src/HOL/Analysis/Infinite_Products.thy
--- 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"
diff -r 7538b5f301ea -r 16d98ef49a2c src/HOL/Analysis/Infinite_Set_Sum.thy
--- 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"
diff -r 7538b5f301ea -r 16d98ef49a2c src/HOL/Analysis/Jordan_Curve.thy
--- 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)"