src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
author paulson <lp15@cam.ac.uk>
Tue, 10 Nov 2015 14:18:41 +0000
changeset 61609 77b453bd616f
parent 61531 ab2e862263e7
child 61610 4f54d2759a0b
permissions -rw-r--r--
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     1
(*  Author: John Harrison, Marco Maggesi, Graziano Gentili, Gianni Ciolli, Valentina Bruno
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     2
    Ported from "hol_light/Multivariate/canal.ml" by L C Paulson (2014)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     3
*)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     4
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
     5
section \<open>Complex Analysis Basics\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     6
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     7
theory Complex_Analysis_Basics
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     8
imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
     9
begin
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    10
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    11
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    12
lemma cmod_fact [simp]: "cmod (fact n) = fact n"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    13
  by (metis norm_of_nat of_nat_fact)
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    14
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
    15
subsection\<open>General lemmas\<close>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    16
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    17
lemma has_derivative_mult_right:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    18
  fixes c:: "'a :: real_normed_algebra"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    19
  shows "((op * c) has_derivative (op * c)) F"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    20
by (rule has_derivative_mult_right [OF has_derivative_id])
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    21
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    22
lemma has_derivative_of_real[derivative_intros, simp]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    23
  "(f has_derivative f') F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_derivative (\<lambda>x. of_real (f' x))) F"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    24
  using bounded_linear.has_derivative[OF bounded_linear_of_real] .
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    25
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    26
lemma has_vector_derivative_real_complex:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    27
  "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a)"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    28
  using has_derivative_compose[of of_real of_real a UNIV f "op * f'"]
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    29
  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    30
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
    31
lemma fact_cancel:
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
    32
  fixes c :: "'a::real_field"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    33
  shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    34
  by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56479
diff changeset
    35
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    36
lemma linear_times:
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    37
  fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
  by (auto simp: linearI distrib_left)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    39
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    40
lemma bilinear_times:
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    41
  fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    42
  by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    43
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
lemma linear_cnj: "linear cnj"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    45
  using bounded_linear.linear[OF bounded_linear_cnj] .
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    46
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    47
lemma tendsto_mult_left:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    48
  fixes c::"'a::real_normed_algebra"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    49
  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) ---> c * l) F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    50
by (rule tendsto_mult [OF tendsto_const])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    51
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    52
lemma tendsto_mult_right:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    53
  fixes c::"'a::real_normed_algebra"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    54
  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) ---> l * c) F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    55
by (rule tendsto_mult [OF _ tendsto_const])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    56
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    57
lemma tendsto_Re_upper:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    58
  assumes "~ (trivial_limit F)"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    59
          "(f ---> l) F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    60
          "eventually (\<lambda>x. Re(f x) \<le> b) F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    61
    shows  "Re(l) \<le> b"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    62
  by (metis assms tendsto_le [OF _ tendsto_const]  tendsto_Re)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    63
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    64
lemma tendsto_Re_lower:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    65
  assumes "~ (trivial_limit F)"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    66
          "(f ---> l) F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    67
          "eventually (\<lambda>x. b \<le> Re(f x)) F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    68
    shows  "b \<le> Re(l)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    69
  by (metis assms tendsto_le [OF _ _ tendsto_const]  tendsto_Re)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    71
lemma tendsto_Im_upper:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    72
  assumes "~ (trivial_limit F)"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    73
          "(f ---> l) F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    74
          "eventually (\<lambda>x. Im(f x) \<le> b) F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
    shows  "Im(l) \<le> b"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    76
  by (metis assms tendsto_le [OF _ tendsto_const]  tendsto_Im)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    77
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
lemma tendsto_Im_lower:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    79
  assumes "~ (trivial_limit F)"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    80
          "(f ---> l) F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    81
          "eventually (\<lambda>x. b \<le> Im(f x)) F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    82
    shows  "b \<le> Im(l)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
  by (metis assms tendsto_le [OF _ _ tendsto_const]  tendsto_Im)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    84
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    85
lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    86
  by auto
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    87
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    88
lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    89
  by auto
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    90
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    91
lemma continuous_mult_left:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    92
  fixes c::"'a::real_normed_algebra"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    93
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    94
by (rule continuous_mult [OF continuous_const])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    95
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    96
lemma continuous_mult_right:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
    97
  fixes c::"'a::real_normed_algebra"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    98
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    99
by (rule continuous_mult [OF _ continuous_const])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
lemma continuous_on_mult_left:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   102
  fixes c::"'a::real_normed_algebra"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   103
  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   104
by (rule continuous_on_mult [OF continuous_on_const])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   105
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   106
lemma continuous_on_mult_right:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   107
  fixes c::"'a::real_normed_algebra"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   109
by (rule continuous_on_mult [OF _ continuous_on_const])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   110
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56370
diff changeset
   111
lemma uniformly_continuous_on_cmul_right [continuous_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   112
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56261
diff changeset
   113
  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   114
  using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] .
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   115
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56370
diff changeset
   116
lemma uniformly_continuous_on_cmul_left[continuous_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   117
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
  assumes "uniformly_continuous_on s f"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   119
    shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   120
by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   121
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   122
lemma continuous_within_norm_id [continuous_intros]: "continuous (at x within S) norm"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   123
  by (rule continuous_norm [OF continuous_ident])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   124
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   125
lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   126
  by (intro continuous_on_id continuous_on_norm)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   127
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   128
subsection\<open>DERIV stuff\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   129
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   130
lemma DERIV_zero_connected_constant:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
  assumes "connected s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   133
      and "open s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   134
      and "finite k"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   135
      and "continuous_on s f"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   136
      and "\<forall>x\<in>(s - k). DERIV f x :> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
    obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   138
using has_derivative_zero_connected_constant [OF assms(1-4)] assms
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   139
by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
lemma DERIV_zero_constant:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   142
  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   143
  shows    "\<lbrakk>convex s;
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   144
             \<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)\<rbrakk>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
             \<Longrightarrow> \<exists>c. \<forall>x \<in> s. f(x) = c"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   146
  by (auto simp: has_field_derivative_def lambda_zero intro: has_derivative_zero_constant)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   147
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   148
lemma DERIV_zero_unique:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   149
  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
  assumes "convex s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
      and d0: "\<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   152
      and "a \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
      and "x \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
    shows "f x = f a"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   155
  by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)])
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56261
diff changeset
   156
     (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   157
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   158
lemma DERIV_zero_connected_unique:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   159
  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   160
  assumes "connected s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   161
      and "open s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   162
      and d0: "\<And>x. x\<in>s \<Longrightarrow> DERIV f x :> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   163
      and "a \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   164
      and "x \<in> s"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   165
    shows "f x = f a"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   166
    by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)])
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   167
       (metis has_field_derivative_def lambda_zero d0)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   168
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   169
lemma DERIV_transform_within:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   170
  assumes "(f has_field_derivative f') (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   171
      and "0 < d" "a \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   172
      and "\<And>x. x\<in>s \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   173
    shows "(g has_field_derivative f') (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   174
  using assms unfolding has_field_derivative_def
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56261
diff changeset
   175
  by (blast intro: has_derivative_transform_within)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   176
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   177
lemma DERIV_transform_within_open:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   178
  assumes "DERIV f a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   179
      and "open s" "a \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   180
      and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   181
    shows "DERIV g a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   182
  using assms unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   183
