src/HOL/Analysis/Complex_Analysis_Basics.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon, 22 Oct 2018 19:03:47 +0200
changeset 69180 922833cc6839
parent 69064 5840724b1d71
child 69286 e4d5a07fecb6
permissions -rw-r--r--
Tagged some theories in HOL-Analysis
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
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 66252
diff changeset
     8
imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
56215
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
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    11
(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    12
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    13
subsection%unimportant\<open>General lemmas\<close>
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
    14
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
    15
lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
    16
  by (simp add: complex_nonneg_Reals_iff cmod_eq_Re)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    17
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    18
lemma has_derivative_mult_right:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    19
  fixes c:: "'a :: real_normed_algebra"
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
    20
  shows "(((*) c) has_derivative ((*) c)) F"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
    21
by (rule has_derivative_mult_right [OF has_derivative_ident])
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    22
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
    23
lemma has_derivative_of_real[derivative_intros, simp]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    24
  "(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
    25
  using bounded_linear.has_derivative[OF bounded_linear_of_real] .
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    26
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
    27
lemma has_vector_derivative_real_field:
61806
d2e62ae01cd8 Cauchy's integral formula for circles. Starting to fix eventually_mono.
paulson <lp15@cam.ac.uk>
parents: 61610
diff changeset
    28
  "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
    29
  using has_derivative_compose[of of_real of_real a _ f "(*) f'"]
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    30
  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
    31
lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    32
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
    33
lemma fact_cancel:
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
    34
  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
    35
  shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
    36
  using of_nat_neq_0 by force
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56479
diff changeset
    37
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    38
lemma bilinear_times:
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    39
  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
    40
  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
    41
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    42
lemma linear_cnj: "linear cnj"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
    43
  using bounded_linear.linear[OF bounded_linear_cnj] .
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    44
68721
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    45
lemma vector_derivative_cnj_within:
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    46
  assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    47
  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) = 
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    48
             cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D")
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    49
proof -
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    50
  let ?D = "vector_derivative f (at x within A)"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    51
  from assms have "(f has_vector_derivative ?D) (at x within A)"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    52
    by (subst (asm) vector_derivative_works)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    53
  hence "((\<lambda>x. cnj (f x)) has_vector_derivative cnj ?D) (at x within A)"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    54
    by (rule has_vector_derivative_cnj)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    55
  thus ?thesis using assms by (auto dest: vector_derivative_within)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    56
qed
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    57
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    58
lemma vector_derivative_cnj:
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    59
  assumes "f differentiable at x"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    60
  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    61
  using assms by (intro vector_derivative_cnj_within) auto
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
    62
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
    63
lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    64
  by auto
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    65
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
    66
lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    67
  by auto
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
    68
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56370
diff changeset
    69
