11 ms·
Calculus for mathematicians (1997) [pdf]
- eccstartup 11y agoI am amazed at seeing that the limit is defined by continuity. It is interesting.
- bumbledraven 11y ago99. Expository notes Common practice in calculus books is to define continuity using limits. I define limits using continuity; continuity is a simpler concept.
- eccstartup 11y agoAre they equivalent? Or both systems work smoothly?
- dirkt 11y agoContinuity in the topological sense implies continuity by limits. For topological spaces with a countable (local) basis, the converse is also true. So, in general it's not equivalent. For the reals etc., it is.
- cottonseed 11y agoThey are equivalent if you consider limits of nets rather than limits of sequences.
- bumbledraven 11y agoThey are logically equivalent for the reals. Search the web for [limits "in terms of continuity"].
- hudibras 11y agoDefinitely stashing this away in my time machine for when I travel back to the 17th century. Make both Leibniz and Newton cry...
- anon4 11y agoIf you're taking things like that back in time, make sure to translate them to French. Also, learn French. Not knowing French in the 17th century is like not knowing English today.
- eccstartup 11y agoI'm learning French. But where is the time machine?
- ghshephard 11y agoAlso, learn French in Canada, not France prior to your trip back in time. I've been told that Canadians speak French like someone from the 1600s, and those visitors (in 2015) from France find it archaic to the ear.
- mhartl 11y agoDid Newton speak French? I'd guess not (or not very well). His principal scientific works were written in Latin, which was the academic lingua franca of the day.
- amelius 11y agoHow difficult would it be to write this in a formal system? How much space would it take?
- madez 11y agoYou would need to get to the reals, which takes already a fair amount of time and includes a lot of machinery. Depending on how you constructed the reals, you might be able to reuse some concepts. So, it depends on where you start and which path you take. Also, arguing by reference to the choice of appropriate values is incomplete argumentation and so it won't be accepted by a formal system. You'd have to fill these holes. I'd suggest to start by evaluating the existing formalized constructions of the reals. I think it is not too hard.
- cottonseed 11y agoThe Coq standard library formalizes real analysis. Have a look at the "Reals" section: https://coq.inria.fr/library/ https://coq.inria.fr/library/
- jojo3000 11y agoEven defining the real numbers is already quite involved, for example in Isabelle/HOL it is introduced as quotient over Cauchy sequences: http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html http://isabelle.in.tum.de/dist/library/HOL/HOL/Real.html This is the classical way (and similar to HOL Light or HOL4). AFAIK in Coq the standard way is to introduce the reals axiomatically. The bottom theories in http://isabelle.in.tum.de/dist/library/HOL/HOL/ http://isabelle.in.tum.de/dist/library/HOL/HOL/ are all about classical real analysis, based on topology and real-normed vector spaces.
- mafribe 11y agoI wonder if the coinductive approach calculus by Pavlovic et al [1, 2] has been considered as a basis for formalisation. I secretly hope that I will one day get to teach calculus to computer scientists. In that case I would introduce reals as a coinductive data type, and the usual operations (such as differentiation, integration, solving differential equations) as stream operations. That should appeal to programmers, athough it would be weird for conventional mathematicians. [1] D. Pavlovic, M. Hölzl Escardo, Calculus in coinductive form. [2] D. Pavlovic, V. Pratt, The continuum as a final coalgebra.
- bandrami 11y agoThe hardest (ie, best) math prof I ever had (I was in EE, he was in the math department) used to say that "engineers can teach calculus, but their students cannot go on to teach calculus". I'm impressed by someone who knows a subject deeply enough to take that long of a view. Personally, I just like the engineering view of dx and dy as simply being new variables (with caveats that we immediately forget). Which is why I'll probably not teach calculus any time soon. But, still, the best "revelation" moment I had was when he off-handedly said "An integral is the inner product of a function and a suitably-dimensioned unit". Light bulb came on, and I "got" integration for the first time. Too bad they can't lead up to it that way in high school. (Side rant: why do they teach trig before calculus in high school? That's completely backwards. Trig is a bunch of arbitrary formulas if you don't have the calculus behind them.)
- k__ 11y agoMaybe to teach the people how to use formulas they didn't make up themself. This is the part of Math that most of us do after school.
- impendia 11y ago> Trig is a bunch of arbitrary formulas if you don't have the calculus behind them. Why do you claim this? You don't have to have seen calculus to appreciate how trig functions are defined, how to manipulate them, or how to use them in applications. As a math professor, I personally like the fact that we teach trig and exponential/logarithmic functions before calculus. They are (as you well know) exceedingly rich examples which illustrate why calculus is interesting and useful, and knowing them already enables the student to study calculus without excessive digressions.
- stephencanon 11y agosin and cos are the natural basis of solutions of y'' + y = 0. How do you define them?
- tarentel 11y ago
- jordigh 11y agoHm, I always thought Spivak was calculus for mathematicians.
- cottonseed 11y agoApostol, I would have said. That's what MIT's 18.014 Calculus with Theory uses, for example. http://ocw.mit.edu/courses/mathematics/18-014-calculus-with-theory-fall-2010/Syllabus/ http://ocw.mit.edu/courses/mathematics/18-014-calculus-with-...
- anon4 11y agoOne thing that bugs me about this, is that a lot of theorems seem to be formulated backwards. To give an example: Theorem 9.1. Let f be a continuous real-valued function. Let y be a real number. Let b ≤ c be real numbers with f(b) ≤ y ≤ f(c). Then f(x) = y for some x in [b, c]. Why is this well-formed? Once you say "Let y be a real number", I'm free to pick any real number, which means that there might not be a b and c such that f(b) ≤ y ≤ f(c). Now, I obviously understand what is said, but shouldn't this be formulated more like: Let f be a continuous real-valued function. Let b ≤ c be real numbers from the domain of f. Let y be a real number in the closed interval bounded by f(b) and f(c) ([f(b), f(c)] or [f(c), f(b)], depending on whether f(b) ≤ f(c) or not). Then there exists an x in [b, c] such, that f(x) = y. The way this and other theorems, definitions, etc. are formulated in the article bugs me, because I must go back and re-qualify variables based on information deduced from things introduced, after the variable in question was introduced.
- murbard2 11y agoThe "let" should really be read as "for all". If you do so, your objection disappears since quantifying over the empty always imply the consequent.
- tel 11y agoYou also need to translate "with" as a forall (pi binder) as well. Then, you'll merely note that the formula is unsatisfiable without demonstrating a proof that y is within the proper bounds.
- eli_gottlieb 11y agoOh good, so I'm not the only one whose mind tries to translate mathematical prose into the notation of dependent type theory!
- tel 11y agoSometimes your problem really does just call for a hammer :)
- murbard2 11y agoI was lucky enough that this is how I was taught calculus in high-school. It definitely wasn't easy at the time, but I feel for all the students for whom calculus is taught as a mindless set of algebraic rules. This focus on calculating derivatives as opposed to actually understanding the concept and why the calculations work that way is, I think, why so many struggle with it.
- WallWextra 11y agoIt was very DJB of him to use the gauge integral, which nobody else does.
- j2kun 11y agoAs much as I respect djb, the title is a huge misnomer. If you're a mathematician you want analysis and topology. You want definitions of continuity and differentiability that generalize nicely to arbitrary dimension, to manifolds, to Lie groups, to whatever. You want to marvel at the connections between certain special integrals and infinite sums, and you want to see the full construction of the real numbers for its own sake. You want a list of equivalent definitions of differentiability so you can get a better intuition and use whichever one is the nicest for what you're trying to do. In a very strong sense, writing a document that "focuses purely on calculus" is antithetical to mathematics.
- blahblah3 11y agoI remember the "concept" part of my high school calculus class. The teacher had us recite out loud the epsilon-delta definition of continuity until everybody memorized it so they could regurgitate it on the test. I always wondered why analogies and pictures weren't used more often: examples: A 100m sprint is a continuous function of time (f(t) = distance from starting line) because sprinters cant teleport. In fact it is uniformly continuous because people have a maximum speed. Beating usain bolt's record is a discontinuous function of completion time because f(world_record + epsilon) = 0 while f(world_record - epsilon) = 1. Fundamental theorem of calculus: If you want to know how fast a guy is running at time t, look at how much ground he covered in 1 second. To get more and more accurate, look at how far he traveled in 0.5 seconds and so on...
- ww2 11y agoDefinition 5.1/5.2 is interesting. It defines derivative at point c, not the derivative function of f. Note that f1(x) is not equal to f'(x) for all x, but f1(c) = f'(c).
- bumbledraven 11y agoYeah. The paper says: The derivative of f at c is written f'(c). The derivative of f, written f', is the function c -> f'(c). So the derivative (f') is the result of substituting c for x in f1. For example, if f1 = (x -> x + c) then we would have f' = (c -> c + c) = (c -> 2c).
- deleted 11y ago[deleted]
- ww2 11y agotry to get the derivative of sin(x) from his approach.
- bumbledraven 11y agohttp://math.stackexchange.com/questions/1303322/from-carath%C3%A9odory-derivative-definition-to-the-derivative-of-sinx http://math.stackexchange.com/questions/1303322/from-carath%...