First fundamental theorem of calculus
Builds on Mean value theorem for integralsAdditivity of the integral over intervalsDerivative
Statement
Let and let be Riemann integrable. Define for . Then is continuous on . If is continuous at , then is differentiable at and .
Remarks
If , then . So is Lipschitz continuous.
By additivity, is the average of over the interval between and . Continuity at makes this average tend to .
Mathlib states a strict form as intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right.
Reading path
To understand this page from the ground up, read these 28 pages in order. The foundations come first.
Show the path as a graph
- no evidence level
- Limit point of a set definition
- Partition of an interval definition
- Sequence definition
- Limit of a function definition
- Mesh of a partition definition
- Riemann sum definition
- Real sequence definition
- Subsequence definition
- Continuity at a point definition
- Derivative definition
- Riemann integrable function definition
- Bounded sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Continuous function definition
- Riemann integral definition
- Convergent sequence definition
- Monotone convergence theorem for sequences statement
- Every sequence has a monotone subsequence statement
- Intermediate value theorem statement
- Definite integral definition
- Bolzano–Weierstrass theorem statement
- Additivity of the integral over intervals statement
- Boundedness theorem statement
- Monotonicity of the integral statement
- Extreme value theorem statement
- Mean value theorem for integrals statement
- First fundamental theorem of calculus statement
Where this leads
15 pages build on this one.
- Integration by substitution
- Trigonometric substitution
- Area under a curve
- The integral of a continuous function is an antiderivative
- Fundamental theorem of calculus
- Tangent half-angle substitution
- Taylor's theorem with the integral remainder
- Arnold tongue
- Lebesgue's theorem on differentiability of monotone functions
- Peano kernel theorem
- Reduction of an initial value problem to a Volterra equation
- Differentiation operator as inverse of integration
- Cauchy formula for repeated integration
- Cantor function
- Volterra's function
Further reading
About this page
| Tag | 063H5KJC69 |
|---|---|
| URI | m2://063H5KJC69 |
| Kind | statement, theorem |
| Writing | W1 stated |
| MSC | 26A42 |
| Status | This copy of the site has no build data. Run m2 status 063H5KJC69. |
| Uses | Mean value theorem for integrals, Additivity of the integral over intervals, Derivative |
Markdown · JSON · Edit on GitHub
What this page needs for W2
- edge about out: the concepts that the statement is about (0 of 1)
- edge proves in: at least one proof node (0 of 1)
- edge instance_of or illustrates in: one example that shows the statement at work (0 of 1)
- explanation L2 (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.