Parametric integrals

Stream: sphere eversion

[Patrick Massot]

Thanks in particular to work on this project, mathlib knows that $x \mapsto \int_a^b F(x, s)\,ds$ and $t \mapsto \int_a^t F(s)\,ds$ are continuous (and even differentiable) functions under appropriate assumptions on $F$. But we to know the same for $(x, t) \mapsto \int_a^t F(x, s)\,ds$.

This should be rather straightforward for people knowing this area of mathlib or wanting to learn it. It doesn't depend on anything specific to the project.

[Patrick Massot]

I've been working on this topic yesterday and today but progress is very slow. Those interval integrals are rather painful (or maybe I simply don't know how to handle them). My progress is at https://github.com/leanprover-community/sphere-eversion/blob/master/src/parametric_interval_integral.lean. Lots of sorries remaining. I won't have any time tomorrow so everyone should feel free to unsorry that file.

[Patrick Massot]

I should say I hope all those sorries are trivial on paper, the actual maths is already there.

[Patrick Massot]

I finished continuity of parametric primitives. See in particular this lemma which is particular says that if $F : X \times \mathbb{R} \to E$ is continuous and $X$ is locally compact then $(t, x) \mapsto \int_a^t F(x, s)\,ds$ is continuous.

[Patrick Massot]

The monster lemma powering this is https://github.com/leanprover-community/sphere-eversion/blob/master/src/parametric_interval_integral.lean#L282-L295

[Patrick Massot]

Note that continuity with respect to $t$ or $x$ alone was already known, also thanks to this project (on top of other work of course).

[Oliver Nash]

Awesome!

[Patrick Massot]

The monster proof is not so awesome actually. It would be interesting to understand whether it could be easier.

[Oliver Nash]

It’s worth celebrating getting there even if there might be easier routes.

[Patrick Massot]

I think part of the difficulty is hard to avoid. Continuity doesn't imply integrability on the whole real line, so restricting to subintervals is unavoidable, and this causes of lot of the suffering.

[Patrick Massot]

What would be really nice would be to have tactics taking care of checking all stupid measurability and integrability assumptions and interval inclusions.

[Patrick Massot]

and also handling the almost everywhere bureaucracy. Applying lemmas such as docs#measure_theory.ae_restrict_of_ae_restrict_of_subset by hand (including a painful interval inclusion proof) is simply unbearable.

[Patrick Massot]

I reach another milestone about parametric integrals. has_fderiv_at_parametric_primitive_of_lip allows to differentiate

$$(x, t) \mapsto \int_a^t F(x, s)\,ds$$

This is yet another 100 lines long proof, despite the fact that we already have partial derivatives with respect to $x$ and $t$. We'll try to understand how to simplify such proofs.