lemma uniformly_continuous_on_cmul_right [continuous_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    70
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56261
diff changeset
    71
  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
    72
  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
    73
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56370
diff changeset
    74
lemma uniformly_continuous_on_cmul_left[continuous_intros]:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    75
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    76
  assumes "uniformly_continuous_on s f"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    77
    shows "uniformly_continuous_on s (\<lambda>x. c * f x)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    78
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
    79
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    80
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
    81
  by (rule continuous_norm [OF continuous_ident])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    82
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    83
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
    84
  by (intro continuous_on_id continuous_on_norm)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    85
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    86
(*MOVE? But not to Finite_Cartesian_Product*)
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    87
lemma sums_vec_nth :
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    88
  assumes "f sums a"
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    89
  shows "(\<lambda>x. f x $ i) sums a $ i"
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    90
using assms unfolding sums_def
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    91
by (auto dest: tendsto_vec_nth [where i=i])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
    92
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    93
lemma summable_vec_nth :
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    94
  assumes "summable f"
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    95
  shows "summable (\<lambda>x. f x $ i)"
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    96
using assms unfolding summable_def
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    97
by (blast intro: sums_vec_nth)
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    98
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
    99
(* TODO: Move? *)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   100
lemma DERIV_zero_connected_constant:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   101
  fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   102
  assumes "connected S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   103
      and "open S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   104
      and "finite K"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   105
      and "continuous_on S f"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   106
      and "\<forall>x\<in>(S - K). DERIV f x :> 0"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   107
    obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   108
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
   109
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
   110
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   111
lemmas DERIV_zero_constant = has_field_derivative_zero_constant
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   112
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   113
lemma DERIV_zero_unique:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   114
  assumes "convex S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   115
      and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   116
      and "a \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   117
      and "x \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   118
    shows "f x = f a"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   119
  by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)])
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56261
diff changeset
   120
     (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
56215
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 DERIV_zero_connected_unique:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   123
  assumes "connected S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   124
      and "open S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   125
      and d0: "\<And>x. x\<in>S \<Longrightarrow> DERIV f x :> 0"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   126
      and "a \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   127
      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
   128
    shows "f x = f a"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   129
    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
   130
       (metis has_field_derivative_def lambda_zero d0)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   131
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   132
lemma DERIV_transform_within:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   133
  assumes "(f has_field_derivative f') (at a within S)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   134
      and "0 < d" "a \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   135
      and "\<And>x. x\<in>S \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   136
    shows "(g has_field_derivative f') (at a within S)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   137
  using assms unfolding has_field_derivative_def
56332
289dd9166d04 tuned proofs
hoelzl
parents: 56261
diff changeset
   138
  by (blast intro: has_derivative_transform_within)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   139
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   140
lemma DERIV_transform_within_open:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   141
  assumes "DERIV f a :> f'"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   142
      and "open S" "a \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   143
      and "\<And>x. x\<in>S \<Longrightarrow> f x = g x"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   144
    shows "DERIV g a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   145
  using assms unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   146
by (metis has_derivative_transform_within_open)
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_transform_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   149
  assumes "DERIV f a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   150
      and "0 < d"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   151
      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
   152
    shows "DERIV g a :> f'"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   153
  by (blast intro: assms DERIV_transform_within)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   154
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   155
(*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
   156
lemma DERIV_zero_UNIV_unique:
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   157
  "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   158
  by (metis DERIV_zero_unique UNIV_I convex_UNIV)
59615
fdfdf89a83a6 A few new lemmas and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents: 59554
diff changeset
   159
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   160
lemma
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   161
  shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   162
    and open_halfspace_Re_gt: "open {z. Re(z) > b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   163
    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
   164
    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
   165
    and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   166
    and open_halfspace_Im_lt: "open {z. Im(z) < b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   167
    and open_halfspace_Im_gt: "open {z. Im(z) > b}"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   168
    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
   169
    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
   170
    and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
63332
f164526d8727 move open_Collect_eq/less to HOL
hoelzl
parents: 63092
diff changeset
   171
  by (intro open_Collect_less closed_Collect_le closed_Collect_eq continuous_on_Re
f164526d8727 move open_Collect_eq/less to HOL
hoelzl
parents: 63092
diff changeset
   172
            continuous_on_Im continuous_on_id continuous_on_const)+
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   173
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60585
diff changeset
   174
lemma closed_complex_Reals: "closed (\<real> :: complex set)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   175
proof -
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60585
diff changeset
   176
  have "(\<real> :: complex set) = {z. Im z = 0}"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   177
    by (auto simp: complex_is_Real_iff)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   178
  then show ?thesis
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   179
    by (metis closed_halfspace_Im_eq)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   180
qed
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   181
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
   182
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
   183
  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
   184
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   185
lemma closed_nonpos_Reals_complex [simp]: "closed (\<real>\<^sub>\<le>\<^sub>0 :: complex set)"
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   186
proof -
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   187
  have "\<real>\<^sub>\<le>\<^sub>0 = \<real> \<inter> {z. Re(z) \<le> 0}"
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   188
    using complex_nonpos_Reals_iff complex_is_Real_iff by auto
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   189
  then show ?thesis
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   190
    by (metis closed_Real_halfspace_Re_le)
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   191
qed
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   192
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
   193
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
   194
  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
   195
  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
   196
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   197
lemma closed_nonneg_Reals_complex [simp]: "closed (\<real>\<^sub>\<ge>\<^sub>0 :: complex set)"
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   198
proof -
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   199
  have "\<real>\<^sub>\<ge>\<^sub>0 = \<real> \<inter> {z. Re(z) \<ge> 0}"
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   200
    using complex_nonneg_Reals_iff complex_is_Real_iff by auto
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   201
  then show ?thesis
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   202
    by (metis closed_Real_halfspace_Re_ge)
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   203
qed
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   204
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
   205
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
   206
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
   207
  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
   208
    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
   209
  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
   210
    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
   211
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
   212
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   213
lemma real_lim:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   214
  fixes l::complex
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   215
  assumes "(f \<longlongrightarrow> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   216
  shows  "l \<in> \<real>"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   217
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
   218
  show "eventually (\<lambda>x. f x \<in> \<real>) F"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   219
    using assms(3, 4) by (auto intro: eventually_mono)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   220
qed
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   221
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   222
lemma real_lim_sequentially:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   223
  fixes l::complex
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   224
  shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   225
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
   226
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
   227
lemma real_series:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   228
  fixes l::complex
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   229
  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
   230
unfolding sums_def
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   231
by (metis real_lim_sequentially sum_in_Reals)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   232
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   233
lemma Lim_null_comparison_Re:
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   234
  assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g \<longlongrightarrow> 0) F" shows "(f \<longlongrightarrow> 0) F"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56479
diff changeset
   235
  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
   236
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   237
subsection\<open>Holomorphic functions\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   238
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   239
definition%important holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   240
           (infixl "(holomorphic'_on)" 50)
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   241
  where "f holomorphic_on s \<equiv> \<forall>x\<in>s. f field_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
   242
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   243
named_theorems%important holomorphic_intros "structural introduction rules for holomorphic_on"
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   244
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   245
lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f field_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   246
  by (simp add: holomorphic_on_def)
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   247
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   248
lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   249
  by (simp add: holomorphic_on_def)
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   250
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   251
lemma holomorphic_on_imp_differentiable_on:
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   252
    "f holomorphic_on s \<Longrightarrow> f differentiable_on s"
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   253
  unfolding holomorphic_on_def differentiable_on_def
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   254
  by (simp add: field_differentiable_imp_differentiable)
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   255
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   256
lemma holomorphic_on_imp_differentiable_at:
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   257
   "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
62131
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   258
using at_within_open holomorphic_on_def by fastforce
1baed43f453e nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
paulson
parents: 62087
diff changeset
   259
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   260
lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   261
  by (simp add: holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   262
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   263
lemma holomorphic_on_open:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   264
    "open s \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>f'. DERIV f x :> f')"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   265
  by (auto simp: holomorphic_on_def field_differentiable_def has_field_derivative_def at_within_open [of _ s])
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   266
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
   267
lemma holomorphic_on_imp_continuous_on:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   268
    "f holomorphic_on s \<Longrightarrow> continuous_on s f"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   269
  by (metis field_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
   270
62540
f2fc5485e3b0 Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
paulson <lp15@cam.ac.uk>
parents: 62534
diff changeset
   271
lemma holomorphic_on_subset [elim]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   272
    "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
   273
  unfolding holomorphic_on_def
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   274
  by (metis field_differentiable_within_subset subsetD)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   275
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   276
lemma holomorphic_transform: "\<lbrakk>f holomorphic_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   277
  by (metis field_differentiable_transform_within linordered_field_no_ub holomorphic_on_def)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   278
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   279
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
   280
  by (metis holomorphic_transform)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   281
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
   282
lemma holomorphic_on_linear [simp, holomorphic_intros]: "((*) c) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   283
  unfolding holomorphic_on_def by (metis field_differentiable_linear)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   284
62217
527488dc8b90 Reorganised a huge proof
paulson <lp15@cam.ac.uk>
parents: 62131
diff changeset
   285
lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   286
  unfolding holomorphic_on_def by (metis field_differentiable_const)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   287
62217
527488dc8b90 Reorganised a huge proof
paulson <lp15@cam.ac.uk>
parents: 62131
diff changeset
   288
lemma holomorphic_on_ident [simp, holomorphic_intros]: "(\<lambda>x. x) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   289
  unfolding holomorphic_on_def by (metis field_differentiable_ident)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   290
62217
527488dc8b90 Reorganised a huge proof
paulson <lp15@cam.ac.uk>
parents: 62131
diff changeset
   291
lemma holomorphic_on_id [simp, holomorphic_intros]: "id holomorphic_on s"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   292
  unfolding id_def by (rule holomorphic_on_ident)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   293
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   294
lemma holomorphic_on_compose:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   295
  "f holomorphic_on s \<Longrightarrow> g holomorphic_on (f ` s) \<Longrightarrow> (g o f) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   296
  using field_differentiable_compose_within[of f _ s g]
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   297
  by (auto simp: holomorphic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   298
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   299
lemma holomorphic_on_compose_gen:
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   300
  "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
   301
  by (metis holomorphic_on_compose holomorphic_on_subset)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   302
68721
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   303
lemma holomorphic_on_balls_imp_entire:
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   304
  assumes "\<not>bdd_above A" "\<And>r. r \<in> A \<Longrightarrow> f holomorphic_on ball c r"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   305
  shows   "f holomorphic_on B"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   306
proof (rule holomorphic_on_subset)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   307
  show "f holomorphic_on UNIV" unfolding holomorphic_on_def
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   308
  proof
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   309
    fix z :: complex
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   310
    from \<open>\<not>bdd_above A\<close> obtain r where r: "r \<in> A" "r > norm (z - c)"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   311
      by (meson bdd_aboveI not_le)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   312
    with assms(2) have "f holomorphic_on ball c r" by blast
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   313
    moreover from r have "z \<in> ball c r" by (auto simp: dist_norm norm_minus_commute)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   314
    ultimately show "f field_differentiable at z"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   315
      by (auto simp: holomorphic_on_def at_within_open[of _ "ball c r"])
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   316
  qed
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   317
qed auto
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   318
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   319
lemma holomorphic_on_balls_imp_entire':
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   320
  assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   321
  shows   "f holomorphic_on B"
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   322
proof (rule holomorphic_on_balls_imp_entire)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   323
  {
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   324
    fix M :: real
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   325
    have "\<exists>x. x > max M 0" by (intro gt_ex)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   326
    hence "\<exists>x>0. x > M" by auto
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   327
  }
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   328
  thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   329
    by (auto simp: not_le)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   330
qed (insert assms, auto)
53ad5c01be3f Small lemmas about analysis
eberlm <eberlm@in.tum.de>
parents: 68296
diff changeset
   331
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   332
lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   333
  by (metis field_differentiable_minus holomorphic_on_def)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   334
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   335
lemma holomorphic_on_add [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   336
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   337
  unfolding holomorphic_on_def by (metis field_differentiable_add)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
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 holomorphic_on_diff [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   340
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   341
  unfolding holomorphic_on_def by (metis field_differentiable_diff)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   342
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   343
lemma holomorphic_on_mult [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   344
  "\<lbrakk>f holomorphic_on s; g holomorphic_on s\<rbrakk> \<Longrightarrow> (\<lambda>z. f z * g z) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   345
  unfolding holomorphic_on_def by (metis field_differentiable_mult)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   346
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   347
lemma holomorphic_on_inverse [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   348
  "\<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"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   349
  unfolding holomorphic_on_def by (metis field_differentiable_inverse)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   350
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   351
lemma holomorphic_on_divide [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   352
  "\<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"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   353
  unfolding holomorphic_on_def by (metis field_differentiable_divide)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   354
61520
8f85bb443d33 Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents: 61518
diff changeset
   355
lemma holomorphic_on_power [holomorphic_intros]:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   356
  "f holomorphic_on s \<Longrightarrow> (\<lambda>z. (f z)^n) holomorphic_on s"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   357
  unfolding holomorphic_on_def by (metis field_differentiable_power)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   358
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   359
lemma holomorphic_on_sum [holomorphic_intros]:
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   360
  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   361
  unfolding holomorphic_on_def by (metis field_differentiable_sum)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   362
67135
1a94352812f4 Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents: 66827
diff changeset
   363
lemma holomorphic_on_prod [holomorphic_intros]:
1a94352812f4 Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents: 66827
diff changeset
   364
  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on s"
1a94352812f4 Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents: 66827
diff changeset
   365
  by (induction I rule: infinite_finite_induct) (auto intro: holomorphic_intros)
1a94352812f4 Moved material from AFP to Analysis/Number_Theory
Manuel Eberl <eberlm@in.tum.de>
parents: 66827
diff changeset
   366
66486
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   367
lemma holomorphic_pochhammer [holomorphic_intros]:
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   368
  "f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   369
  by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   370
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   371
lemma holomorphic_on_scaleR [holomorphic_intros]:
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   372
  "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   373
  by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
ffaaa83543b2 Lemmas about analysis and permutations
Manuel Eberl <eberlm@in.tum.de>
parents: 66453
diff changeset
   374
67167
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   375
lemma holomorphic_on_Un [holomorphic_intros]:
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   376
  assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   377
  shows   "f holomorphic_on (A \<union> B)"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   378
  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A]
67167
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   379
                             at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   380
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   381
lemma holomorphic_on_If_Un [holomorphic_intros]:
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   382
  assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B"
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   383
  assumes "\<And>z. z \<in> A \<Longrightarrow> z \<in> B \<Longrightarrow> f z = g z"
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   384
  shows   "(\<lambda>z. if z \<in> A then f z else g z) holomorphic_on (A \<union> B)" (is "?h holomorphic_on _")
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   385
proof (intro holomorphic_on_Un)
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   386
  note \<open>f holomorphic_on A\<close>
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   387
  also have "f holomorphic_on A \<longleftrightarrow> ?h holomorphic_on A"
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   388
    by (intro holomorphic_cong) auto
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   389
  finally show \<dots> .
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   390
next
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   391
  note \<open>g holomorphic_on B\<close>
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   392
  also have "g holomorphic_on B \<longleftrightarrow> ?h holomorphic_on B"
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   393
    using assms by (intro holomorphic_cong) auto
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   394
  finally show \<dots> .
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   395
qed (insert assms, auto)
88d1c9d86f48 Moved analysis material from AFP
Manuel Eberl <eberlm@in.tum.de>
parents: 67135
diff changeset
   396
67371
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   397
lemma leibniz_rule_holomorphic:
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   398
  fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   399
  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   400
  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   401
  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   402
  assumes "convex U"
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   403
  shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   404
  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   405
  by (auto simp: holomorphic_on_def)
2d9cf74943e1 moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents: 67167
diff changeset
   406
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   407
lemma DERIV_deriv_iff_field_differentiable:
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   408
  "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   409
  unfolding field_differentiable_def by (metis DERIV_imp_deriv)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   410
62533
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   411
lemma holomorphic_derivI:
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   412
     "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   413
      \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   414
by (metis DERIV_deriv_iff_field_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
62533
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   415
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   416
lemma complex_derivative_chain:
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   417
  "f field_differentiable at x \<Longrightarrow> g field_differentiable at (f x)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   418
    \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   419
  by (metis DERIV_deriv_iff_field_differentiable DERIV_chain DERIV_imp_deriv)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   420
62397
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62217
diff changeset
   421
lemma deriv_linear [simp]: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   422
  by (metis DERIV_imp_deriv DERIV_cmult_Id)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   423
62397
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62217
diff changeset
   424
lemma deriv_ident [simp]: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   425
  by (metis DERIV_imp_deriv DERIV_ident)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   426
62397
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62217
diff changeset
   427
lemma deriv_id [simp]: "deriv id = (\<lambda>z. 1)"
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62217
diff changeset
   428
  by (simp add: id_def)
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62217
diff changeset
   429
5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents: 62217
diff changeset
   430
lemma deriv_const [simp]: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   431
  by (metis DERIV_imp_deriv DERIV_const)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   432
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   433
lemma deriv_add [simp]:
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   434
  "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   435
   \<Longrightarrow> deriv (\<lambda>w. f w + g w) z = deriv f z + deriv g z"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   436
  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   437
  by (auto intro!: DERIV_imp_deriv derivative_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   438
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   439
lemma deriv_diff [simp]:
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   440
  "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   441
   \<Longrightarrow> deriv (\<lambda>w. f w - g w) z = deriv f z - deriv g z"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   442
  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   443
  by (auto intro!: DERIV_imp_deriv derivative_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   444
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   445
lemma deriv_mult [simp]:
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   446
  "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk>
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   447
   \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   448
  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   449
  by (auto intro!: DERIV_imp_deriv derivative_eq_intros)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   450
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   451
lemma deriv_cmult:
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   452
  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   453
  by simp
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   454
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   455
lemma deriv_cmult_right:
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   456
  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   457
  by simp
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   458
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   459
lemma deriv_inverse [simp]:
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   460
  "\<lbrakk>f field_differentiable at z; f z \<noteq> 0\<rbrakk>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   461
   \<Longrightarrow> deriv (\<lambda>w. inverse (f w)) z = - deriv f z / f z ^ 2"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   462
  unfolding DERIV_deriv_iff_field_differentiable[symmetric]
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   463
  by (safe intro!: DERIV_imp_deriv derivative_eq_intros) (auto simp: divide_simps power2_eq_square)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   464
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   465
lemma deriv_divide [simp]:
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   466
  "\<lbrakk>f field_differentiable at z; g field_differentiable at z; g z \<noteq> 0\<rbrakk>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   467
   \<Longrightarrow> deriv (\<lambda>w. f w / g w) z = (deriv f z * g z - f z * deriv g z) / g z ^ 2"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   468
  by (simp add: field_class.field_divide_inverse field_differentiable_inverse)
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   469
     (simp add: divide_simps power2_eq_square)
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   470
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   471
lemma deriv_cdivide_right:
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   472
  "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   473
  by (simp add: field_class.field_divide_inverse)
62217
527488dc8b90 Reorganised a huge proof
paulson <lp15@cam.ac.uk>
parents: 62131
diff changeset
   474
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   475
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
   476
  "\<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
   477
   \<Longrightarrow> deriv f z = deriv g z"
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   478
  unfolding holomorphic_on_def
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   479
  by (rule DERIV_imp_deriv)
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   480
     (metis DERIV_deriv_iff_field_differentiable DERIV_transform_within_open at_within_open)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   481
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   482
lemma deriv_compose_linear:
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   483
  "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   484
apply (rule DERIV_imp_deriv)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   485
  unfolding DERIV_deriv_iff_field_differentiable [symmetric]
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   486
  by (metis (full_types) DERIV_chain2 DERIV_cmult_Id mult.commute)
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   487
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   488
62533
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   489
lemma nonzero_deriv_nonconstant:
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   490
  assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   491
    shows "\<not> f constant_on S"
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   492
unfolding constant_on_def
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   493
by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique)
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   494
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   495
lemma holomorphic_nonconstant:
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   496
  assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0"
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   497
    shows "\<not> f constant_on S"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   498
  by (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   499
    (use assms in \<open>auto simp: holomorphic_derivI\<close>)
62533
bc25f3916a99 new material to Blochj's theorem, as well as supporting lemmas
paulson <lp15@cam.ac.uk>
parents: 62408
diff changeset
   500
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   501
subsection%unimportant\<open>Caratheodory characterization\<close>
64394
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   502
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   503
lemma field_differentiable_caratheodory_at:
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   504
  "f field_differentiable (at z) \<longleftrightarrow>
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   505
         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   506
  using CARAT_DERIV [of f]
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   507
  by (simp add: field_differentiable_def has_field_derivative_def)
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   508
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   509
lemma field_differentiable_caratheodory_within:
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   510
  "f field_differentiable (at z within s) \<longleftrightarrow>
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   511
         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   512
  using DERIV_caratheodory_within [of f]
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   513
  by (simp add: field_differentiable_def has_field_derivative_def)
141e1ed8d5a0 more new material
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   514
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
   515
subsection\<open>Analyticity on a set\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   516
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   517
definition%important analytic_on (infixl "(analytic'_on)" 50)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   518
  where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   519
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   520
named_theorems%important analytic_intros "introduction rules for proving analyticity"
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   521
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   522
lemma analytic_imp_holomorphic: "f analytic_on S \<Longrightarrow> f holomorphic_on S"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   523
  by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   524
     (metis centre_in_ball field_differentiable_at_within)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   525
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   526
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
   527
apply (auto simp: analytic_imp_holomorphic)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   528
apply (auto simp: analytic_on_def holomorphic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   529
by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   530
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   531
lemma analytic_on_imp_differentiable_at:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   532
  "f analytic_on S \<Longrightarrow> x \<in> S \<Longrightarrow> f field_differentiable (at x)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   533
 apply (auto simp: analytic_on_def holomorphic_on_def)
66827
c94531b5007d Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents: 66486
diff changeset
   534
by (metis open_ball centre_in_ball field_differentiable_within_open)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   535
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   536
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
   537
  by (auto simp: analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   538
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   539
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
   540
  by (auto simp: analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   541
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   542
lemma analytic_on_Union: "f analytic_on (\<Union>\<T>) \<longleftrightarrow> (\<forall>T \<in> \<T>. f analytic_on T)"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   543
  by (auto simp: analytic_on_def)
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   544
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   545
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
   546
  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
   547
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   548
lemma analytic_on_holomorphic:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   549
  "f analytic_on S \<longleftrightarrow> (\<exists>T. open T \<and> S \<subseteq> T \<and> f holomorphic_on T)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   550
  (is "?lhs = ?rhs")
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   551
proof -
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   552
  have "?lhs \<longleftrightarrow> (\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   553
  proof safe
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   554
    assume "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   555
    then show "\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   556
      apply (simp add: analytic_on_def)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   557
      apply (rule exI [where x="\<Union>{U. open U \<and> f analytic_on U}"], auto)
66827
c94531b5007d Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents: 66486
diff changeset
   558
      apply (metis open_ball analytic_on_open centre_in_ball)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   559
      by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   560
  next
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   561
    fix T
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   562
    assume "open T" "S \<subseteq> T" "f analytic_on T"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   563
    then show "f analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   564
        by (metis analytic_on_subset)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   565
  qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   566
  also have "... \<longleftrightarrow> ?rhs"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   567
    by (auto simp: analytic_on_open)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   568
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   569
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   570
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
   571
lemma analytic_on_linear [analytic_intros,simp]: "((*) c) analytic_on S"
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   572
  by (auto simp add: analytic_on_holomorphic)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   573
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   574
lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   575
  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
   576
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   577
lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on S"
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   578
  by (simp add: analytic_on_def gt_ex)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   579
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   580
lemma analytic_on_id [analytic_intros]: "id analytic_on S"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   581
  unfolding id_def by (rule analytic_on_ident)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   582
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   583
lemma analytic_on_compose:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   584
  assumes f: "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   585
      and g: "g analytic_on (f ` S)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   586
    shows "(g o f) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   587
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   588
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   589
  fix x
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   590
  assume x: "x \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   591
  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
   592
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   593
  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
   594
    by (metis analytic_on_def g image_eqI x)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   595
  have "isCont f x"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   596
    by (metis analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at f x)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   597
  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
   598
     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
   599
  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
   600
    apply (rule holomorphic_on_compose)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   601
    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
   602
    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
   603
  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
   604
    by (metis d e min_less_iff_conj)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   605
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   606
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   607
lemma analytic_on_compose_gen:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   608
  "f analytic_on S \<Longrightarrow> g analytic_on T \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<in> T)
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   609
             \<Longrightarrow> g o f analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   610
by (metis analytic_on_compose analytic_on_subset image_subset_iff)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   611
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   612
lemma analytic_on_neg [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   613
  "f analytic_on S \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   614
by (metis analytic_on_holomorphic holomorphic_on_minus)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   615
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   616
lemma analytic_on_add [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   617
  assumes f: "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   618
      and g: "g analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   619
    shows "(\<lambda>z. f z + g z) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   620
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   621
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   622
  fix z
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   623
  assume z: "z \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   624
  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
   625
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   626
  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
   627
    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
   628
  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
   629
    apply (rule holomorphic_on_add)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   630
    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
   631
    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
   632
  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
   633
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   634
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   635
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   636
lemma analytic_on_diff [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   637
  assumes f: "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   638
      and g: "g analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   639
    shows "(\<lambda>z. f z - g z) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   640
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   641
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   642
  fix z
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   643
  assume z: "z \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   644
  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
   645
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   646
  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
   647
    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
   648
  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
   649
    apply (rule holomorphic_on_diff)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   650
    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
   651
    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
   652
  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
   653
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   654
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   655
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   656
lemma analytic_on_mult [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   657
  assumes f: "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   658
      and g: "g analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   659
    shows "(\<lambda>z. f z * g z) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   660
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   661
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   662
  fix z
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   663
  assume z: "z \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   664
  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
   665
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   666
  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
   667
    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
   668
  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
   669
    apply (rule holomorphic_on_mult)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   670
    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
   671
    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
   672
  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
   673
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   674
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   675
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   676
lemma analytic_on_inverse [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   677
  assumes f: "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   678
      and nz: "(\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   679
    shows "(\<lambda>z. inverse (f z)) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   680
unfolding analytic_on_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   681
proof (intro ballI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   682
  fix z
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   683
  assume z: "z \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   684
  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
   685
    by (metis analytic_on_def)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   686
  have "continuous_on (ball z e) f"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   687
    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
   688
  then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0"
66827
c94531b5007d Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
paulson <lp15@cam.ac.uk>
parents: 66486
diff changeset
   689
    by (metis open_ball centre_in_ball continuous_on_open_avoid e z nz)
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
   690
  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
   691
    apply (rule holomorphic_on_inverse)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   692
    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
   693
    by (metis nz' mem_ball min_less_iff_conj)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   694
  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
   695
    by (metis e e' min_less_iff_conj)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   696
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   697
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   698
lemma analytic_on_divide [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   699
  assumes f: "f analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   700
      and g: "g analytic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   701
      and nz: "(\<And>z. z \<in> S \<Longrightarrow> g z \<noteq> 0)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   702
    shows "(\<lambda>z. f z / g z) analytic_on S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   703
unfolding divide_inverse
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   704
by (metis analytic_on_inverse analytic_on_mult f g nz)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   705
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   706
lemma analytic_on_power [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   707
  "f analytic_on S \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on S"
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   708
by (induct n) (auto simp: analytic_on_mult)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   709
65587
16a8991ab398 New material (and some tidying) purely in the Analysis directory
paulson <lp15@cam.ac.uk>
parents: 64394
diff changeset
   710
lemma analytic_on_sum [analytic_intros]:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   711
  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on S"
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
   712
  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
   713
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   714
lemma deriv_left_inverse:
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   715
  assumes "f holomorphic_on S" and "g holomorphic_on T"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   716
      and "open S" and "open T"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   717
      and "f ` S \<subseteq> T"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   718
      and [simp]: "\<And>z. z \<in> S \<Longrightarrow> g (f z) = z"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   719
      and "w \<in> S"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   720
    shows "deriv f w * deriv g (f w) = 1"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   721
proof -
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   722
  have "deriv f w * deriv g (f w) = deriv g (f w) * deriv f w"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   723
    by (simp add: algebra_simps)
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   724
  also have "... = deriv (g o f) w"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   725
    using assms
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   726
    by (metis analytic_on_imp_differentiable_at analytic_on_open complex_derivative_chain image_subset_iff)
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   727
  also have "... = deriv id w"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   728
  proof (rule complex_derivative_transform_within_open [where s=S])
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   729
    show "g \<circ> f holomorphic_on S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   730
      by (rule assms holomorphic_on_compose_gen holomorphic_intros)+
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   731
  qed (use assms in auto)
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   732
  also have "... = 1"
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   733
    by simp
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   734
  finally show ?thesis .
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   735
qed
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
   736
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   737
subsection%unimportant\<open>Analyticity at a point\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   738
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   739
lemma analytic_at_ball:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   740
  "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
   741
by (metis analytic_on_def singleton_iff)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   742
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   743
lemma analytic_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   744
    "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
   745
by (metis analytic_on_holomorphic empty_subsetI insert_subset)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   746
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   747
lemma analytic_on_analytic_at:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   748
    "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
   749
by (metis analytic_at_ball analytic_on_def)
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_two:
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   752
  "f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   753
   (\<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
   754
  (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
   755
proof
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   756
  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
   757
  then obtain s t
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   758
    where st: "open s" "z \<in> s" "f holomorphic_on s"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   759
              "open t" "z \<in> t" "g holomorphic_on t"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   760
    by (auto simp: analytic_at)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   761
  show ?rhs
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   762
    apply (rule_tac x="s \<inter> t" in exI)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   763
    using st
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   764
    apply (auto simp: Diff_subset holomorphic_on_subset)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   765
    done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   766
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
   767
  assume ?rhs
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   768
  then show ?lhs
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   769
    by (force simp add: analytic_at)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   770
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   771
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   772
subsection%unimportant\<open>Combining theorems for derivative with ``analytic at'' hypotheses\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   773
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
   774
lemma
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   775
  assumes "f analytic_on {z}" "g analytic_on {z}"
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   776
  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
   777
    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
   778
    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
   779
           f z * deriv g z + deriv f z * g z"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   780
proof -
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   781
  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
   782
    using assms by (metis analytic_at_two)
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   783
  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
   784
    apply (rule DERIV_imp_deriv [OF DERIV_add])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   785
    using s
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   786
    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   787
    done
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   788
  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
   789
    apply (rule DERIV_imp_deriv [OF DERIV_diff])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   790
    using s
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   791
    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   792
    done
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   793
  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
   794
    apply (rule DERIV_imp_deriv [OF DERIV_mult'])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   795
    using s
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   796
    apply (auto simp: holomorphic_on_open field_differentiable_def DERIV_deriv_iff_field_differentiable)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   797
    done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   798
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   799
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   800
lemma deriv_cmult_at:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   801
  "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
61848
9250e546ab23 New complex analysis material
paulson <lp15@cam.ac.uk>
parents: 61808
diff changeset
   802
by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   803
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   804
lemma deriv_cmult_right_at:
56370
7c717ba55a0b reorder Complex_Analysis_Basics; rename DD to deriv
hoelzl
parents: 56369
diff changeset
   805
  "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
61848
9250e546ab23 New complex analysis material
paulson <lp15@cam.ac.uk>
parents: 61808
diff changeset
   806
by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   807
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   808
subsection%unimportant\<open>Complex differentiation of sequences and series\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   809
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   810
(* TODO: Could probably be simplified using Uniform_Limit *)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   811
lemma has_complex_derivative_sequence:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   812
  fixes S :: "complex set"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   813
  assumes cvs: "convex S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   814
      and df:  "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   815
      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"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   816
      and "\<exists>x l. x \<in> S \<and> ((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   817
    shows "\<exists>g. \<forall>x \<in> S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   818
                       (g has_field_derivative (g' x)) (at x within S)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   819
proof -
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   820
  from assms obtain x l where x: "x \<in> S" and tf: "((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   821
    by blast
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   822
  { fix e::real assume e: "e > 0"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   823
    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
   824
      by (metis conv)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   825
    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"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   826
    proof (rule exI [of _ N], clarify)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   827
      fix n y h
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   828
      assume "N \<le> n" "y \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   829
      then have "cmod (f' n y - g' y) \<le> e"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   830
        by (metis N)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   831
      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
   832
        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
   833
      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
   834
        by (simp add: norm_mult [symmetric] field_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   835
    qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   836
  } note ** = this
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   837
  show ?thesis
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
   838
    unfolding has_field_derivative_def
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   839
  proof (rule has_derivative_sequence [OF cvs _ _ x])
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   840
    show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   841
      by (rule tf)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   842
  next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   843
      unfolding eventually_sequentially by (blast intro: **)
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
   844
  qed (metis has_field_derivative_def df)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   845
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   846
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   847
lemma has_complex_derivative_series:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   848
  fixes S :: "complex set"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   849
  assumes cvs: "convex S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   850
      and df:  "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   851
      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
   852
                \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   853
      and "\<exists>x l. x \<in> S \<and> ((\<lambda>n. f n x) sums l)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   854
    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))"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   855
proof -
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   856
  from assms obtain x l where x: "x \<in> S" and sf: "((\<lambda>n. f n x) sums l)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   857
    by blast
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   858
  { fix e::real assume e: "e > 0"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   859
    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
   860
            \<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
   861
      by (metis conv)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   862
    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"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   863
    proof (rule exI [of _ N], clarify)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   864
      fix n y h
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   865
      assume "N \<le> n" "y \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   866
      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
   867
        by (metis N)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   868
      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
   869
        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
   870
      then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   871
        by (simp add: norm_mult [symmetric] field_simps sum_distrib_left)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   872
    qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   873
  } note ** = this
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   874
  show ?thesis
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   875
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   876
  proof (rule has_derivative_series [OF cvs _ _ x])
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   877
    fix n x
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   878
    assume "x \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   879
    then show "((f n) has_derivative (\<lambda>z. z * f' n x)) (at x within S)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   880
      by (metis df has_field_derivative_def mult_commute_abs)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   881
  next show " ((\<lambda>n. f n x) sums l)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   882
    by (rule sf)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   883
  next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h"
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   884
      unfolding eventually_sequentially by (blast intro: **)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   885
  qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   886
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   887
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   888
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   889
lemma field_differentiable_series:
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   890
  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   891
  assumes "convex S" "open S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   892
  assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   893
  assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   894
  assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S"
68055
2cab37094fc4 more defer/prefer
paulson <lp15@cam.ac.uk>
parents: 67979
diff changeset
   895
  shows  "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)"
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   896
proof -
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   897
  from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   898
    unfolding uniformly_convergent_on_def by blast
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   899
  from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open)
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   900
  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)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   901
    by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   902
  then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   903
    "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
   904
  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   905
    by (simp add: has_field_derivative_def S)
69064
5840724b1d71 Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents: 68721
diff changeset
   906
  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   907
    by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   908
       (insert g, auto simp: sums_iff)
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   909
  thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   910
    by (auto simp: summable_def field_differentiable_def has_field_derivative_def)
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   911
qed
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61520
diff changeset
   912
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   913
subsection%unimportant\<open>Bound theorem\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   914
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
   915
lemma field_differentiable_bound:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   916
  fixes S :: "'a::real_normed_field set"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   917
  assumes cvs: "convex S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   918
      and df:  "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z within S)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   919
      and dn:  "\<And>z. z \<in> S \<Longrightarrow> norm (f' z) \<le> B"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   920
      and "x \<in> S"  "y \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   921
    shows "norm(f x - f y) \<le> B * norm(x - y)"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   922
  apply (rule differentiable_bound [OF cvs])
68239
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   923
  apply (erule df [unfolded has_field_derivative_def])
0764ee22a4d1 tidy up of Derivative
paulson <lp15@cam.ac.uk>
parents: 68055
diff changeset
   924
  apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   925
  done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   926
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   927
subsection%unimportant\<open>Inverse function theorem for complex derivatives\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   928
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   929
lemma has_field_derivative_inverse_basic:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   930
  shows "DERIV f (g y) :> f' \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   931
        f' \<noteq> 0 \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   932
        continuous (at y) g \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   933
        open t \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   934
        y \<in> t \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   935
        (\<And>z. z \<in> t \<Longrightarrow> f (g z) = z)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   936
        \<Longrightarrow> DERIV g y :> inverse (f')"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   937
  unfolding has_field_derivative_def
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   938
  apply (rule has_derivative_inverse_basic)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   939
  apply (auto simp:  bounded_linear_mult_right)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   940
  done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   941
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   942
lemma has_field_derivative_inverse_strong:
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   943
  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   944
  shows "DERIV f x :> f' \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   945
         f' \<noteq> 0 \<Longrightarrow>
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   946
         open S \<Longrightarrow>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   947
         x \<in> S \<Longrightarrow>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   948
         continuous_on S f \<Longrightarrow>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   949
         (\<And>z. z \<in> S \<Longrightarrow> g (f z) = z)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   950
         \<Longrightarrow> DERIV g (f x) :> inverse (f')"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   951
  unfolding has_field_derivative_def
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   952
  apply (rule has_derivative_inverse_strong [of S x f g ])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   953
  by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   954
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   955
lemma has_field_derivative_inverse_strong_x:
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   956
  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   957
  shows  "DERIV f (g y) :> f' \<Longrightarrow>
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   958
          f' \<noteq> 0 \<Longrightarrow>
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   959
          open S \<Longrightarrow>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   960
          continuous_on S f \<Longrightarrow>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   961
          g y \<in> S \<Longrightarrow> f(g y) = y \<Longrightarrow>
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   962
          (\<And>z. z \<in> S \<Longrightarrow> g (f z) = z)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   963
          \<Longrightarrow> DERIV g y :> inverse (f')"
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   964
  unfolding has_field_derivative_def
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   965
  apply (rule has_derivative_inverse_strong_x [of S g y f])
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   966
  by auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   967
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
   968
subsection%unimportant \<open>Taylor on Complex Numbers\<close>
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   969
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   970
lemma sum_Suc_reindex:
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   971
  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
   972
    shows  "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   973
by (induct n) auto
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   974
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   975
lemma field_taylor:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   976
  assumes S: "convex S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   977
      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)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   978
      and B: "\<And>x. x \<in> S \<Longrightarrow> norm (f (Suc n) x) \<le> B"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   979
      and w: "w \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   980
      and z: "z \<in> S"
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   981
    shows "norm(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
   982
          \<le> B * norm(z - w)^(Suc n) / fact n"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   983
proof -
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   984
  have wzs: "closed_segment w z \<subseteq> S" using assms
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   985
    by (metis convex_contains_segment)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   986
  { fix u
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   987
    assume "u \<in> closed_segment w z"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
   988
    then have "u \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   989
      by (metis wzs subsetD)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
   990
    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
   991
                      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
   992
              f (Suc n) u * (z-u) ^ n / (fact n)"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   993
    proof (induction n)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   994
      case 0 show ?case by simp
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   995
    next
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
   996
      case (Suc n)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
   997
      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
   998
                             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
   999
           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
  1000
           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
  1001
           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
  1002
        using Suc by simp
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1003
      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
  1004
      proof -
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1005
        have "(fact(Suc n)) *
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1006
             (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
  1007
               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
  1008
               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
  1009
            ((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
  1010
            ((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
  1011
            ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
63367
6c731c8b7f03 simplified definitions of combinatorial functions
haftmann
parents: 63332
diff changeset
  1012
          by (simp add: algebra_simps del: fact_Suc)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1013
        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
  1014
                         (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
  1015
                         (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
63367
6c731c8b7f03 simplified definitions of combinatorial functions
haftmann
parents: 63332
diff changeset
  1016
          by (simp del: fact_Suc)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1017
        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
  1018
                         (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
  1019
                         (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
63367
6c731c8b7f03 simplified definitions of combinatorial functions
haftmann
parents: 63332
diff changeset
  1020
          by (simp only: fact_Suc of_nat_mult ac_simps) simp
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1021
        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
  1022
          by (simp add: algebra_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1023
        finally show ?thesis
63367
6c731c8b7f03 simplified definitions of combinatorial functions
haftmann
parents: 63332
diff changeset
  1024
        by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact_Suc)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1025
      qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1026
      finally show ?case .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1027
    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
  1028
    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
  1029
                has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1030
               (at u within S)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
  1031
      apply (intro derivative_eq_intros)
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1032
      apply (blast intro: assms \<open>u \<in> S\<close>)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1033
      apply (rule refl)+
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1034
      apply (auto simp: field_simps)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1035
      done
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1036
  } note sum_deriv = this
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1037
  { fix u
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1038
    assume u: "u \<in> closed_segment w z"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1039
    then have us: "u \<in> S"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1040
      by (metis wzs subsetD)
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1041
    have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> norm (f (Suc n) u) * norm (u - z) ^ n"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1042
      by (metis norm_minus_commute order_refl)
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1043
    also have "... \<le> norm (f (Suc n) u) * norm (z - w) ^ n"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1044
      by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u])
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1045
    also have "... \<le> B * norm (z - w) ^ n"
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1046
      by (metis norm_ge_zero zero_le_power mult_right_mono  B [OF us])
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1047
    finally have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> B * norm (z - w) ^ n" .
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1048
  } note cmod_bound = this
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1049
  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
  1050
    by simp
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1051
  also have "\<dots> = f 0 z / (fact 0)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
  1052
    by (subst sum_zero_power) simp
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1053
  finally have "norm (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)))
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1054
                \<le> norm ((\<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
  1055
                        (\<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
  1056
    by (simp add: norm_minus_commute)
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1057
  also have "... \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)"
62534
6855b348e828 complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
paulson <lp15@cam.ac.uk>
parents: 62533
diff changeset
  1058
    apply (rule field_differentiable_bound
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1059
      [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1060
         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
  1061
    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
  1062
                  norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1063
    done
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1064
  also have "...  \<le> B * norm (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
  1065
    by (simp add: algebra_simps norm_minus_commute)
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1066
  finally show ?thesis .
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1067
qed
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1068
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1069
lemma complex_taylor:
68255
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1070
  assumes S: "convex S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1071
      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)"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1072
      and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1073
      and w: "w \<in> S"
009f783d1bac small clean-up of Complex_Analysis_Basics
paulson <lp15@cam.ac.uk>
parents: 68239
diff changeset
  1074
      and z: "z \<in> S"
66252
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1075
    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1076
          \<le> B * cmod(z - w)^(Suc n) / fact n"
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1077
  using assms by (rule field_taylor)
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1078
b73f94b366b7 some generalizations complex=>real_normed_field
immler
parents: 66089
diff changeset
  1079
62408
86f27b264d3d Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents: 62397
diff changeset
  1080
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
  1081
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1082
lemma complex_mvt_line:
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1083
  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
  1084
    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
  1085
proof -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1086
  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
  1087
    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
  1088
  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
  1089
  show ?thesis
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1090
    apply (cut_tac mvt_simple
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1091
                     [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
  1092
                      "\<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
  1093
    apply auto
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1094
    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
  1095
    apply (auto simp: closed_segment_def twz) []
67979
53323937ee25 new material about vec, real^1, etc.
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
  1096
    apply (intro derivative_eq_intros has_derivative_at_withinI, simp_all)
56369
2704ca85be98 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents: 56332
diff changeset
  1097
    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
  1098
    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
  1099
    done
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1100
qed
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1101
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1102
lemma complex_taylor_mvt:
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1103
  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
  1104
    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
  1105
            Re (f 0 z) =
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1106
            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
  1107
                (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
  1108
proof -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1109
  { fix u
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1110
    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
  1111
    have "(\<Sum>i = 0..n.
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1112
               (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
  1113
               (fact i)) =
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1114
          f (Suc 0) u -
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1115
             (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
  1116
             (fact (Suc n)) +
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1117
             (\<Sum>i = 0..n.
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1118
                 (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
  1119
                 (fact (Suc i)))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
  1120
       by (subst sum_Suc_reindex) simp
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1121
    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
  1122
             (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
  1123
             (fact (Suc n)) +
56238
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1124
             (\<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
  1125
                 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
  1126
                 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
  1127
      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
  1128
    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
  1129
             (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
  1130
             (fact (Suc n)) +
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1131
             f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63941
diff changeset
  1132
      by (subst sum_Suc_diff) auto
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1133
    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
  1134
      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
  1135
    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
  1136
                             - 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
  1137
                  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
  1138
    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
  1139
                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
  1140
      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
  1141
      apply (force intro: u assms)
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1142
      apply (rule refl)+
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 56889
diff changeset
  1143
      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
  1144
      done
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1145
  }
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1146
  then show ?thesis
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59615
diff changeset
  1147
    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
  1148
               "\<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
  1149
    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
  1150
    done
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1151
qed
5d147e1e18d1 a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents: 56223
diff changeset
  1152
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
  1153
69180
922833cc6839 Tagged some theories in HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 69064
diff changeset
  1154
subsection%unimportant \<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
  1155
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
  1156
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
  1157
    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
  1158
  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
  1159
    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
  1160
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
  1161
  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
  1162
  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
  1163
    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
  1164
    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
  1165
    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
  1166
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
  1167
  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
  1168
  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
  1169
    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
  1170
  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
  1171
  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
  1172
    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
  1173
    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
  1174
    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
  1175
      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
  1176
    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
  1177
      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
  1178
    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
  1179
      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
  1180
    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
  1181
      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
  1182
    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
  1183
      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
  1184
    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
  1185
      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
  1186
    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
  1187
      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
  1188
  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
  1189
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
  1190
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
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
  1192
    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
  1193
  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
  1194
    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
  1195
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
  1196
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
  1197
  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
  1198
  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
  1199
    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
  1200
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
  1201
  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
  1202
  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
  1203
  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
  1204
  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
  1205
    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
  1206
    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
  1207
      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
  1208
  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
  1209
    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
  1210
    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
  1211
          "\<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
  1212
      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
  1213
      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
  1214
    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
  1215
    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
  1216
      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
  1217
      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
  1218
         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
  1219
      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
  1220
        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
  1221
      have nz: "norm z \<le> norm z ^ Suc m"
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 60162
diff changeset
  1222
        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
  1223
      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
  1224
        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
  1225
      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
  1226
            \<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
  1227
        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
  1228
      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
  1229
        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
  1230
      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
  1231
        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
  1232
        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
  1233
        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
  1234
        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
  1235
        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
  1236
    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
  1237
    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
  1238
      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
  1239
  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
  1240
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
  1241
56215
fcf90317383d New complex analysis material
paulson <lp15@cam.ac.uk>
parents:
diff changeset
  1242
end