by (metis has_derivative_transform_within_open)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   184
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   185
lemma DERIV_transform_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   186
  assumes "DERIV f a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   187
      and "0 < d"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   188
      and "\<And>x. dist x a < d \<Longrightarrow> f x = g x"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   189
    shows "DERIV g a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   190
  by (blast intro: assms DERIV_transform_within)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   191
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   192
(*generalising DERIV_isconst_all, which requires type real (using the ordering)*)
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   193
lemma DERIV_zero_UNIV_unique:
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   194
  fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   195
  shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   196
by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   197
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   198
subsection \<open>Some limit theorems about real part of real series etc.\<close>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   199
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   200
(*MOVE? But not to Finite_Cartesian_Product*)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   201
lemma sums_vec_nth :
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   202
  assumes "f sums a"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   203
  shows "(\<lambda>x. f x $ i) sums a $ i"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   204
using assms unfolding sums_def
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   205
by (auto dest: tendsto_vec_nth [where i=i])
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   206
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   207
lemma summable_vec_nth :
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   208
  assumes "summable f"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   209
  shows "summable (\<lambda>x. f x $ i)"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   210
using assms unfolding summable_def
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   211
by (blast intro: sums_vec_nth)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   212
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   213
subsection \<open>Complex number lemmas\<close>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   214
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   215
lemma
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   216
  shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   217
    and open_halfspace_Re_gt: "open {z. Re(z) > b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   218
    and closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   219
    and closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   220
    and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   221
    and open_halfspace_Im_lt: "open {z. Im(z) < b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   222
    and open_halfspace_Im_gt: "open {z. Im(z) > b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   223
    and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   224
    and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   225
    and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   226
  by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
60150
bd773c47ad0b New material about complex transcendental functions (especially Ln, Arg) and polynomials
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
   227
            isCont_Im continuous_ident continuous_const)+
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   228
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60585
diff changeset
   229
lemma closed_complex_Reals: "closed (\<real> :: complex set)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   230
proof -
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60585
diff changeset
   231
  have "(\<real> :: complex set) = {z. Im z = 0}"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   232
    by (auto simp: complex_is_Real_iff)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   233
  then show ?thesis
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   234
    by (metis closed_halfspace_Im_eq)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   235
qed
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   236
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   237
lemma closed_Real_halfspace_Re_le: "closed (\<real> \<inter> {w. Re w \<le> x})"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   238
  by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   239
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   240
lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   241
  using closed_halfspace_Re_ge
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   242
  by (simp add: closed_Int closed_complex_Reals)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   243
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   244
lemma closed_real_abs_le: "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   245
proof -
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   246
  have "{w \<in> \<real>. \<bar>Re w\<bar> \<le> r} = (\<real> \<inter> {w. Re w \<le> r}) \<inter> (\<real> \<inter> {w. Re w \<ge> -r})"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   247
    by auto
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   248
  then show "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   249
    by (simp add: closed_Int closed_Real_halfspace_Re_ge closed_Real_halfspace_Re_le)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   250
qed
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
   251
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   252
lemma real_lim:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   253
  fixes l::complex
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   254
  assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   255
  shows  "l \<in> \<real>"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   256
proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   257
  show "eventually (\<lambda>x. f x \<in> \<real>) F"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   258
    using assms(3, 4) by (auto intro: eventually_mono)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   259
qed
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   260
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   261
lemma real_lim_sequentially:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   262
  fixes l::complex
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   263
  shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   264
by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   265
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   266
lemma real_series:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   267
  fixes l::complex
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   268
  shows "f sums l \<Longrightarrow> (\<And>n. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   269
