tagged
authorManuel Eberl <eberlm@in.tum.de>
Tue Jul 17 12:23:37 2018 +0200 (12 months ago)
changeset 6865116d98ef49a2c
parent 68650 7538b5f301ea
child 68653 5a5146c3a35b
tagged
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Analysis/Infinite_Set_Sum.thy
src/HOL/Analysis/Jordan_Curve.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 18 17:01:12 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jul 17 12:23:37 2018 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    imports Topology_Euclidean_Space Complex_Transcendental
     1.5  begin
     1.6  
     1.7 -subsection\<open>Preliminaries\<close>
     1.8 +subsection%unimportant \<open>Preliminaries\<close>
     1.9  
    1.10  lemma sum_le_prod:
    1.11    fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
    1.12 @@ -54,17 +54,18 @@
    1.13  
    1.14  subsection\<open>Definitions and basic properties\<close>
    1.15  
    1.16 -definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
    1.17 +definition%important raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
    1.18    where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
    1.19  
    1.20  text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
    1.21 -definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    1.22 +definition%important
    1.23 +  has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    1.24    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)"
    1.25  
    1.26 -definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
    1.27 +definition%important convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
    1.28    "convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p"
    1.29  
    1.30 -definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
    1.31 +definition%important prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
    1.32      (binder "\<Prod>" 10)
    1.33    where "prodinf f = (THE p. f has_prod p)"
    1.34  
    1.35 @@ -146,7 +147,7 @@
    1.36  
    1.37  subsection\<open>Absolutely convergent products\<close>
    1.38  
    1.39 -definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
    1.40 +definition%important abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
    1.41    "abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"
    1.42  
    1.43  lemma abs_convergent_prodI:
    1.44 @@ -220,7 +221,7 @@
    1.45      by (rule_tac x=0 in exI) auto
    1.46  qed
    1.47  
    1.48 -lemma convergent_prod_iff_convergent: 
    1.49 +lemma%important convergent_prod_iff_convergent: 
    1.50    fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    1.51    assumes "\<And>i. f i \<noteq> 0"
    1.52    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"
    1.53 @@ -367,7 +368,7 @@
    1.54    qed
    1.55  qed
    1.56  
    1.57 -lemma abs_convergent_prod_conv_summable:
    1.58 +theorem abs_convergent_prod_conv_summable:
    1.59    fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"
    1.60    shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>i. norm (f i - 1))"
    1.61    by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)
    1.62 @@ -396,6 +397,8 @@
    1.63    thus ?thesis by eventually_elim auto
    1.64  qed
    1.65  
    1.66 +subsection%unimportant \<open>Ignoring initial segments\<close>
    1.67 +
    1.68  lemma convergent_prod_offset:
    1.69    assumes "convergent_prod (\<lambda>n. f (n + m))"  
    1.70    shows   "convergent_prod f"
    1.71 @@ -411,7 +414,6 @@
    1.72    shows   "abs_convergent_prod f"
    1.73    using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)
    1.74  
    1.75 -subsection\<open>Ignoring initial segments\<close>
    1.76  
    1.77  lemma raw_has_prod_ignore_initial_segment:
    1.78    fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
    1.79 @@ -447,7 +449,7 @@
    1.80      using raw_has_prod_def that by blast 
    1.81  qed
    1.82  
    1.83 -corollary convergent_prod_ignore_initial_segment:
    1.84 +corollary%unimportant convergent_prod_ignore_initial_segment:
    1.85    fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
    1.86    assumes "convergent_prod f"
    1.87    shows   "convergent_prod (\<lambda>n. f (n + m))"
    1.88 @@ -458,20 +460,22 @@
    1.89    apply (auto simp add: raw_has_prod_def add_ac)
    1.90    done
    1.91  
    1.92 -corollary convergent_prod_ignore_nonzero_segment:
    1.93 +corollary%unimportant convergent_prod_ignore_nonzero_segment:
    1.94    fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
    1.95    assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
    1.96    shows "\<exists>p. raw_has_prod f M p"
    1.97    using convergent_prod_ignore_initial_segment [OF f]
    1.98    by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))
    1.99  
   1.100 -corollary abs_convergent_prod_ignore_initial_segment:
   1.101 +corollary%unimportant abs_convergent_prod_ignore_initial_segment:
   1.102    assumes "abs_convergent_prod f"
   1.103    shows   "abs_convergent_prod (\<lambda>n. f (n + m))"
   1.104    using assms unfolding abs_convergent_prod_def 
   1.105    by (rule convergent_prod_ignore_initial_segment)
   1.106  
   1.107 -lemma abs_convergent_prod_imp_convergent_prod:
   1.108 +subsection\<open>More elementary properties\<close>
   1.109 +
   1.110 +theorem abs_convergent_prod_imp_convergent_prod:
   1.111    fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"
   1.112    assumes "abs_convergent_prod f"
   1.113    shows   "convergent_prod f"
   1.114 @@ -599,8 +603,6 @@
   1.115    with L show ?thesis by (auto simp: prod_defs)
   1.116  qed
   1.117  
   1.118 -subsection\<open>More elementary properties\<close>
   1.119 -
   1.120  lemma raw_has_prod_cases:
   1.121    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   1.122    assumes "raw_has_prod f M p"
   1.123 @@ -758,7 +760,7 @@
   1.124    qed
   1.125  qed
   1.126  
   1.127 -corollary has_prod_0:
   1.128 +corollary%unimportant has_prod_0:
   1.129    fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
   1.130    assumes "\<And>n. f n = 1"
   1.131    shows "f has_prod 1"
   1.132 @@ -851,7 +853,7 @@
   1.133    by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent 
   1.134        convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
   1.135  
   1.136 -lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
   1.137 +theorem has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
   1.138  proof
   1.139    assume "f has_prod x"
   1.140    then show "convergent_prod f \<and> prodinf f = x"
   1.141 @@ -871,7 +873,7 @@
   1.142  
   1.143  end
   1.144  
   1.145 -subsection \<open>Infinite products on ordered, topological monoids\<close>
   1.146 +subsection%unimportant \<open>Infinite products on ordered topological monoids\<close>
   1.147  
   1.148  lemma LIMSEQ_prod_0: 
   1.149    fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
   1.150 @@ -1072,7 +1074,7 @@
   1.151    using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast
   1.152  
   1.153  
   1.154 -subsection \<open>Infinite products on topological spaces\<close>
   1.155 +subsection%unimportant \<open>Infinite products on topological spaces\<close>
   1.156  
   1.157  context
   1.158    fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
   1.159 @@ -1173,7 +1175,7 @@
   1.160  
   1.161  end
   1.162  
   1.163 -subsection \<open>Infinite summability on real normed fields\<close>
   1.164 +subsection%unimportant \<open>Infinite summability on real normed fields\<close>
   1.165  
   1.166  context
   1.167    fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
   1.168 @@ -1328,7 +1330,7 @@
   1.169      by (simp add: ac_simps)
   1.170  qed
   1.171  
   1.172 -corollary has_prod_iff_shift':
   1.173 +corollary%unimportant has_prod_iff_shift':
   1.174    assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
   1.175    shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a"
   1.176    by (simp add: assms has_prod_iff_shift)
   1.177 @@ -1430,7 +1432,7 @@
   1.178  
   1.179  end
   1.180  
   1.181 -lemma convergent_prod_iff_summable_real:
   1.182 +theorem convergent_prod_iff_summable_real:
   1.183    fixes a :: "nat \<Rightarrow> real"
   1.184    assumes "\<And>n. a n > 0"
   1.185    shows "convergent_prod (\<lambda>k. 1 + a k) \<longleftrightarrow> summable a" (is "?lhs = ?rhs")
   1.186 @@ -1556,7 +1558,7 @@
   1.187    by (simp add: "0" f less_0_prodinf suminf_ln_real)
   1.188  
   1.189  
   1.190 -lemma Ln_prodinf_complex:
   1.191 +theorem Ln_prodinf_complex:
   1.192    fixes z :: "nat \<Rightarrow> complex"
   1.193    assumes z: "\<And>j. z j \<noteq> 0" and \<xi>: "\<xi> \<noteq> 0"
   1.194    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")
   1.195 @@ -1769,7 +1771,7 @@
   1.196    using convergent_prod_def assms convergent_prod_iff_summable_complex by blast
   1.197  
   1.198  
   1.199 -subsection\<open>Embeddings from the reals into some complete real normed field\<close>
   1.200 +subsection%unimportant \<open>Embeddings from the reals into some complete real normed field\<close>
   1.201  
   1.202  lemma tendsto_eq_of_real_lim:
   1.203    assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
     2.1 --- a/src/HOL/Analysis/Infinite_Set_Sum.thy	Wed Jul 18 17:01:12 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Tue Jul 17 12:23:37 2018 +0200
     2.3 @@ -86,14 +86,14 @@
     2.4  
     2.5  
     2.6  
     2.7 -definition abs_summable_on ::
     2.8 +definition%important abs_summable_on ::
     2.9      "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
    2.10      (infix "abs'_summable'_on" 50)
    2.11   where
    2.12     "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
    2.13  
    2.14  
    2.15 -definition infsetsum ::
    2.16 +definition%important infsetsum ::
    2.17      "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b"
    2.18   where
    2.19     "infsetsum f A = lebesgue_integral (count_space A) f"
    2.20 @@ -553,7 +553,7 @@
    2.21         (insert assms, auto simp: bij_betw_def)    
    2.22  qed
    2.23  
    2.24 -lemma infsetsum_reindex:
    2.25 +theorem infsetsum_reindex:
    2.26    assumes "inj_on g A"
    2.27    shows   "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A"
    2.28    by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms)
    2.29 @@ -607,7 +607,7 @@
    2.30    unfolding abs_summable_on_def infsetsum_def
    2.31    by (rule Bochner_Integration.integral_norm_bound)
    2.32  
    2.33 -lemma infsetsum_Sigma:
    2.34 +theorem infsetsum_Sigma:
    2.35    fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set"
    2.36    assumes [simp]: "countable A" and "\<And>i. countable (B i)"
    2.37    assumes summable: "f abs_summable_on (Sigma A B)"
    2.38 @@ -692,7 +692,7 @@
    2.39    finally show ?thesis .
    2.40  qed
    2.41  
    2.42 -lemma abs_summable_on_Sigma_iff:
    2.43 +theorem abs_summable_on_Sigma_iff:
    2.44    assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
    2.45    shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
    2.46               (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
    2.47 @@ -783,7 +783,7 @@
    2.48    by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]]
    2.49          norm_infsetsum_bound)
    2.50  
    2.51 -lemma infsetsum_prod_PiE:
    2.52 +theorem infsetsum_prod_PiE:
    2.53    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
    2.54    assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
    2.55    assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
     3.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Wed Jul 18 17:01:12 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Jul 17 12:23:37 2018 +0200
     3.3 @@ -6,7 +6,6 @@
     3.4  
     3.5  theory Jordan_Curve
     3.6    imports Arcwise_Connected Further_Topology
     3.7 -
     3.8  begin
     3.9  
    3.10  subsection\<open>Janiszewski's theorem\<close>
    3.11 @@ -114,8 +113,8 @@
    3.12  
    3.13  
    3.14  theorem Janiszewski:
    3.15 -  fixes a b::complex
    3.16 -  assumes "compact S" "closed T" and conST: "connected(S \<inter> T)"
    3.17 +  fixes a b :: complex
    3.18 +  assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
    3.19        and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
    3.20      shows "connected_component (- (S \<union> T)) a b"
    3.21  proof -
    3.22 @@ -166,6 +165,7 @@
    3.23  using Janiszewski [OF ST]
    3.24  by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
    3.25  
    3.26 +
    3.27  subsection\<open>The Jordan Curve theorem\<close>
    3.28  
    3.29  lemma exists_double_arc:
    3.30 @@ -219,7 +219,7 @@
    3.31  qed
    3.32  
    3.33  
    3.34 -theorem Jordan_curve:
    3.35 +theorem%unimportant Jordan_curve:
    3.36    fixes c :: "real \<Rightarrow> complex"
    3.37    assumes "simple_path c" and loop: "pathfinish c = pathstart c"
    3.38    obtains inner outer where
    3.39 @@ -389,7 +389,7 @@
    3.40  qed
    3.41  
    3.42  
    3.43 -corollary Jordan_disconnected:
    3.44 +corollary%unimportant Jordan_disconnected:
    3.45    fixes c :: "real \<Rightarrow> complex"
    3.46    assumes "simple_path c" "pathfinish c = pathstart c"
    3.47      shows "\<not> connected(- path_image c)"