antiderivative

Stream: new members

[Leonid Kimelfeld]

Hi. Is there definition of indefinite integral / antiderivative in lean4 mathlib?

[Yury G. Kudryashov]

fun b => ∫ x in a .. b, f x

[Yury G. Kudryashov]

What exactly do you want: the se of all antiderivatives? One antiderivative? A predicate saying that F is an antiderivative of f?

[Yury G. Kudryashov]

For the first, you can either use {F | ∀ x, HasDerivAt F (f x) x} (if you want it as a Set (Real → E)) or you need to introduce an appropriate Setoid (functions up to addition of a constant? of a piecewise constant on the complement of the set of singularities of f?) and deal with an element of the quotient space.

[Yury G. Kudryashov]

For one antiderivative, use the formula above. For the predicate, use ∀ x, HasDerivAt F (f x) x