statement theorem
First fundamental theorem of calculus
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.
Explanations
L1 human
Let the area under the graph from to be a function of . Where is continuous, this area grows at the rate .
What this node needs for W1
- an inventory row: the row of the inventory that the node accounts for (0 of 1)
The writing levels say how complete the text of a node is. They do not measure its truth.
What this needs
To read this node, read these 28 nodes in this order. The foundations come first, and the list ends with this node.
- 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
What depends on this
7 nodes use this node, directly or through other nodes.
- Integration by substitution 0D37QFPEZE
- Trigonometric substitution 0EAR3KNRTN
- Area under a curve 0GXA8Z205E
- The integral of a continuous function is an antiderivative 0NC2A3HWGT
- Fundamental theorem of calculus 0NHGY0N0JB
- Tangent half-angle substitution 0W8ETY2AZ6
- Taylor's theorem with the integral remainder 0WJGR81HBD