statement theorem
Second fundamental theorem of calculus
Statement
Let , and let be continuous on and differentiable on . Assume that extends to a Riemann integrable function on . Then
Remarks
For a partition , the mean value theorem gives tags with . So is a Riemann sum of for each partition.
One writes .
The hypothesis that is integrable is needed. Some differentiable functions have derivatives that are not Riemann integrable.
Mathlib states it as intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le.
Explanations
L1 human
To integrate , find a function with derivative . The integral is the change of from to .
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 27 nodes in this order. The foundations come first, and the list ends with this node.
- no evidence level
- Limit point of a set definition
- Local maximum definition
- Partition of an interval definition
- Sequence definition
- Limit of a function definition
- Local minimum 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
- Fermat's theorem on stationary points statement
- Convergent sequence definition
- Monotone convergence theorem for sequences statement
- Every sequence has a monotone subsequence statement
- Bolzano–Weierstrass theorem statement
- Boundedness theorem statement
- Extreme value theorem statement
- Rolle's theorem statement
- Mean value theorem statement
- Second fundamental theorem of calculus statement
What depends on this
22 nodes use this node, directly or through other nodes.
- Euler–Mascheroni constant 00C5P9JZBK
- Reduction formula 012RYET5E2
- Integral of exp(-x) over the half line 039JAF7ZAN
- Integral of cosine 04WTBQ7APQ
- Harmonic numbers grow like log n 05S2GSPMGA
- Integral of the exponential function 06D0EWR2DV
- Integration by parts 08Y1BBQTK9
- Integration by substitution 0D37QFPEZE
- Trigonometric substitution 0EAR3KNRTN
- The gamma function extends the factorial 0FDCW77H44
- Area under a curve 0GXA8Z205E
- Integral of sine 0GXCXCX3QN
- Dirichlet integral 0GZNSHMG4Q
- Integral of 1/x 0K1N1Y4EGZ
- Stirling's formula 0KC0F51T6A
- Fundamental theorem of calculus 0NHGY0N0JB
- Integral of a power 0Q3HYFT9RQ
- Improper integral of x^p on an unbounded interval 0VGKB2NC4T
- Tangent half-angle substitution 0W8ETY2AZ6
- Integration by partial fractions 0WBTWFXJQG
- Taylor's theorem with the integral remainder 0WJGR81HBD
- Wallis product 0XCYA4YERS
Sources
What links here
Used by
- Integral of cosine 04WTBQ7APQ
- Integral of the exponential function 06D0EWR2DV
- Integration by parts 08Y1BBQTK9
- Integration by substitution 0D37QFPEZE
- Integral of sine 0GXCXCX3QN
- Integral of 1/x 0K1N1Y4EGZ
- Fundamental theorem of calculus 0NHGY0N0JB
- Integral of a power 0Q3HYFT9RQ