src/HOL/Limits.thy
author hoelzl
Tue, 09 Apr 2013 14:04:41 +0200
changeset 51641 cd05e9fcc63d
parent 51531 f415febf4234
child 51642 400ec5ae7f8f
permissions -rw-r--r--
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51526
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     1
(*  Title:      Limits.thy
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     2
    Author:     Brian Huffman
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     3
    Author:     Jacques D. Fleuriot, University of Cambridge
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     4
    Author:     Lawrence C Paulson
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     5
    Author:     Jeremy Avigad
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     6
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
     7
*)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
     8
51526
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
     9
header {* Limits on Real Vector Spaces *}
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
    10
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
    11
theory Limits
51524
7cb5ac44ca9e rename RealVector.thy to Real_Vector_Spaces.thy
hoelzl
parents: 51478
diff changeset
    12
imports Real_Vector_Spaces
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
    13
begin
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
    14
51526
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
    15
subsection {* Filter going to infinity norm *}
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
    16
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    17
definition at_infinity :: "'a::real_normed_vector filter" where
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    18
  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    19
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    20
lemma eventually_at_infinity:
50325
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    21
  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    22
unfolding at_infinity_def
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    23
proof (rule eventually_Abs_filter, rule is_filter.intro)
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    24
  fix P Q :: "'a \<Rightarrow> bool"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    25
  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    26
  then obtain r s where
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    27
    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    28
  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    29
  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
    30
qed auto
31392
69570155ddf8 replace filters with filter bases
huffman
parents: 31357
diff changeset
    31
50325
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    32
lemma at_infinity_eq_at_top_bot:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    33
  "(at_infinity \<Colon> real filter) = sup at_top at_bot"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    34
  unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    35
proof (intro arg_cong[where f=Abs_filter] ext iffI)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    36
  fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    37
  then guess r ..
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    38
  then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    39
  then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    40
next
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    41
  fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    42
  then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    43
  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    44
    by (intro exI[of _ "max p (-q)"])
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    45
       (auto simp: abs_real_def)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    46
qed
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    47
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    48
lemma at_top_le_at_infinity:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    49
  "at_top \<le> (at_infinity :: real filter)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    50
  unfolding at_infinity_eq_at_top_bot by simp
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    51
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    52
lemma at_bot_le_at_infinity:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    53
  "at_bot \<le> (at_infinity :: real filter)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    54
  unfolding at_infinity_eq_at_top_bot by simp
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
    55
51531
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    56
subsubsection {* Boundedness *}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    57
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    58
definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    59
  Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    60
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    61
abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    62
  "Bseq X \<equiv> Bfun X sequentially"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    63
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    64
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" ..
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    65
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    66
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    67
  unfolding Bfun_metric_def by (subst eventually_sequentially_seg)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    68
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    69
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
    70
  unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    71
51474
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    72
lemma Bfun_def:
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    73
  "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    74
  unfolding Bfun_metric_def norm_conv_dist
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    75
proof safe
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    76
  fix y K assume "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F"
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    77
  moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F"
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    78
    by (intro always_eventually) (metis dist_commute dist_triangle)
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    79
  with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F"
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    80
    by eventually_elim auto
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    81
  with `0 < K` show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    82
    by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51472
diff changeset
    83
qed auto
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    84
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
    85
lemma BfunI:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
    86
  assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    87
unfolding Bfun_def
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    88
proof (intro exI conjI allI)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    89
  show "0 < max K 1" by simp
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    90
next
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
    91
  show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    92
    using K by (rule eventually_elim1, simp)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    93
qed
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    94
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    95
lemma BfunE:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
    96
  assumes "Bfun f F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
    97
  obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    98
using assms unfolding Bfun_def by fast
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
    99
