src/HOL/Analysis/Cauchy_Integral_Theorem.thy
changeset 68247 7344affc0bd4
parent 68239 0764ee22a4d1
child 68256 79c437817348
equal deleted inserted replaced
68245:37974ddde928 68247:7344affc0bd4
   285 
   285 
   286 ``The usual assumption in complex analysis texts is that a path \<open>\<gamma>\<close> should be piecewise
   286 ``The usual assumption in complex analysis texts is that a path \<open>\<gamma>\<close> should be piecewise
   287 continuously differentiable, which ensures that the path integral exists at least for any continuous
   287 continuously differentiable, which ensures that the path integral exists at least for any continuous
   288 f, since all piecewise continuous functions are integrable. However, our notion of validity is
   288 f, since all piecewise continuous functions are integrable. However, our notion of validity is
   289 weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a
   289 weaker, just piecewise differentiability... [namely] continuity plus differentiability except on a
   290 finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
   290 finite set ... [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
   291 the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
   291 the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
   292 can integrate all derivatives.''
   292 can integrate all derivatives.''
   293 
   293 
   294 "Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
   294 "Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
   295 Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.
   295 Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.