Revision #1835 → #2993 · back to history
modifiedIndefinite integral / antiderivativef78185eb80d5
| Field | From #1835 | To #2993 |
|---|
| note | Mathlib has no named `antiderivative` definition; antiderivatives are stated via `HasDerivAt F' = f` hypotheses. | Mathlib has no named `antiderivative` constant; antiderivatives are expressed via `HasDerivAt F (f x) x` hypotheses. |
modifiedLine integral4ab2c3ff01e4
| Field | From #1835 | To #2993 |
|---|
| note | No general line integral over a curve is defined in Mathlib (no `curveIntegral` decl exists); only `intervalIntegral` over an interval and `circleIntegral` for circles. | No general line integral over a curve exists in Mathlib; only `intervalIntegral` (over an interval) and `circleIntegral` (over a circle). |
addedSum of fourth powers formulada366a44c436
modifiedMesh of a partition7b6ae7fbe1f8
| Field | From #1835 | To #2993 |
|---|
| note | Mathlib's BoxIntegral uses `distortion` and `isSubordinate` rather than a scalar mesh. | Mathlib's `BoxIntegral` uses `distortion` and `isSubordinate` rather than a scalar mesh. |
modifiedHenstock–Kurzweil integrale47c3630a08d
| Field | From #1835 | To #2993 |
|---|
| note | BoxIntegral with the Henstock filter is the gauge / Henstock–Kurzweil integral. | `BoxIntegral` with the Henstock filter is the gauge / Henstock–Kurzweil integral. |
addedRectangle methode66d3a3dc4ad
addedClenshaw–Curtis quadrature467876f01846
addedMonte Carlo integrationaea08a28a728