51531
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   100
lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   101
  unfolding Cauchy_def Bfun_metric_def eventually_sequentially
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   102
  apply (erule_tac x=1 in allE)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   103
  apply simp
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   104
  apply safe
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   105
  apply (rule_tac x="X M" in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   106
  apply (rule_tac x=1 in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   107
  apply (erule_tac x=M in allE)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   108
  apply simp
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   109
  apply (rule_tac x=M in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   110
  apply (auto simp: dist_commute)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   111
  done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   112
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   113
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   114
subsubsection {* Bounded Sequences *}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   115
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   116
lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   117
  by (intro BfunI) (auto simp: eventually_sequentially)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   118
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   119
lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   120
  by (intro BfunI) (auto simp: eventually_sequentially)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   121
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   122
lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   123
  unfolding Bfun_def eventually_sequentially
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   124
proof safe
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   125
  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   126
  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   127
    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   128
       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   129
qed auto
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   130
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   131
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   132
unfolding Bseq_def by auto
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   133
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   134
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   135
by (simp add: Bseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   136
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   137
lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   138
by (auto simp add: Bseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   139
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   140
lemma lemma_NBseq_def:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   141
  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   142
proof safe
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   143
  fix K :: real
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   144
  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   145
  then have "K \<le> real (Suc n)" by auto
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   146
  moreover assume "\<forall>m. norm (X m) \<le> K"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   147
  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   148
    by (blast intro: order_trans)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   149
  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   150
qed (force simp add: real_of_nat_Suc)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   151
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   152
text{* alternative definition for Bseq *}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   153
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   154
apply (simp add: Bseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   155
apply (simp (no_asm) add: lemma_NBseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   156
done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   157
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   158
lemma lemma_NBseq_def2:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   159
     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   160
apply (subst lemma_NBseq_def, auto)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   161
apply (rule_tac x = "Suc N" in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   162
apply (rule_tac [2] x = N in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   163
apply (auto simp add: real_of_nat_Suc)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   164
 prefer 2 apply (blast intro: order_less_imp_le)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   165
apply (drule_tac x = n in spec, simp)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   166
done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   167
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   168
(* yet another definition for Bseq *)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   169
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   170
by (simp add: Bseq_def lemma_NBseq_def2)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   171
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   172
subsubsection{*A Few More Equivalence Theorems for Boundedness*}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   173
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   174
text{*alternative formulation for boundedness*}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   175
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   176
apply (unfold Bseq_def, safe)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   177
apply (rule_tac [2] x = "k + norm x" in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   178
apply (rule_tac x = K in exI, simp)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   179
apply (rule exI [where x = 0], auto)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   180
apply (erule order_less_le_trans, simp)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   181
apply (drule_tac x=n in spec, fold diff_minus)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   182
apply (drule order_trans [OF norm_triangle_ineq2])
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   183
apply simp
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   184
done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   185
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   186
text{*alternative formulation for boundedness*}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   187
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   188
apply safe
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   189
apply (simp add: Bseq_def, safe)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   190
apply (rule_tac x = "K + norm (X N)" in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   191
apply auto
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   192
apply (erule order_less_le_trans, simp)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   193
apply (rule_tac x = N in exI, safe)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   194
apply (drule_tac x = n in spec)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   195
apply (rule order_trans [OF norm_triangle_ineq], simp)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   196
apply (auto simp add: Bseq_iff2)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   197
done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   198
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   199
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   200
apply (simp add: Bseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   201
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   202
apply (drule_tac x = n in spec, arith)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   203
done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   204
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   205
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   206
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   207
lemma Bseq_isUb:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   208
  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   209
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   210
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   211
text{* Use completeness of reals (supremum property)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   212
   to show that any bounded sequence has a least upper bound*}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   213
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   214
lemma Bseq_isLub:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   215
  "!!(X::nat=>real). Bseq X ==>
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   216
   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   217
by (blast intro: reals_complete Bseq_isUb)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   218
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   219
lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   220
  by (simp add: Bseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   221
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   222
lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   223
  apply (simp add: subset_eq)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   224
  apply (rule BseqI'[where K="max (norm a) (norm b)"])
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   225
  apply (erule_tac x=n in allE)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   226
  apply auto
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   227
  done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   228
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   229
lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   230
  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   231
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   232
lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   233
  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   234
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   235
subsection {* Bounded Monotonic Sequences *}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   236
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   237
subsubsection{*A Bounded and Monotonic Sequence Converges*}
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   238
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   239
(* TODO: delete *)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   240
(* FIXME: one use in NSA/HSEQ.thy *)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   241
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   242
  apply (rule_tac x="X m" in exI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   243
  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   244
  unfolding eventually_sequentially
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   245
  apply blast
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   246
  done
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   247
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   248
subsection {* Convergence to Zero *}
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   249
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   250
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   251
  where "Zfun f F = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) F)"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   252
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   253
lemma ZfunI:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   254
  "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F) \<Longrightarrow> Zfun f F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   255
  unfolding Zfun_def by simp
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   256
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   257
lemma ZfunD:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   258
  "\<lbrakk>Zfun f F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   259
  unfolding Zfun_def by simp
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   260
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   261
lemma Zfun_ssubst:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   262
  "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun f F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   263
  unfolding Zfun_def by (auto elim!: eventually_rev_mp)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   264
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   265
lemma Zfun_zero: "Zfun (\<lambda>x. 0) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   266
  unfolding Zfun_def by simp
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   267
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   268
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) F = Zfun (\<lambda>x. f x) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   269
  unfolding Zfun_def by simp
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   270
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   271
lemma Zfun_imp_Zfun:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   272
  assumes f: "Zfun f F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   273
  assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   274
  shows "Zfun (\<lambda>x. g x) F"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   275
proof (cases)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   276
  assume K: "0 < K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   277
  show ?thesis
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   278
  proof (rule ZfunI)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   279
    fix r::real assume "0 < r"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   280
    hence "0 < r / K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   281
      using K by (rule divide_pos_pos)
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   282
    then have "eventually (\<lambda>x. norm (f x) < r / K) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   283
      using ZfunD [OF f] by fast
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   284
    with g show "eventually (\<lambda>x. norm (g x) < r) F"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   285
    proof eventually_elim
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   286
      case (elim x)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   287
      hence "norm (f x) * K < r"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   288
        by (simp add: pos_less_divide_eq K)
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   289
      thus ?case
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   290
        by (simp add: order_le_less_trans [OF elim(1)])
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   291
    qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   292
  qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   293
next
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   294
  assume "\<not> 0 < K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   295
  hence K: "K \<le> 0" by (simp only: not_less)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   296
  show ?thesis
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   297
  proof (rule ZfunI)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   298
    fix r :: real
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   299
    assume "0 < r"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   300
    from g show "eventually (\<lambda>x. norm (g x) < r) F"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   301
    proof eventually_elim
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   302
      case (elim x)
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   303
      also have "norm (f x) * K \<le> norm (f x) * 0"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   304
        using K norm_ge_zero by (rule mult_left_mono)
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   305
      finally show ?case
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   306
        using `0 < r` by simp
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   307
    qed
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   308
  qed
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   309
qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   310
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   311
lemma Zfun_le: "\<lbrakk>Zfun g F; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   312
  by (erule_tac K="1" in Zfun_imp_Zfun, simp)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   313
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   314
lemma Zfun_add:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   315
  assumes f: "Zfun f F" and g: "Zfun g F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   316
  shows "Zfun (\<lambda>x. f x + g x) F"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   317
proof (rule ZfunI)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   318
  fix r::real assume "0 < r"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   319
  hence r: "0 < r / 2" by simp
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   320
  have "eventually (\<lambda>x. norm (f x) < r/2) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   321
    using f r by (rule ZfunD)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   322
  moreover
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   323
  have "eventually (\<lambda>x. norm (g x) < r/2) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   324
    using g r by (rule ZfunD)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   325
  ultimately
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   326
  show "eventually (\<lambda>x. norm (f x + g x) < r) F"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   327
  proof eventually_elim
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   328
    case (elim x)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   329
    have "norm (f x + g x) \<le> norm (f x) + norm (g x)"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   330
      by (rule norm_triangle_ineq)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   331
    also have "\<dots> < r/2 + r/2"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   332
      using elim by (rule add_strict_mono)
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   333
    finally show ?case
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   334
      by simp
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   335
  qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   336
qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   337
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   338
lemma Zfun_minus: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. - f x) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   339
  unfolding Zfun_def by simp
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   340
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   341
lemma Zfun_diff: "\<lbrakk>Zfun f F; Zfun g F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   342
  by (simp only: diff_minus Zfun_add Zfun_minus)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   343
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   344
lemma (in bounded_linear) Zfun:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   345
  assumes g: "Zfun g F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   346
  shows "Zfun (\<lambda>x. f (g x)) F"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   347
proof -
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   348
  obtain K where "\<And>x. norm (f x) \<le> norm x * K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   349
    using bounded by fast
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   350
  then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   351
    by simp
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   352
  with g show ?thesis
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   353
    by (rule Zfun_imp_Zfun)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   354
qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   355
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   356
lemma (in bounded_bilinear) Zfun:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   357
  assumes f: "Zfun f F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   358
  assumes g: "Zfun g F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   359
  shows "Zfun (\<lambda>x. f x ** g x) F"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   360
proof (rule ZfunI)
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   361
  fix r::real assume r: "0 < r"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   362
  obtain K where K: "0 < K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   363
    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   364
    using pos_bounded by fast
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   365
  from K have K': "0 < inverse K"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   366
    by (rule positive_imp_inverse_positive)
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   367
  have "eventually (\<lambda>x. norm (f x) < r) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   368
    using f r by (rule ZfunD)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   369
  moreover
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   370
  have "eventually (\<lambda>x. norm (g x) < inverse K) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   371
    using g K' by (rule ZfunD)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   372
  ultimately
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   373
  show "eventually (\<lambda>x. norm (f x ** g x) < r) F"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   374
  proof eventually_elim
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   375
    case (elim x)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   376
    have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   377
      by (rule norm_le)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   378
    also have "norm (f x) * norm (g x) * K < r * inverse K * K"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   379
      by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   380
    also from K have "r * inverse K * K = r"
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   381
      by simp
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   382
    finally show ?case .
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   383
  qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   384
qed
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   385
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   386
lemma (in bounded_bilinear) Zfun_left:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   387
  "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. f x ** a) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   388
  by (rule bounded_linear_left [THEN bounded_linear.Zfun])
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   389
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   390
lemma (in bounded_bilinear) Zfun_right:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   391
  "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   392
  by (rule bounded_linear_right [THEN bounded_linear.Zfun])
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   393
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   394
lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   395
lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   396
lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult]
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   397
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   398
lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   399
  by (simp only: tendsto_iff Zfun_def dist_norm)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   400
44205
18da2a87421c generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents: 44195
diff changeset
   401
subsubsection {* Distance and norms *}
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   402
51531
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   403
lemma tendsto_dist [tendsto_intros]:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   404
  fixes l m :: "'a :: metric_space"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   405
  assumes f: "(f ---> l) F" and g: "(g ---> m) F"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   406
  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   407
proof (rule tendstoI)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   408
  fix e :: real assume "0 < e"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   409
  hence e2: "0 < e/2" by simp
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   410
  from tendstoD [OF f e2] tendstoD [OF g e2]
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   411
  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   412
  proof (eventually_elim)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   413
    case (elim x)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   414
    then show "dist (dist (f x) (g x)) (dist l m) < e"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   415
      unfolding dist_real_def
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   416
      using dist_triangle2 [of "f x" "g x" "l"]
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   417
      using dist_triangle2 [of "g x" "l" "m"]
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   418
      using dist_triangle3 [of "l" "m" "f x"]
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   419
      using dist_triangle [of "f x" "m" "g x"]
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   420
      by arith
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   421
  qed
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   422
qed
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   423
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   424
lemma continuous_dist[continuous_intros]:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   425
  fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   426
  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   427
  unfolding continuous_def by (rule tendsto_dist)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   428
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   429
lemma continuous_on_dist[continuous_on_intros]:
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   430
  fixes f g :: "_ \<Rightarrow> 'a :: metric_space"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   431
  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))"
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   432
  unfolding continuous_on_def by (auto intro: tendsto_dist)
f415febf4234 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents: 51529
diff changeset
   433
31565
da5a5589418e theorem attribute [tendsto_intros]
huffman
parents: 31492
diff changeset
   434
lemma tendsto_norm [tendsto_intros]:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   435
  "(f ---> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   436
  unfolding norm_conv_dist by (intro tendsto_intros)
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   437
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   438
lemma continuous_norm [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   439
  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   440
  unfolding continuous_def by (rule tendsto_norm)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   441
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   442
lemma continuous_on_norm [continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   443
  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   444
  unfolding continuous_on_def by (auto intro: tendsto_norm)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   445
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   446
lemma tendsto_norm_zero:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   447
  "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   448
  by (drule tendsto_norm, simp)
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   449
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   450
lemma tendsto_norm_zero_cancel:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   451
  "((\<lambda>x. norm (f x)) ---> 0) F \<Longrightarrow> (f ---> 0) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   452
  unfolding tendsto_iff dist_norm by simp
36662
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   453
621122eeb138 generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents: 36656
diff changeset
   454
lemma tendsto_norm_zero_iff:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   455
  "((\<lambda>x. norm (f x)) ---> 0) F \<longleftrightarrow> (f ---> 0) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   456
  unfolding tendsto_iff dist_norm by simp
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   457
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   458
lemma tendsto_rabs [tendsto_intros]:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   459
  "(f ---> (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> \<bar>l\<bar>) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   460
  by (fold real_norm_def, rule tendsto_norm)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   461
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   462
lemma continuous_rabs [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   463
  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   464
  unfolding real_norm_def[symmetric] by (rule continuous_norm)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   465
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   466
lemma continuous_on_rabs [continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   467
  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   468
  unfolding real_norm_def[symmetric] by (rule continuous_on_norm)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   469
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   470
lemma tendsto_rabs_zero:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   471
  "(f ---> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   472
  by (fold real_norm_def, rule tendsto_norm_zero)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   473
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   474
lemma tendsto_rabs_zero_cancel:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   475
  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) F \<Longrightarrow> (f ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   476
  by (fold real_norm_def, rule tendsto_norm_zero_cancel)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   477
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   478
lemma tendsto_rabs_zero_iff:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   479
  "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) F \<longleftrightarrow> (f ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   480
  by (fold real_norm_def, rule tendsto_norm_zero_iff)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   481
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   482
subsubsection {* Addition and subtraction *}
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   483
31565
da5a5589418e theorem attribute [tendsto_intros]
huffman
parents: 31492
diff changeset
   484
lemma tendsto_add [tendsto_intros]:
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   485
  fixes a b :: "'a::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   486
  shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   487
  by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   488
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   489
lemma continuous_add [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   490
  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   491
  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   492
  unfolding continuous_def by (rule tendsto_add)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   493
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   494
lemma continuous_on_add [continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   495
  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   496
  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   497
  unfolding continuous_on_def by (auto intro: tendsto_add)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   498
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   499
lemma tendsto_add_zero:
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   500
  fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   501
  shows "\<lbrakk>(f ---> 0) F; (g ---> 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   502
  by (drule (1) tendsto_add, simp)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   503
31565
da5a5589418e theorem attribute [tendsto_intros]
huffman
parents: 31492
diff changeset
   504
lemma tendsto_minus [tendsto_intros]:
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   505
  fixes a :: "'a::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   506
  shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   507
  by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   508
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   509
lemma continuous_minus [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   510
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   511
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   512
  unfolding continuous_def by (rule tendsto_minus)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   513
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   514
lemma continuous_on_minus [continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   515
  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   516
  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   517
  unfolding continuous_on_def by (auto intro: tendsto_minus)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   518
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   519
lemma tendsto_minus_cancel:
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   520
  fixes a :: "'a::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   521
  shows "((\<lambda>x. - f x) ---> - a) F \<Longrightarrow> (f ---> a) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   522
  by (drule tendsto_minus, simp)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   523
50330
d0b12171118e conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents: 50327
diff changeset
   524
lemma tendsto_minus_cancel_left:
d0b12171118e conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents: 50327
diff changeset
   525
    "(f ---> - (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x. - f x) ---> y) F"
d0b12171118e conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents: 50327
diff changeset
   526
  using tendsto_minus_cancel[of f "- y" F]  tendsto_minus[of f "- y" F]
d0b12171118e conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents: 50327
diff changeset
   527
  by auto
d0b12171118e conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents: 50327
diff changeset
   528
31565
da5a5589418e theorem attribute [tendsto_intros]
huffman
parents: 31492
diff changeset
   529
lemma tendsto_diff [tendsto_intros]:
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   530
  fixes a b :: "'a::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   531
  shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   532
  by (simp add: diff_minus tendsto_add tendsto_minus)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   533
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   534
lemma continuous_diff [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   535
  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   536
  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   537
  unfolding continuous_def by (rule tendsto_diff)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   538
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   539
lemma continuous_on_diff [continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   540
  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   541
  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   542
  unfolding continuous_on_def by (auto intro: tendsto_diff)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   543
31588
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   544
lemma tendsto_setsum [tendsto_intros]:
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   545
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   546
  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   547
  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) F"
31588
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   548
proof (cases "finite S")
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   549
  assume "finite S" thus ?thesis using assms
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   550
    by (induct, simp add: tendsto_const, simp add: tendsto_add)
31588
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   551
next
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   552
  assume "\<not> finite S" thus ?thesis
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   553
    by (simp add: tendsto_const)
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   554
qed
2651f172c38b add lemma tendsto_setsum
huffman
parents: 31565
diff changeset
   555
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   556
lemma continuous_setsum [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   557
  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   558
  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   559
  unfolding continuous_def by (rule tendsto_setsum)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   560
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   561
lemma continuous_on_setsum [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   562
  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   563
  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Sum>i\<in>S. f i x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   564
  unfolding continuous_on_def by (auto intro: tendsto_setsum)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   565
50999
3de230ed0547 introduce order topology
hoelzl
parents: 50880
diff changeset
   566
lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
3de230ed0547 introduce order topology
hoelzl
parents: 50880
diff changeset
   567
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   568
subsubsection {* Linear operators and multiplication *}
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   569
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   570
lemma (in bounded_linear) tendsto:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   571
  "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   572
  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   573
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   574
lemma (in bounded_linear) continuous:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   575
  "continuous F g \<Longrightarrow> continuous F (\<lambda>x. f (g x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   576
  using tendsto[of g _ F] by (auto simp: continuous_def)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   577
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   578
lemma (in bounded_linear) continuous_on:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   579
  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   580
  using tendsto[of g] by (auto simp: continuous_on_def)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   581
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   582
lemma (in bounded_linear) tendsto_zero:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   583
  "(g ---> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   584
  by (drule tendsto, simp only: zero)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   585
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   586
lemma (in bounded_bilinear) tendsto:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   587
  "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   588
  by (simp only: tendsto_Zfun_iff prod_diff_prod
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   589
                 Zfun_add Zfun Zfun_left Zfun_right)
31349
2261c8781f73 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff changeset
   590
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   591
lemma (in bounded_bilinear) continuous:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   592
  "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ** g x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   593
  using tendsto[of f _ F g] by (auto simp: continuous_def)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   594
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   595
lemma (in bounded_bilinear) continuous_on:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   596
  "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   597
  using tendsto[of f _ _ g] by (auto simp: continuous_on_def)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   598
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   599
lemma (in bounded_bilinear) tendsto_zero:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   600
  assumes f: "(f ---> 0) F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   601
  assumes g: "(g ---> 0) F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   602
  shows "((\<lambda>x. f x ** g x) ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   603
  using tendsto [OF f g] by (simp add: zero_left)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   604
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   605
lemma (in bounded_bilinear) tendsto_left_zero:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   606
  "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. f x ** c) ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   607
  by (rule bounded_linear.tendsto_zero [OF bounded_linear_left])
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   608
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   609
lemma (in bounded_bilinear) tendsto_right_zero:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   610
  "(f ---> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) ---> 0) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   611
  by (rule bounded_linear.tendsto_zero [OF bounded_linear_right])
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   612
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   613
lemmas tendsto_of_real [tendsto_intros] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   614
  bounded_linear.tendsto [OF bounded_linear_of_real]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   615
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   616
lemmas tendsto_scaleR [tendsto_intros] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   617
  bounded_bilinear.tendsto [OF bounded_bilinear_scaleR]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   618
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   619
lemmas tendsto_mult [tendsto_intros] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   620
  bounded_bilinear.tendsto [OF bounded_bilinear_mult]
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   621
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   622
lemmas continuous_of_real [continuous_intros] =
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   623
  bounded_linear.continuous [OF bounded_linear_of_real]
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   624
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   625
lemmas continuous_scaleR [continuous_intros] =
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   626
  bounded_bilinear.continuous [OF bounded_bilinear_scaleR]
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   627
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   628
lemmas continuous_mult [continuous_intros] =
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   629
  bounded_bilinear.continuous [OF bounded_bilinear_mult]
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   630
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   631
lemmas continuous_on_of_real [continuous_on_intros] =
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   632
  bounded_linear.continuous_on [OF bounded_linear_of_real]
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   633
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   634
lemmas continuous_on_scaleR [continuous_on_intros] =
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   635
  bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR]
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   636
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   637
lemmas continuous_on_mult [continuous_on_intros] =
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   638
  bounded_bilinear.continuous_on [OF bounded_bilinear_mult]
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   639
44568
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   640
lemmas tendsto_mult_zero =
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   641
  bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult]
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   642
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   643
lemmas tendsto_mult_left_zero =
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   644
  bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult]
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   645
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   646
lemmas tendsto_mult_right_zero =
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   647
  bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
e6f291cb5810 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents: 44342
diff changeset
   648
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   649
lemma tendsto_power [tendsto_intros]:
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   650
  fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   651
  shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   652
  by (induct n) (simp_all add: tendsto_const tendsto_mult)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   653
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   654
lemma continuous_power [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   655
  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   656
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   657
  unfolding continuous_def by (rule tendsto_power)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   658
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   659
lemma continuous_on_power [continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   660
  fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   661
  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   662
  unfolding continuous_on_def by (auto intro: tendsto_power)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   663
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   664
lemma tendsto_setprod [tendsto_intros]:
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   665
  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   666
  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   667
  shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   668
proof (cases "finite S")
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   669
  assume "finite S" thus ?thesis using assms
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   670
    by (induct, simp add: tendsto_const, simp add: tendsto_mult)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   671
next
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   672
  assume "\<not> finite S" thus ?thesis
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   673
    by (simp add: tendsto_const)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   674
qed
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   675
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   676
lemma continuous_setprod [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   677
  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   678
  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   679
  unfolding continuous_def by (rule tendsto_setprod)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   680
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   681
lemma continuous_on_setprod [continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   682
  fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   683
  shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   684
  unfolding continuous_on_def by (auto intro: tendsto_setprod)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   685
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   686
subsubsection {* Inverse and division *}
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   687
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   688
lemma (in bounded_bilinear) Zfun_prod_Bfun:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   689
  assumes f: "Zfun f F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   690
  assumes g: "Bfun g F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   691
  shows "Zfun (\<lambda>x. f x ** g x) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   692
proof -
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   693
  obtain K where K: "0 \<le> K"
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   694
    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   695
    using nonneg_bounded by fast
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   696
  obtain B where B: "0 < B"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   697
    and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   698
    using g by (rule BfunE)
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   699
  have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   700
  using norm_g proof eventually_elim
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   701
    case (elim x)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   702
    have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   703
      by (rule norm_le)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   704
    also have "\<dots> \<le> norm (f x) * B * K"
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   705
      by (intro mult_mono' order_refl norm_g norm_ge_zero
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   706
                mult_nonneg_nonneg K elim)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   707
    also have "\<dots> = norm (f x) * (B * K)"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   708
      by (rule mult_assoc)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   709
    finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" .
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   710
  qed
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   711
  with f show ?thesis
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   712
    by (rule Zfun_imp_Zfun)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   713
qed
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   714
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   715
lemma (in bounded_bilinear) flip:
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   716
  "bounded_bilinear (\<lambda>x y. y ** x)"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   717
  apply default
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   718
  apply (rule add_right)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   719
  apply (rule add_left)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   720
  apply (rule scaleR_right)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   721
  apply (rule scaleR_left)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   722
  apply (subst mult_commute)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   723
  using bounded by fast
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   724
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   725
lemma (in bounded_bilinear) Bfun_prod_Zfun:
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   726
  assumes f: "Bfun f F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   727
  assumes g: "Zfun g F"
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   728
  shows "Zfun (\<lambda>x. f x ** g x) F"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   729
  using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   730
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   731
lemma Bfun_inverse_lemma:
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   732
  fixes x :: "'a::real_normed_div_algebra"
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   733
  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
44081
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   734
  apply (subst nonzero_norm_inverse, clarsimp)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   735
  apply (erule (1) le_imp_inverse_le)
730f7cced3a6 rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents: 44079
diff changeset
   736
  done
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   737
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   738
lemma Bfun_inverse:
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   739
  fixes a :: "'a::real_normed_div_algebra"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   740
  assumes f: "(f ---> a) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   741
  assumes a: "a \<noteq> 0"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   742
  shows "Bfun (\<lambda>x. inverse (f x)) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   743
proof -
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   744
  from a have "0 < norm a" by simp
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   745
  hence "\<exists>r>0. r < norm a" by (rule dense)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   746
  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   747
  have "eventually (\<lambda>x. dist (f x) a < r) F"
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   748
    using tendstoD [OF f r1] by fast
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   749
  hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) F"
46887
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   750
  proof eventually_elim
cb891d9a23c1 use eventually_elim method
noschinl
parents: 46886
diff changeset
   751
    case (elim x)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   752
    hence 1: "norm (f x - a) < r"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   753
      by (simp add: dist_norm)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   754
    hence 2: "f x \<noteq> 0" using r2 by auto
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   755
    hence "norm (inverse (f x)) = inverse (norm (f x))"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   756
      by (rule nonzero_norm_inverse)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   757
    also have "\<dots> \<le> inverse (norm a - r)"
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   758
    proof (rule le_imp_inverse_le)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   759
      show "0 < norm a - r" using r2 by simp
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   760
    next
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   761
      have "norm a - norm (f x) \<le> norm (a - f x)"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   762
        by (rule norm_triangle_ineq2)
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   763
      also have "\<dots> = norm (f x - a)"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   764
        by (rule norm_minus_commute)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   765
      also have "\<dots> < r" using 1 .
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   766
      finally show "norm a - r \<le> norm (f x)" by simp
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   767
    qed
31487
93938cafc0e6 put syntax for tendsto in Limits.thy; rename variables
huffman
parents: 31447
diff changeset
   768
    finally show "norm (inverse (f x)) \<le> inverse (norm a - r)" .
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   769
  qed
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   770
  thus ?thesis by (rule BfunI)
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   771
qed
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   772
31565
da5a5589418e theorem attribute [tendsto_intros]
huffman
parents: 31492
diff changeset
   773
lemma tendsto_inverse [tendsto_intros]:
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   774
  fixes a :: "'a::real_normed_div_algebra"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   775
  assumes f: "(f ---> a) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   776
  assumes a: "a \<noteq> 0"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   777
  shows "((\<lambda>x. inverse (f x)) ---> inverse a) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   778
proof -
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   779
  from a have "0 < norm a" by simp
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   780
  with f have "eventually (\<lambda>x. dist (f x) a < norm a) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   781
    by (rule tendstoD)
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   782
  then have "eventually (\<lambda>x. f x \<noteq> 0) F"
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   783
    unfolding dist_norm by (auto elim!: eventually_elim1)
44627
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   784
  with a have "eventually (\<lambda>x. inverse (f x) - inverse a =
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   785
    - (inverse (f x) * (f x - a) * inverse a)) F"
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   786
    by (auto elim!: eventually_elim1 simp: inverse_diff_inverse)
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   787
  moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F"
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   788
    by (intro Zfun_minus Zfun_mult_left
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   789
      bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult]
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   790
      Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff])
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   791
  ultimately show ?thesis
134c06282ae6 convert to Isar-style proof
huffman
parents: 44571
diff changeset
   792
    unfolding tendsto_Zfun_iff by (rule Zfun_ssubst)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   793
qed
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   794
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   795
lemma continuous_inverse:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   796
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   797
  assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   798
  shows "continuous F (\<lambda>x. inverse (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   799
  using assms unfolding continuous_def by (rule tendsto_inverse)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   800
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   801
lemma continuous_at_within_inverse[continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   802
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   803
  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   804
  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   805
  using assms unfolding continuous_within by (rule tendsto_inverse)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   806
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   807
lemma isCont_inverse[continuous_intros, simp]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   808
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   809
  assumes "isCont f a" and "f a \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   810
  shows "isCont (\<lambda>x. inverse (f x)) a"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   811
  using assms unfolding continuous_at by (rule tendsto_inverse)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   812
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   813
lemma continuous_on_inverse[continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   814
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   815
  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   816
  shows "continuous_on s (\<lambda>x. inverse (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   817
  using assms unfolding continuous_on_def by (fast intro: tendsto_inverse)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   818
31565
da5a5589418e theorem attribute [tendsto_intros]
huffman
parents: 31492
diff changeset
   819
lemma tendsto_divide [tendsto_intros]:
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   820
  fixes a b :: "'a::real_normed_field"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   821
  shows "\<lbrakk>(f ---> a) F; (g ---> b) F; b \<noteq> 0\<rbrakk>
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   822
    \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) F"
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44253
diff changeset
   823
  by (simp add: tendsto_mult tendsto_inverse divide_inverse)
31355
3d18766ddc4b limits of inverse using filters
huffman
parents: 31353
diff changeset
   824
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   825
lemma continuous_divide:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   826
  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   827
  assumes "continuous F f" and "continuous F g" and "g (Lim F (\<lambda>x. x)) \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   828
  shows "continuous F (\<lambda>x. (f x) / (g x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   829
  using assms unfolding continuous_def by (rule tendsto_divide)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   830
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   831
lemma continuous_at_within_divide[continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   832
  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   833
  assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   834
  shows "continuous (at a within s) (\<lambda>x. (f x) / (g x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   835
  using assms unfolding continuous_within by (rule tendsto_divide)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   836
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   837
lemma isCont_divide[continuous_intros, simp]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   838
  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   839
  assumes "isCont f a" "isCont g a" "g a \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   840
  shows "isCont (\<lambda>x. (f x) / g x) a"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   841
  using assms unfolding continuous_at by (rule tendsto_divide)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   842
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   843
lemma continuous_on_divide[continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   844
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   845
  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   846
  shows "continuous_on s (\<lambda>x. (f x) / (g x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   847
  using assms unfolding continuous_on_def by (fast intro: tendsto_divide)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   848
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   849
lemma tendsto_sgn [tendsto_intros]:
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   850
  fixes l :: "'a::real_normed_vector"
44195
f5363511b212 consistently use variable name 'F' for filters
huffman
parents: 44194
diff changeset
   851
  shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
44194
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   852
  unfolding sgn_div_norm by (simp add: tendsto_intros)
0639898074ae generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents: 44081
diff changeset
   853
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   854
lemma continuous_sgn:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   855
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   856
  assumes "continuous F f" and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   857
  shows "continuous F (\<lambda>x. sgn (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   858
  using assms unfolding continuous_def by (rule tendsto_sgn)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   859
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   860
lemma continuous_at_within_sgn[continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   861
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   862
  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   863
  shows "continuous (at a within s) (\<lambda>x. sgn (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   864
  using assms unfolding continuous_within by (rule tendsto_sgn)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   865
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   866
lemma isCont_sgn[continuous_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   867
  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   868
  assumes "isCont f a" and "f a \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   869
  shows "isCont (\<lambda>x. sgn (f x)) a"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   870
  using assms unfolding continuous_at by (rule tendsto_sgn)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   871
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   872
lemma continuous_on_sgn[continuous_on_intros]:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   873
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   874
  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   875
  shows "continuous_on s (\<lambda>x. sgn (f x))"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   876
  using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   877
50325
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   878
lemma filterlim_at_infinity:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   879
  fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   880
  assumes "0 \<le> c"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   881
  shows "(LIM x F. f x :> at_infinity) \<longleftrightarrow> (\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   882
  unfolding filterlim_iff eventually_at_infinity
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   883
proof safe
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   884
  fix P :: "'a \<Rightarrow> bool" and b
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   885
  assume *: "\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   886
    and P: "\<forall>x. b \<le> norm x \<longrightarrow> P x"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   887
  have "max b (c + 1) > c" by auto
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   888
  with * have "eventually (\<lambda>x. max b (c + 1) \<le> norm (f x)) F"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   889
    by auto
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   890
  then show "eventually (\<lambda>x. P (f x)) F"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   891
  proof eventually_elim
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   892
    fix x assume "max b (c + 1) \<le> norm (f x)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   893
    with P show "P (f x)" by auto
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   894
  qed
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   895
qed force
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
   896
51529
2d2f59e6055a move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
hoelzl
parents: 51526
diff changeset
   897
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   898
subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   899
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   900
text {*
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   901
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   902
This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   903
@{term "at_right x"} and also @{term "at_right 0"}.
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   904
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   905
*}
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   906
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents: 51360
diff changeset
   907
lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   908
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   909
lemma filtermap_homeomorph:
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   910
  assumes f: "continuous (at a) f"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   911
  assumes g: "continuous (at (f a)) g"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   912
  assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   913
  shows "filtermap f (nhds a) = nhds (f a)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   914
  unfolding filter_eq_iff eventually_filtermap eventually_nhds
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   915
proof safe
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   916
  fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   917
  from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   918
  show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   919
next
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   920
  fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   921
  with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   922
  obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   923
    by (metis UNIV_I)
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   924
  with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   925
    by (force intro!: exI[of _ A])
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   926
qed
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   927
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   928
lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   929
  by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   930
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   931
lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   932
  by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   933
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   934
lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   935
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   936
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   937
lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d::real)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   938
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   939
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   940
lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   941
  using filtermap_at_right_shift[of "-a" 0] by simp
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   942
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   943
lemma filterlim_at_right_to_0:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   944
  "filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   945
  unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   946
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   947
lemma eventually_at_right_to_0:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   948
  "eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   949
  unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   950
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   951
lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a::'a::real_normed_vector)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   952
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   953
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   954
lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x. - x) (at_right (- a))"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   955
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   956
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   957
lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x. - x) (at_left (- a))"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   958
  by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   959
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   960
lemma filterlim_at_left_to_right:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   961
  "filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   962
  unfolding filterlim_def filtermap_filtermap at_left_minus[of a] ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   963
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   964
lemma eventually_at_left_to_right:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   965
  "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   966
  unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   967
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   968
lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   969
  unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   970
  by (metis le_minus_iff minus_minus)
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   971
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   972
lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   973
  unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   974
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   975
lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   976
  unfolding filterlim_def at_top_mirror filtermap_filtermap ..
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   977
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   978
lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (-x::real) :> F)"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   979
  unfolding filterlim_def at_bot_mirror filtermap_filtermap ..
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   980
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   981
lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   982
  unfolding filterlim_at_top eventually_at_bot_dense
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   983
  by (metis leI minus_less_iff order_less_asym)
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   984
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   985
lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   986
  unfolding filterlim_at_bot eventually_at_top_dense
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   987
  by (metis leI less_minus_iff order_less_asym)
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   988
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   989
lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_bot)"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   990
  using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F]
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   991
  using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   992
  by auto
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   993
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   994
lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
   995
  unfolding filterlim_uminus_at_top by simp
50323
3764d4620fb3 add filterlim rules for unary minus and inverse
hoelzl
parents: 50322
diff changeset
   996
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   997
lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
   998
  unfolding filterlim_at_top_gt[where c=0] eventually_at_filter
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
   999
proof safe
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1000
  fix Z :: real assume [arith]: "0 < Z"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1001
  then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1002
    by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1003
  then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1004
    by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1005
qed
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1006
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1007
lemma filterlim_inverse_at_top:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1008
  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1009
  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1010
     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1011
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1012
lemma filterlim_inverse_at_bot_neg:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1013
  "LIM x (at_left (0::real)). inverse x :> at_bot"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1014
  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1015
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1016
lemma filterlim_inverse_at_bot:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1017
  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1018
  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1019
  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1020
50325
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1021
lemma tendsto_inverse_0:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1022
  fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1023
  shows "(inverse ---> (0::'a)) at_infinity"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1024
  unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1025
proof safe
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1026
  fix r :: real assume "0 < r"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1027
  show "\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> norm (inverse x :: 'a) < r"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1028
  proof (intro exI[of _ "inverse (r / 2)"] allI impI)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1029
    fix x :: 'a
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1030
    from `0 < r` have "0 < inverse (r / 2)" by simp
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1031
    also assume *: "inverse (r / 2) \<le> norm x"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1032
    finally show "norm (inverse x) < r"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1033
      using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1034
  qed
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1035
qed
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1036
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1037
lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1038
proof (rule antisym)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1039
  have "(inverse ---> (0::real)) at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1040
    by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1041
  then show "filtermap inverse at_top \<le> at_right (0::real)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1042
    by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1043
next
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1044
  have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1045
    using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1046
  then show "at_right (0::real) \<le> filtermap inverse at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1047
    by (simp add: filtermap_ident filtermap_filtermap)
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1048
qed
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1049
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1050
lemma eventually_at_right_to_top:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1051
  "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1052
  unfolding at_right_to_top eventually_filtermap ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1053
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1054
lemma filterlim_at_right_to_top:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1055
  "filterlim f F (at_right (0::real)) \<longleftrightarrow> (LIM x at_top. f (inverse x) :> F)"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1056
  unfolding filterlim_def at_right_to_top filtermap_filtermap ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1057
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1058
lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1059
  unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1060
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1061
lemma eventually_at_top_to_right:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1062
  "eventually P at_top \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) (at_right (0::real))"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1063
  unfolding at_top_to_right eventually_filtermap ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1064
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1065
lemma filterlim_at_top_to_right:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1066
  "filterlim f F at_top \<longleftrightarrow> (LIM x (at_right (0::real)). f (inverse x) :> F)"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1067
  unfolding filterlim_def at_top_to_right filtermap_filtermap ..
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1068
50325
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1069
lemma filterlim_inverse_at_infinity:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1070
  fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1071
  shows "filterlim inverse at_infinity (at (0::'a))"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1072
  unfolding filterlim_at_infinity[OF order_refl]
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1073
proof safe
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1074
  fix r :: real assume "0 < r"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1075
  then show "eventually (\<lambda>x::'a. r \<le> norm (inverse x)) (at 0)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1076
    unfolding eventually_at norm_inverse
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1077
    by (intro exI[of _ "inverse r"])
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1078
       (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1079
qed
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1080
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1081
lemma filterlim_inverse_at_iff:
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1082
  fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1083
  shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1084
  unfolding filterlim_def filtermap_filtermap[symmetric]
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1085
proof
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1086
  assume "filtermap g F \<le> at_infinity"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1087
  then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1088
    by (rule filtermap_mono)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1089
  also have "\<dots> \<le> at 0"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1090
    using tendsto_inverse_0[where 'a='b]
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1091
    by (auto intro!: exI[of _ 1]
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1092
             simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity)
50325
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1093
  finally show "filtermap inverse (filtermap g F) \<le> at 0" .
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1094
next
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1095
  assume "filtermap inverse (filtermap g F) \<le> at 0"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1096
  then have "filtermap inverse (filtermap inverse (filtermap g F)) \<le> filtermap inverse (at 0)"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1097
    by (rule filtermap_mono)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1098
  with filterlim_inverse_at_infinity show "filtermap g F \<le> at_infinity"
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1099
    by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1100
qed
5e40ad9f212a add filterlim rules for inverse and at_infinity
hoelzl
parents: 50324
diff changeset
  1101
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1102
lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51531
diff changeset
  1103
 by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1104
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1105
text {*
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1106
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1107
We only show rules for multiplication and addition when the functions are either against a real
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1108
value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}.
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1109
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1110
*}
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1111
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1112
lemma filterlim_tendsto_pos_mult_at_top: 
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1113
  assumes f: "(f ---> c) F" and c: "0 < c"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1114
  assumes g: "LIM x F. g x :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1115
  shows "LIM x F. (f x * g x :: real) :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1116
  unfolding filterlim_at_top_gt[where c=0]
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1117
proof safe
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1118
  fix Z :: real assume "0 < Z"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1119
  from f `0 < c` have "eventually (\<lambda>x. c / 2 < f x) F"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1120
    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1121
             simp: dist_real_def abs_real_def split: split_if_asm)
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1122
  moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1123
    unfolding filterlim_at_top by auto
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1124
  ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1125
  proof eventually_elim
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1126
    fix x assume "c / 2 < f x" "Z / c * 2 \<le> g x"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1127
    with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) \<le> f x * g x"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1128
      by (intro mult_mono) (auto simp: zero_le_divide_iff)
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1129
    with `0 < c` show "Z \<le> f x * g x"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1130
       by simp
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1131
  qed
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1132
qed
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1133
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1134
lemma filterlim_at_top_mult_at_top: 
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1135
  assumes f: "LIM x F. f x :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1136
  assumes g: "LIM x F. g x :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1137
  shows "LIM x F. (f x * g x :: real) :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1138
  unfolding filterlim_at_top_gt[where c=0]
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1139
proof safe
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1140
  fix Z :: real assume "0 < Z"
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1141
  from f have "eventually (\<lambda>x. 1 \<le> f x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1142
    unfolding filterlim_at_top by auto
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1143
  moreover from g have "eventually (\<lambda>x. Z \<le> g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1144
    unfolding filterlim_at_top by auto
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1145
  ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1146
  proof eventually_elim
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1147
    fix x assume "1 \<le> f x" "Z \<le> g x"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1148
    with `0 < Z` have "1 * Z \<le> f x * g x"
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1149
      by (intro mult_mono) (auto simp: zero_le_divide_iff)
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1150
    then show "Z \<le> f x * g x"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1151
       by simp
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1152
  qed
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1153
qed
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1154
50419
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1155
lemma filterlim_tendsto_pos_mult_at_bot:
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1156
  assumes "(f ---> c) F" "0 < (c::real)" "filterlim g at_bot F"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1157
  shows "LIM x F. f x * g x :> at_bot"
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1158
  using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3)
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1159
  unfolding filterlim_uminus_at_bot by simp
3177d0374701 add exponential and uniform distributions
hoelzl
parents: 50347
diff changeset
  1160
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1161
lemma filterlim_tendsto_add_at_top: 
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1162
  assumes f: "(f ---> c) F"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1163
  assumes g: "LIM x F. g x :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1164
  shows "LIM x F. (f x + g x :: real) :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1165
  unfolding filterlim_at_top_gt[where c=0]
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1166
proof safe
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1167
  fix Z :: real assume "0 < Z"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1168
  from f have "eventually (\<lambda>x. c - 1 < f x) F"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1169
    by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def)
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1170
  moreover from g have "eventually (\<lambda>x. Z - (c - 1) \<le> g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1171
    unfolding filterlim_at_top by auto
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1172
  ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1173
    by eventually_elim simp
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1174
qed
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1175
50347
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1176
lemma LIM_at_top_divide:
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1177
  fixes f g :: "'a \<Rightarrow> real"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1178
  assumes f: "(f ---> a) F" "0 < a"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1179
  assumes g: "(g ---> 0) F" "eventually (\<lambda>x. 0 < g x) F"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1180
  shows "LIM x F. f x / g x :> at_top"
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1181
  unfolding divide_inverse
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1182
  by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
77e3effa50b6 prove tendsto_power_div_exp_0
hoelzl
parents: 50346
diff changeset
  1183
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1184
lemma filterlim_at_top_add_at_top: 
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1185
  assumes f: "LIM x F. f x :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1186
  assumes g: "LIM x F. g x :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1187
  shows "LIM x F. (f x + g x :: real) :> at_top"
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1188
  unfolding filterlim_at_top_gt[where c=0]
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1189
proof safe
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1190
  fix Z :: real assume "0 < Z"
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1191
  from f have "eventually (\<lambda>x. 0 \<le> f x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1192
    unfolding filterlim_at_top by auto
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1193
  moreover from g have "eventually (\<lambda>x. Z \<le> g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1194
    unfolding filterlim_at_top by auto
50346
a75c6429c3c3 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents: 50331
diff changeset
  1195
  ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F"
50324
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1196
    by eventually_elim simp
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1197
qed
0a1242d5e7d4 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents: 50323
diff changeset
  1198
50331
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1199
lemma tendsto_divide_0:
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1200
  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1201
  assumes f: "(f ---> c) F"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1202
  assumes g: "LIM x F. g x :> at_infinity"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1203
  shows "((\<lambda>x. f x / g x) ---> 0) F"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1204
  using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1205
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1206
lemma linear_plus_1_le_power:
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1207
  fixes x :: real
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1208
  assumes x: "0 \<le> x"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1209
  shows "real n * x + 1 \<le> (x + 1) ^ n"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1210
proof (induct n)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1211
  case (Suc n)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1212
  have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1213
    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1214
  also have "\<dots> \<le> (x + 1)^Suc n"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1215
    using Suc x by (simp add: mult_left_mono)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1216
  finally show ?case .
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1217
qed simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1218
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1219
lemma filterlim_realpow_sequentially_gt1:
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1220
  fixes x :: "'a :: real_normed_div_algebra"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1221
  assumes x[arith]: "1 < norm x"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1222
  shows "LIM n sequentially. x ^ n :> at_infinity"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1223
proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1224
  fix y :: real assume "0 < y"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1225
  have "0 < norm x - 1" by simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1226
  then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1227
  also have "\<dots> \<le> real N * (norm x - 1) + 1" by simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1228
  also have "\<dots> \<le> (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1229
  also have "\<dots> = norm x ^ N" by simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1230
  finally have "\<forall>n\<ge>N. y \<le> norm x ^ n"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1231
    by (metis order_less_le_trans power_increasing order_less_imp_le x)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1232
  then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially"
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1233
    unfolding eventually_sequentially
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1234
    by (auto simp: norm_power)
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1235
qed simp
4b6dc5077e98 use filterlim in Lim and SEQ; tuned proofs
hoelzl
parents: 50330
diff changeset
  1236
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents: 51360
diff changeset
  1237
51526
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1238
subsection {* Limits of Sequences *}
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1239
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1240
lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1241
  by simp
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1242
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1243
lemma LIMSEQ_iff:
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1244
  fixes L :: "'a::real_normed_vector"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1245
  shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1246
unfolding LIMSEQ_def dist_norm ..
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1247
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1248
lemma LIMSEQ_I:
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1249
  fixes L :: "'a::real_normed_vector"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1250
  shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1251
by (simp add: LIMSEQ_iff)
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1252
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1253
lemma LIMSEQ_D:
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1254
  fixes L :: "'a::real_normed_vector"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1255
  shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1256
by (simp add: LIMSEQ_iff)
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1257
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1258
lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1259
  unfolding tendsto_def eventually_sequentially
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1260
  by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1261
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1262
lemma Bseq_inverse_lemma:
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1263
  fixes x :: "'a::real_normed_div_algebra"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1264
  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1265
apply (subst nonzero_norm_inverse, clarsimp)
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1266
apply (erule (1) le_imp_inverse_le)
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1267
done
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1268
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1269
lemma Bseq_inverse:
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1270
  fixes a :: "'a::real_normed_div_algebra"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1271
  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1272
  by (rule Bfun_inverse)
155263089e7b move SEQ.thy and Lim.thy to Limits.thy
hoelzl
parents: 51524
diff changeset
  1273