Parametric interval integrals

Stream: maths

[Yury G. Kudryashov]

We have 2 versions of the theorem about parametric interval integrals:

• docs#intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip written by in in Lean 3, see !3#10404
• docs#hasFDerivAt_integral_of_dominated_loc_of_lip_interval backported from the sphere eversion project in #10004

The backported version doesn't work for complex derivatives. OTOH, my version has heavier imports for no good reason.

[Yury G. Kudryashov]

(note: I don't remember how much of "written by me" was "backported"; anyway, it's a simple wrapper over Patrick's version)

[Yury G. Kudryashov]

BTW, the docstrings never explain what's the difference in the assumptions between the primed and the non-primed version of the main theorem.

[Damiano Testa]

Yury G. Kudryashov said:

BTW, the docstrings never explain what's the difference in the assumptions between the primed and the non-primed version of the main theorem.

Should the docPrime linter be revised/restarted?

[Yury G. Kudryashov]

Wouldn't help in this case. The primed version has a doc string, but it doesn't discuss the difference with the non primed version.

[Patrick Massot]

I can confirm the sphere eversion proof uses the second one and not the first one.

[Patrick Massot]

It really looks like this was PRed twice from the sphere eversion project.

[Yury G. Kudryashov]

Patrick Massot said:

It really looks like this was PRed twice from the sphere eversion project.

As you can see from the discussion in my old PR, first I wrote my version based on the backported parametric_integral.lean instead of backporting, then it was backported without using my version.