unfolding sums_def
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   270
by (metis real_lim_sequentially setsum_in_Reals)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   271
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   272
lemma Lim_null_comparison_Re:
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56479
diff changeset
   273
  assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g ---> 0) F" shows "(f ---> 0) F"
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56479
diff changeset
   274
  by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   275
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   276
subsection\<open>Holomorphic functions\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   277
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   278
definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   279
           (infixr "(complex'_differentiable)" 50)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   280
  where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   281
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   282
lemma complex_differentiable_imp_continuous_at:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   283
    "f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   284
  by (metis DERIV_continuous complex_differentiable_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   285
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   286
lemma complex_differentiable_within_subset:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   287
    "\<lbrakk>f complex_differentiable (at x within s); t \<subseteq> s\<rbrakk>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   288
     \<Longrightarrow> f complex_differentiable (at x within t)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   289
  by (metis DERIV_subset complex_differentiable_def)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   290
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   291
lemma complex_differentiable_at_within:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   292
    "\<lbrakk>f complex_differentiable (at x)\<rbrakk>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   293
     \<Longrightarrow> f complex_differentiable (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   294
  unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   295
  by (metis DERIV_subset top_greatest)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   296
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   297
lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   298
proof -
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   299
  show ?thesis
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   300
    unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   301
    by (force intro: has_derivative_mult_right)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   302
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   303
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   304
lemma complex_differentiable_const [derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   305
  unfolding complex_differentiable_def has_field_derivative_def
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   306
  by (rule exI [where x=0])
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   307
     (metis has_derivative_const lambda_zero)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   308
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   309
lemma complex_differentiable_ident [derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   310
  unfolding complex_differentiable_def has_field_derivative_def
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   311
  by (rule exI [where x=1])
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   312
     (simp add: lambda_one [symmetric])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   313
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   314
lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   315
  unfolding id_def by (rule complex_differentiable_ident)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   316
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   317
lemma complex_differentiable_minus [derivative_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   318
  "f complex_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) complex_differentiable F"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   319
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   320
  by (metis field_differentiable_minus)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   321
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   322
lemma complex_differentiable_add [derivative_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   323
  assumes "f complex_differentiable F" "g complex_differentiable F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   324
    shows "(\<lambda>z. f z + g z) complex_differentiable F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   325
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   326
  by (metis field_differentiable_add)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   327
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   328
lemma complex_differentiable_setsum [derivative_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   329
  "(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   330
  by (induct I rule: infinite_finite_induct)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   331
     (auto intro: complex_differentiable_add complex_differentiable_const)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   332
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   333
lemma complex_differentiable_diff [derivative_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   334
  assumes "f complex_differentiable F" "g complex_differentiable F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   335
    shows "(\<lambda>z. f z - g z) complex_differentiable F"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   336
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   337
  by (metis field_differentiable_diff)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   338
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   339
lemma complex_differentiable_inverse [derivative_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   340
  assumes "f complex_differentiable (at a within s)" "f a \<noteq> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   341
  shows "(\<lambda>z. inverse (f z)) complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   342
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   343
  by (metis DERIV_inverse_fun)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   344
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   345
lemma complex_differentiable_mult [derivative_intros]:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   346
  assumes "f complex_differentiable (at a within s)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   347
          "g complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   348
    shows "(\<lambda>z. f z * g z) complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   349
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   350
  by (metis DERIV_mult [of f _ a s g])
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   351
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   352
lemma complex_differentiable_divide [derivative_intros]:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   353
  assumes "f complex_differentiable (at a within s)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   354
          "g complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   355
          "g a \<noteq> 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   356
    shows "(\<lambda>z. f z / g z) complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   357
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   358
  by (metis DERIV_divide [of f _ a s g])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   359
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   360
lemma complex_differentiable_power [derivative_intros]:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   361
  assumes "f complex_differentiable (at a within s)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   362
    shows "(\<lambda>z. f z ^ n) complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   363
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   364
  by (metis DERIV_power)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   365
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   366
lemma complex_differentiable_transform_within:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   367
  "0 < d \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   368
        x \<in> s \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   369
        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   370
        f complex_differentiable (at x within s)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   371
        \<Longrightarrow> g complex_differentiable (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   372
  unfolding complex_differentiable_def has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   373
  by (blast intro: has_derivative_transform_within)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   374
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   375
lemma complex_differentiable_compose_within:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   376
  assumes "f complex_differentiable (at a within s)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   377
          "g complex_differentiable (at (f a) within f`s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   378
    shows "(g o f) complex_differentiable (at a within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   379
  using assms unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   380
  by (metis DERIV_image_chain)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   381
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   382
lemma complex_differentiable_compose:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   383
  "f complex_differentiable at z \<Longrightarrow> g complex_differentiable at (f z)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   384
          \<Longrightarrow> (g o f) complex_differentiable at z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   385
by (metis complex_differentiable_at_within complex_differentiable_compose_within)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   386
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   387
lemma complex_differentiable_within_open:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   388
     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f complex_differentiable at a within s \<longleftrightarrow>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   389
                          f complex_differentiable at a"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   390
  unfolding complex_differentiable_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   391
  by (metis at_within_open)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   392
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   393
subsection\<open>Caratheodory characterization.\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   394
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   395
lemma complex_differentiable_caratheodory_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   396
  "f complex_differentiable (at z) \<longleftrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   397
         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   398
  using CARAT_DERIV [of f]
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   399
  by (simp add: complex_differentiable_def has_field_derivative_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   400
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   401
lemma complex_differentiable_caratheodory_within:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   402
  "f complex_differentiable (at z within s) \<longleftrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   403
         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   404
  using DERIV_caratheodory_within [of f]
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   405
  by (simp add: complex_differentiable_def has_field_derivative_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   406
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   407
subsection\<open>Holomorphic\<close>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   408
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   409
definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   410
           (infixl "(holomorphic'_on)" 50)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   411
  where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f complex_differentiable (at x within s)"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   412
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   413
named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   414
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   415
lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   416
  by (simp add: holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   417
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   418
lemma holomorphic_on_open:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   419
    "open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   420
  by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s])
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   421
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   422
lemma holomorphic_on_imp_continuous_on:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   423
    "f holomorphic_on s \<Longrightarrow> continuous_on s f"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   424
  by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   425
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   426
lemma holomorphic_on_subset:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   427
    "f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   428
  unfolding holomorphic_on_def
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   429
  by (metis complex_differentiable_within_subset subsetD)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   430
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   431
lemma holomorphic_transform: "\<lbrakk>f holomorphic_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   432
  by (metis complex_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   433
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   434
lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   435
  by (metis holomorphic_transform)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   436
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   437
lemma holomorphic_on_linear [holomorphic_intros]: "(op * c) holomorphic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   438
  unfolding holomorphic_on_def by (metis complex_differentiable_linear)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   439
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   440
lemma holomorphic_on_const [holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   441
  unfolding holomorphic_on_def by (metis complex_differentiable_const)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   442
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   443
lemma holomorphic_on_ident [holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   444
  unfolding holomorphic_on_def by (metis complex_differentiable_ident)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   445
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   446
lemma holomorphic_on_id [holomorphic_intros]: "id holomorphic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   447
  unfolding id_def by (rule holomorphic_on_ident)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   448
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   449
lemma holomorphic_on_compose:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   450
  "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   451
  using complex_differentiable_compose_within[of f _ s g]
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   452
  by (auto simp: holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   453
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   454
lemma holomorphic_on_compose_gen:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   455
  "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   456
  by (metis holomorphic_on_compose holomorphic_on_subset)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   457
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   458
lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   459
  by (metis complex_differentiable_minus holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   460
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   461
lemma holomorphic_on_add [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   462
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   463
  unfolding holomorphic_on_def by (metis complex_differentiable_add)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   464
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   465
lemma holomorphic_on_diff [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   466
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   467
  unfolding holomorphic_on_def by (metis complex_differentiable_diff)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   468
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   469
lemma holomorphic_on_mult [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   470
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   471
  unfolding holomorphic_on_def by (metis complex_differentiable_mult)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   472
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   473
lemma holomorphic_on_inverse [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   474
  "\<lbrakk>f holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. inverse (f z)) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   475
  unfolding holomorphic_on_def by (metis complex_differentiable_inverse)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   476
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   477
lemma holomorphic_on_divide [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   478
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s; \<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>z. f z / g z) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   479
  unfolding holomorphic_on_def by (metis complex_differentiable_divide)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   480
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   481
lemma holomorphic_on_power [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   482
  "f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   483
  unfolding holomorphic_on_def by (metis complex_differentiable_power)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   484
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   485
lemma holomorphic_on_setsum [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   486
  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   487
  unfolding holomorphic_on_def by (metis complex_differentiable_setsum)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   488
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   489
lemma DERIV_deriv_iff_complex_differentiable:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   490
  "DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   491
  unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   492
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   493
lemma complex_derivative_chain:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   494
  "f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   495
    \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   496
  by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   497
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   498
lemma complex_derivative_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   499
  by (metis DERIV_imp_deriv DERIV_cmult_Id)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   500
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   501
lemma complex_derivative_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   502
  by (metis DERIV_imp_deriv DERIV_ident)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   503
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   504
lemma complex_derivative_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   505
  by (metis DERIV_imp_deriv DERIV_const)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   506
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   507
lemma complex_derivative_add:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   508
  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   509
   \<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   510
  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   511
  by (auto intro!: DERIV_imp_deriv derivative_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   512
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   513
lemma complex_derivative_diff:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   514
  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   515
   \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   516
  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   517
  by (auto intro!: DERIV_imp_deriv derivative_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   518
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   519
lemma complex_derivative_mult:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   520
  "\<lbrakk>f complex_differentiable at z; g complex_differentiable at z\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   521
   \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   522
  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   523
  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   524
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   525
lemma complex_derivative_cmult:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   526
  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   527
  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   528
  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   529
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   530
lemma complex_derivative_cmult_right:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   531
  "f complex_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   532
  unfolding DERIV_deriv_iff_complex_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   533
  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   534
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   535
lemma complex_derivative_transform_within_open:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   536
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   537
   \<Longrightarrow> deriv f z = deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   538
  unfolding holomorphic_on_def
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   539
  by (rule DERIV_imp_deriv)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   540
     (metis DERIV_deriv_iff_complex_differentiable DERIV_transform_within_open at_within_open)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   541
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   542
lemma complex_derivative_compose_linear:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   543
  "f complex_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   544
apply (rule DERIV_imp_deriv)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   545
apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric])
59554
4044f53326c9 inlined rules to free user-space from technical names
haftmann
parents: 58877
diff changeset
   546
apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id])
4044f53326c9 inlined rules to free user-space from technical names
haftmann
parents: 58877
diff changeset
   547
apply (simp add: algebra_simps)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   548
done
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   549
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   550
subsection\<open>Analyticity on a set\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   551
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   552
definition analytic_on (infixl "(analytic'_on)" 50)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   553
  where
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   554
   "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   555
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   556
lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   557
  by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   558
     (metis centre_in_ball complex_differentiable_at_within)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   559
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   560
lemma analytic_on_open: "open s \<Longrightarrow> f analytic_on s \<longleftrightarrow> f holomorphic_on s"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   561
apply (auto simp: analytic_imp_holomorphic)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   562
apply (auto simp: analytic_on_def holomorphic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   563
by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   564
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   565
lemma analytic_on_imp_differentiable_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   566
  "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f complex_differentiable (at x)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   567
 apply (auto simp: analytic_on_def holomorphic_on_def)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   568
by (metis Topology_Euclidean_Space.open_ball centre_in_ball complex_differentiable_within_open)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   569
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   570
lemma analytic_on_subset: "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   571
  by (auto simp: analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   572
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   573
lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   574
  by (auto simp: analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   575
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60420
diff changeset
   576
lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   577
  by (auto simp: analytic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   578
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   579
lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   580
  by (auto simp: analytic_on_def)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   581
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   582
lemma analytic_on_holomorphic:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   583
  "f analytic_on s \<longleftrightarrow> (\<exists>t. open t \<and> s \<subseteq> t \<and> f holomorphic_on t)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   584
  (is "?lhs = ?rhs")
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   585
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   586
  have "?lhs \<longleftrightarrow> (\<exists>t. open t \<and> s \<subseteq> t \<and> f analytic_on t)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   587
  proof safe
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   588
    assume "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   589
    then show "\<exists>t. open t \<and> s \<subseteq> t \<and> f analytic_on t"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   590
      apply (simp add: analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   591
      apply (rule exI [where x="\<Union>{u. open u \<and> f analytic_on u}"], auto)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   592
      apply (metis Topology_Euclidean_Space.open_ball analytic_on_open centre_in_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   593
      by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   594
  next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   595
    fix t
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   596
    assume "open t" "s \<subseteq> t" "f analytic_on t"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   597
    then show "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   598
        by (metis analytic_on_subset)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   599
  qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   600
  also have "... \<longleftrightarrow> ?rhs"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   601
    by (auto simp: analytic_on_open)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   602
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   603
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   604
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   605
lemma analytic_on_linear: "(op * c) analytic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   606
  by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   607
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   608
lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   609
  by (metis analytic_on_def holomorphic_on_const zero_less_one)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   610
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   611
lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   612
  by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   613
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   614
lemma analytic_on_id: "id analytic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   615
  unfolding id_def by (rule analytic_on_ident)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   616
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   617
lemma analytic_on_compose:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   618
  assumes f: "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   619
      and g: "g analytic_on (f ` s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   620
    shows "(g o f) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   621
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   622
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   623
  fix x
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   624
  assume x: "x \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   625
  then obtain e where e: "0 < e" and fh: "f holomorphic_on ball x e" using f
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   626
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   627
  obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   628
    by (metis analytic_on_def g image_eqI x)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   629
  have "isCont f x"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   630
    by (metis analytic_on_imp_differentiable_at complex_differentiable_imp_continuous_at f x)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   631
  with e' obtain d where d: "0 < d" and fd: "f ` ball x d \<subseteq> ball (f x) e'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   632
     by (auto simp: continuous_at_ball)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   633
  have "g \<circ> f holomorphic_on ball x (min d e)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   634
    apply (rule holomorphic_on_compose)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   635
    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   636
    by (metis fd gh holomorphic_on_subset image_mono min.cobounded1 subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   637
  then show "\<exists>e>0. g \<circ> f holomorphic_on ball x e"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   638
    by (metis d e min_less_iff_conj)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   639
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   640
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   641
lemma analytic_on_compose_gen:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   642
  "f analytic_on s \<Longrightarrow> g analytic_on t \<Longrightarrow> (\<And>z. z \<in> s \<Longrightarrow> f z \<in> t)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   643
             \<Longrightarrow> g o f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   644
by (metis analytic_on_compose analytic_on_subset image_subset_iff)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   645
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   646
lemma analytic_on_neg:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   647
  "f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   648
by (metis analytic_on_holomorphic holomorphic_on_minus)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   649
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   650
lemma analytic_on_add:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   651
  assumes f: "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   652
      and g: "g analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   653
    shows "(\<lambda>z. f z + g z) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   654
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   655
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   656
  fix z
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   657
  assume z: "z \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   658
  then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   659
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   660
  obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   661
    by (metis analytic_on_def g z)
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   662
  have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   663
    apply (rule holomorphic_on_add)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   664
    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   665
    by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   666
  then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   667
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   668
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   669
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   670
lemma analytic_on_diff:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   671
  assumes f: "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   672
      and g: "g analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   673
    shows "(\<lambda>z. f z - g z) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   674
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   675
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   676
  fix z
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   677
  assume z: "z \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   678
  then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   679
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   680
  obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   681
    by (metis analytic_on_def g z)
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   682
  have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   683
    apply (rule holomorphic_on_diff)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   684
    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   685
    by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   686
  then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   687
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   688
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   689
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   690
lemma analytic_on_mult:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   691
  assumes f: "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   692
      and g: "g analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   693
    shows "(\<lambda>z. f z * g z) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   694
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   695
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   696
  fix z
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   697
  assume z: "z \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   698
  then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   699
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   700
  obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   701
    by (metis analytic_on_def g z)
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   702
  have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   703
    apply (rule holomorphic_on_mult)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   704
    apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   705
    by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   706
  then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   707
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   708
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   709
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   710
lemma analytic_on_inverse:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   711
  assumes f: "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   712
      and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   713
    shows "(\<lambda>z. inverse (f z)) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   714
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   715
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   716
  fix z
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   717
  assume z: "z \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   718
  then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   719
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   720
  have "continuous_on (ball z e) f"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   721
    by (metis fh holomorphic_on_imp_continuous_on)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   722
  then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   723
    by (metis Topology_Euclidean_Space.open_ball centre_in_ball continuous_on_open_avoid e z nz)
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   724
  have "(\<lambda>z. inverse (f z)) holomorphic_on ball z (min e e')"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   725
    apply (rule holomorphic_on_inverse)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   726
    apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   727
    by (metis nz' mem_ball min_less_iff_conj)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   728
  then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   729
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   730
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   731
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   732
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   733
lemma analytic_on_divide:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   734
  assumes f: "f analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   735
      and g: "g analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   736
      and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   737
    shows "(\<lambda>z. f z / g z) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   738
unfolding divide_inverse
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   739
by (metis analytic_on_inverse analytic_on_mult f g nz)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   740
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   741
lemma analytic_on_power:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   742
  "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   743
by (induct n) (auto simp: analytic_on_const analytic_on_mult)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   744
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   745
lemma analytic_on_setsum:
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   746
  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   747
  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   748
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   749
subsection\<open>analyticity at a point.\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   750
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   751
lemma analytic_at_ball:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   752
  "f analytic_on {z} \<longleftrightarrow> (\<exists>e. 0<e \<and> f holomorphic_on ball z e)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   753
by (metis analytic_on_def singleton_iff)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   754
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   755
lemma analytic_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   756
    "f analytic_on {z} \<longleftrightarrow> (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   757
by (metis analytic_on_holomorphic empty_subsetI insert_subset)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   758
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   759
lemma analytic_on_analytic_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   760
    "f analytic_on s \<longleftrightarrow> (\<forall>z \<in> s. f analytic_on {z})"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   761
by (metis analytic_at_ball analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   762
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   763
lemma analytic_at_two:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   764
  "f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   765
   (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s \<and> g holomorphic_on s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   766
  (is "?lhs = ?rhs")
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   767
proof
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   768
  assume ?lhs
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   769
  then obtain s t
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   770
    where st: "open s" "z \<in> s" "f holomorphic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   771
              "open t" "z \<in> t" "g holomorphic_on t"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   772
    by (auto simp: analytic_at)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   773
  show ?rhs
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   774
    apply (rule_tac x="s \<inter> t" in exI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   775
    using st
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   776
    apply (auto simp: Diff_subset holomorphic_on_subset)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   777
    done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   778
next
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   779
  assume ?rhs
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   780
  then show ?lhs
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   781
    by (force simp add: analytic_at)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   782
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   783
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   784
subsection\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   785
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   786
lemma
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   787
  assumes "f analytic_on {z}" "g analytic_on {z}"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   788
  shows complex_derivative_add_at: "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   789
    and complex_derivative_diff_at: "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   790
    and complex_derivative_mult_at: "deriv (\<lambda>w. f w * g w) z =
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   791
           f z * deriv g z + deriv f z * g z"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   792
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   793
  obtain s where s: "open s" "z \<in> s" "f holomorphic_on s" "g holomorphic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   794
    using assms by (metis analytic_at_two)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   795
  show "deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   796
    apply (rule DERIV_imp_deriv [OF DERIV_add])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   797
    using s
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   798
    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   799
    done
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   800
  show "deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   801
    apply (rule DERIV_imp_deriv [OF DERIV_diff])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   802
    using s
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   803
    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   804
    done
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   805
  show "deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   806
    apply (rule DERIV_imp_deriv [OF DERIV_mult'])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   807
    using s
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   808
    apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   809
    done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   810
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   811
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   812
lemma complex_derivative_cmult_at:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   813
  "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   814
by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   815
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   816
lemma complex_derivative_cmult_right_at:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   817
  "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   818
by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   819
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   820
subsection\<open>Complex differentiation of sequences and series\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   821
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   822
(* TODO: Could probably be simplified using Uniform_Limit *)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   823
lemma has_complex_derivative_sequence:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   824
  fixes s :: "complex set"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   825
  assumes cvs: "convex s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   826
      and df:  "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   827
      and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s \<longrightarrow> norm (f' n x - g' x) \<le> e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   828
      and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) ---> l) sequentially"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   829
    shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) ---> g x) sequentially \<and>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   830
                       (g has_field_derivative (g' x)) (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   831
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   832
  from assms obtain x l where x: "x \<in> s" and tf: "((\<lambda>n. f n x) ---> l) sequentially"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   833
    by blast
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   834
  { fix e::real assume e: "e > 0"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   835
    then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> s \<longrightarrow> cmod (f' n x - g' x) \<le> e"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   836
      by (metis conv)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   837
    have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   838
    proof (rule exI [of _ N], clarify)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   839
      fix n y h
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   840
      assume "N \<le> n" "y \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   841
      then have "cmod (f' n y - g' y) \<le> e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   842
        by (metis N)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   843
      then have "cmod h * cmod (f' n y - g' y) \<le> cmod h * e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   844
        by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   845
      then show "cmod (f' n y * h - g' y * h) \<le> e * cmod h"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   846
        by (simp add: norm_mult [symmetric] field_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   847
    qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   848
  } note ** = this
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   849
  show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   850
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   851
  proof (rule has_derivative_sequence [OF cvs _ _ x])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   852
    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (op * (f' n x))) (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   853
      by (metis has_field_derivative_def df)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   854
  next show "(\<lambda>n. f n x) ----> l"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   855
    by (rule tf)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   856
  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   857
    by (blast intro: **)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   858
  qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   859
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   860
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   861
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   862
lemma has_complex_derivative_series:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   863
  fixes s :: "complex set"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   864
  assumes cvs: "convex s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   865
      and df:  "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   866
      and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   867
                \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   868
      and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) sums l)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   869
    shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((g has_field_derivative g' x) (at x within s))"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   870
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   871
  from assms obtain x l where x: "x \<in> s" and sf: "((\<lambda>n. f n x) sums l)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   872
    by blast
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   873
  { fix e::real assume e: "e > 0"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   874
    then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> s
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   875
            \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   876
      by (metis conv)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   877
    have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   878
    proof (rule exI [of _ N], clarify)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   879
      fix n y h
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   880
      assume "N \<le> n" "y \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   881
      then have "cmod ((\<Sum>i<n. f' i y) - g' y) \<le> e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   882
        by (metis N)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   883
      then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   884
        by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   885
      then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   886
        by (simp add: norm_mult [symmetric] field_simps setsum_right_distrib)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   887
    qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   888
  } note ** = this
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   889
  show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   890
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   891
  proof (rule has_derivative_series [OF cvs _ _ x])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   892
    fix n x
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   893
    assume "x \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   894
    then show "((f n) has_derivative (\<lambda>z. z * f' n x)) (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   895
      by (metis df has_field_derivative_def mult_commute_abs)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   896
  next show " ((\<lambda>n. f n x) sums l)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   897
    by (rule sf)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   898
  next show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   899
    by (blast intro: **)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   900
  qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   901
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   902
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   903
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   904
lemma complex_differentiable_series:
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   905
  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   906
  assumes "convex s" "open s"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   907
  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   908
  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   909
  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   910
  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   911
proof -
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   912
  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   913
    unfolding uniformly_convergent_on_def by blast
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   914
  from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   915
  have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   916
    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   917
  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   918
    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   919
  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   920
  from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   921
    by (simp add: has_field_derivative_def s)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   922
  have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   923
    by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   924
       (insert g, auto simp: sums_iff)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   925
  thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   926
    by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   927
qed
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   928
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   929
lemma complex_differentiable_series':
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   930
  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   931
  assumes "convex s" "open s"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   932
  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   933
  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   934
  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   935
  shows   "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x0)"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   936
  using complex_differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   937
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   938
subsection\<open>Bound theorem\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   939
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   940
lemma complex_differentiable_bound:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   941
  fixes s :: "complex set"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   942
  assumes cvs: "convex s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   943
      and df:  "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   944
      and dn:  "\<And>z. z \<in> s \<Longrightarrow> norm (f' z) \<le> B"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   945
      and "x \<in> s"  "y \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   946
    shows "norm(f x - f y) \<le> B * norm(x - y)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   947
  apply (rule differentiable_bound [OF cvs])
56223
7696903b9e61 generalize theory of operator norms to work with class real_normed_vector
huffman
parents: 56217
diff changeset
   948
  apply (rule ballI, erule df [unfolded has_field_derivative_def])
7696903b9e61 generalize theory of operator norms to work with class real_normed_vector
huffman
parents: 56217
diff changeset
   949
  apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn)
7696903b9e61 generalize theory of operator norms to work with class real_normed_vector
huffman
parents: 56217
diff changeset
   950
  apply fact
7696903b9e61 generalize theory of operator norms to work with class real_normed_vector
huffman
parents: 56217
diff changeset
   951
  apply fact
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   952
  done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   953
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   954
subsection\<open>Inverse function theorem for complex derivatives.\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   955
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   956
lemma has_complex_derivative_inverse_basic:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   957
  fixes f :: "complex \<Rightarrow> complex"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   958
  shows "DERIV f (g y) :> f' \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   959
        f' \<noteq> 0 \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   960
        continuous (at y) g \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   961
        open t \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   962
        y \<in> t \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   963
        (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   964
        \<Longrightarrow> DERIV g y :> inverse (f')"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   965
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   966
  apply (rule has_derivative_inverse_basic)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   967
  apply (auto simp:  bounded_linear_mult_right)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   968
  done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   969
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   970
(*Used only once, in Multivariate/cauchy.ml. *)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   971
lemma has_complex_derivative_inverse_strong:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   972
  fixes f :: "complex \<Rightarrow> complex"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   973
  shows "DERIV f x :> f' \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   974
         f' \<noteq> 0 \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   975
         open s \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   976
         x \<in> s \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   977
         continuous_on s f \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   978
         (\<And>z. z \<in> s \<Longrightarrow> g (f z) = z)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   979
         \<Longrightarrow> DERIV g (f x) :> inverse (f')"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   980
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   981
  apply (rule has_derivative_inverse_strong [of s x f g ])
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   982
  using assms
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   983
  by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   984
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   985
lemma has_complex_derivative_inverse_strong_x:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   986
  fixes f :: "complex \<Rightarrow> complex"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   987
  shows  "DERIV f (g y) :> f' \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   988
          f' \<noteq> 0 \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   989
          open s \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   990
          continuous_on s f \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   991
          g y \<in> s \<Longrightarrow> f(g y) = y \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   992
          (\<And>z. z \<in> s \<Longrightarrow> g (f z) = z)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   993
          \<Longrightarrow> DERIV g y :> inverse (f')"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   994
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   995
  apply (rule has_derivative_inverse_strong_x [of s g y f])
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
   996
  using assms
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   997
  by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   998
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   999
subsection \<open>Taylor on Complex Numbers\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1000
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1001
lemma setsum_Suc_reindex:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1002
  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1003
    shows  "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1004
by (induct n) auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1005
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1006
lemma complex_taylor:
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1007
  assumes s: "convex s"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1008
      and f: "\<And>i x. x \<in> s \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within s)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1009
      and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1010
      and w: "w \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1011
      and z: "z \<in> s"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1012
    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1013
          \<le> B * cmod(z - w)^(Suc n) / fact n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1014
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1015
  have wzs: "closed_segment w z \<subseteq> s" using assms
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1016
    by (metis convex_contains_segment)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1017
  { fix u
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1018
    assume "u \<in> closed_segment w z"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1019
    then have "u \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1020
      by (metis wzs subsetD)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1021
    have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1022
                      f (Suc i) u * (z-u)^i / (fact i)) =
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1023
              f (Suc n) u * (z-u) ^ n / (fact n)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1024
    proof (induction n)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1025
      case 0 show ?case by simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1026
    next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1027
      case (Suc n)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1028
      have "(\<Sum>i\<le>Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / (fact i) +
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1029
                             f (Suc i) u * (z-u) ^ i / (fact i)) =
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1030
           f (Suc n) u * (z-u) ^ n / (fact n) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1031
           f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) -
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1032
           f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))"
56479
91958d4b30f7 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents: 56409
diff changeset
  1033
        using Suc by simp
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1034
      also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1035
      proof -
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1036
        have "(fact(Suc n)) *
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1037
             (f(Suc n) u *(z-u) ^ n / (fact n) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1038
               f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / (fact(Suc n)) -
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1039
               f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / (fact(Suc n))) =
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1040
            ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1041
            ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1042
            ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1043
          by (simp add: algebra_simps del: fact.simps)
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1044
        also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1045
                         (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1046
                         (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1047
          by (simp del: fact.simps)
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1048
        also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1049
                         (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1050
                         (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1051
          by (simp only: fact.simps of_nat_mult ac_simps) simp
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1052
        also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1053
          by (simp add: algebra_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1054
        finally show ?thesis
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1055
        by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1056
      qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1057
      finally show ?case .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1058
    qed
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1059
    then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i)))
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1060
                has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1061
               (at u within s)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
  1062
      apply (intro derivative_eq_intros)
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
  1063
      apply (blast intro: assms \<open>u \<in> s\<close>)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1064
      apply (rule refl)+
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1065
      apply (auto simp: field_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1066
      done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1067
  } note sum_deriv = this
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1068
  { fix u
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1069
    assume u: "u \<in> closed_segment w z"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1070
    then have us: "u \<in> s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1071
      by (metis wzs subsetD)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1072
    have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> cmod (f (Suc n) u) * cmod (u - z) ^ n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1073
      by (metis norm_minus_commute order_refl)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1074
    also have "... \<le> cmod (f (Suc n) u) * cmod (z - w) ^ n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1075
      by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1076
    also have "... \<le> B * cmod (z - w) ^ n"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1077
      by (metis norm_ge_zero zero_le_power mult_right_mono  B [OF us])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1078
    finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> B * cmod (z - w) ^ n" .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1079
  } note cmod_bound = this
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1080
  have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)) = (\<Sum>i\<le>n. (f i z / (fact i)) * 0 ^ i)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1081
    by simp
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1082
  also have "\<dots> = f 0 z / (fact 0)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1083
    by (subst setsum_zero_power) simp
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1084
  finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1085
                \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1086
                        (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1087
    by (simp add: norm_minus_commute)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1088
  also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1089
    apply (rule complex_differentiable_bound
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1090
      [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
61518
ff12606337e9 new lemmas about topology, etc., for Cauchy integral formula
paulson
parents: 61235
diff changeset
  1091
         and s = "closed_segment w z", OF convex_closed_segment])
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1092
    apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs]
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1093
                  norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1094
    done
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1095
  also have "...  \<le> B * cmod (z - w) ^ Suc n / (fact n)"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1096
    by (simp add: algebra_simps norm_minus_commute)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1097
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1098
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1099
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
  1100
text\<open>Something more like the traditional MVT for real components.\<close>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
  1101
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1102
lemma complex_mvt_line:
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1103
  assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
61518
ff12606337e9 new lemmas about topology, etc., for Cauchy integral formula
paulson
parents: 61235
diff changeset
  1104
    shows "\<exists>u. u \<in> closed_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1105
proof -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1106
  have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1107
    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
  1108
  note assms[unfolded has_field_derivative_def, derivative_intros]
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1109
  show ?thesis
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1110
    apply (cut_tac mvt_simple
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1111
                     [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w +  t *\<^sub>R z)"
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1112
                      "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1113
    apply auto
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1114
    apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
61518
ff12606337e9 new lemmas about topology, etc., for Cauchy integral formula
paulson
parents: 61235
diff changeset
  1115
    apply (auto simp: closed_segment_def twz) []
ff12606337e9 new lemmas about topology, etc., for Cauchy integral formula
paulson
parents: 61235
diff changeset
  1116
    apply (intro derivative_eq_intros has_derivative_at_within, simp_all)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1117
    apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
61518
ff12606337e9 new lemmas about topology, etc., for Cauchy integral formula
paulson
parents: 61235
diff changeset
  1118
    apply (force simp: twz closed_segment_def)
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1119
    done
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1120
qed
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1121
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1122
lemma complex_taylor_mvt:
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1123
  assumes "\<And>i x. \<lbrakk>x \<in> closed_segment w z; i \<le> n\<rbrakk> \<Longrightarrow> ((f i) has_field_derivative f (Suc i) x) (at x)"
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1124
    shows "\<exists>u. u \<in> closed_segment w z \<and>
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1125
            Re (f 0 z) =
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1126
            Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / (fact i)) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1127
                (f (Suc n) u * (z-u)^n / (fact n)) * (z - w))"
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1128
proof -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1129
  { fix u
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1130
    assume u: "u \<in> closed_segment w z"
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1131
    have "(\<Sum>i = 0..n.
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1132
               (f (Suc i) u * (z-u) ^ i - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) /
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1133
               (fact i)) =
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1134
          f (Suc 0) u -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1135
             (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1136
             (fact (Suc n)) +
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1137
             (\<Sum>i = 0..n.
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1138
                 (f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1139
                 (fact (Suc i)))"
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1140
       by (subst setsum_Suc_reindex) simp
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1141
    also have "... = f (Suc 0) u -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1142
             (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1143
             (fact (Suc n)) +
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1144
             (\<Sum>i = 0..n.
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1145
                 f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i))  -
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1146
                 f (Suc i) u * (z-u) ^ i / (fact i))"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 56889
diff changeset
  1147
      by (simp only: diff_divide_distrib fact_cancel ac_simps)
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1148
    also have "... = f (Suc 0) u -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1149
             (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1150
             (fact (Suc n)) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1151
             f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1152
      by (subst setsum_Suc_diff) auto
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1153
    also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1154
      by (simp only: algebra_simps diff_divide_distrib fact_cancel)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61531
diff changeset
  1155
    finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1156
                             - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) =
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1157
                  f (Suc n) u * (z - u) ^ n / (fact n)" .
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1158
    then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1159
                f (Suc n) u * (z - u) ^ n / (fact n))  (at u)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
  1160
      apply (intro derivative_eq_intros)+
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1161
      apply (force intro: u assms)
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1162
      apply (rule refl)+
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 56889
diff changeset
  1163
      apply (auto simp: ac_simps)
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1164
      done
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1165
  }
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1166
  then show ?thesis
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1167
    apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / (fact i)"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1168
               "\<lambda>u. (f (Suc n) u * (z-u)^n / (fact n))"])
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1169
    apply (auto simp add: intro: open_closed_segment)
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1170
    done
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1171
qed
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1172
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1173
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
  1174
subsection \<open>Polynomal function extremal theorem, from HOL Light\<close>
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1175
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1176
lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1177
    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1178
  assumes "0 < e"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1179
    shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1180
proof (induct n)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1181
  case 0 with assms
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1182
  show ?case
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1183
    apply (rule_tac x="norm (c 0) / e" in exI)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1184
    apply (auto simp: field_simps)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1185
    done
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1186
next
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1187
  case (Suc n)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1188
  obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1189
    using Suc assms by blast
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1190
  show ?case
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1191
  proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1192
    fix z::'a
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1193
    assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1194
    then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1195
      using assms by (simp add: field_simps)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1196
    have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1197
      using M [OF z1] by simp
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1198
    then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1199
      by simp
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1200
    then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1201
      by (blast intro: norm_triangle_le elim: )
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1202
    also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1203
      by (simp add: norm_power norm_mult algebra_simps)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1204
    also have "... \<le> (e * norm z) * norm z ^ Suc n"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1205
      by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1206
    finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 60150
diff changeset
  1207
      by simp
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1208
  qed
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1209
qed
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1210
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1211
lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1212
    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1213
  assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1214
    shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1215
using kn
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1216
proof (induction n)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1217
  case 0
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1218
  then show ?case
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1219
    using k  by simp
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1220
next
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1221
  case (Suc m)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1222
  let ?even = ?case
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1223
  show ?even
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1224
  proof (cases "c (Suc m) = 0")
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1225
    case True
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1226
    then show ?even using Suc k
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1227
      by auto (metis antisym_conv less_eq_Suc_le not_le)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1228
  next
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1229
    case False
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1230
    then obtain M where M:
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1231
          "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1232
      using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1233
      by auto
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1234
    have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1235
    proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1236
      fix z::'a
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1237
      assume z1: "M \<le> norm z" "1 \<le> norm z"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1238
         and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1239
      then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1240
        using False by (simp add: field_simps)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1241
      have nz: "norm z \<le> norm z ^ Suc m"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
  1242
        by (metis \<open>1 \<le> norm z\<close> One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1243
      have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1244
        by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1245
      have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1246
            \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1247
        using M [of z] Suc z1  by auto
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1248
      also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1249
        using nz by (simp add: mult_mono del: power_Suc)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1250
      finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1251
        using Suc.IH
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1252
        apply (auto simp: eventually_at_infinity)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1253
        apply (rule *)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1254
        apply (simp add: field_simps norm_mult norm_power)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1255
        done
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1256
    qed
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1257
    then show ?even
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1258
      by (simp add: eventually_at_infinity)
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1259
  qed
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1260
qed
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 59730
diff changeset
  1261
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1262
end