Zulip Chat Archive

Stream: sphere eversion

Topic: Parametric integrals

Patrick Massot (Oct 08 2021 at 15:36):

Thanks in particular to work on this project, mathlib knows that xabF(x,s)dsx \mapsto \int_a^b F(x, s)\,ds and tatF(s)dst \mapsto \int_a^t F(s)\,ds are continuous (and even differentiable) functions under appropriate assumptions on FF. But we to know the same for (x,t)atF(x,s)ds(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 (Oct 13 2021 at 16:05):

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 (Oct 13 2021 at 16:06):

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

Patrick Massot (Oct 20 2021 at 19:44):

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

Patrick Massot (Oct 20 2021 at 19:44):

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

Patrick Massot (Oct 20 2021 at 19:45):

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

Oliver Nash (Oct 20 2021 at 19:56):


Patrick Massot (Oct 20 2021 at 19:57):

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

Oliver Nash (Oct 20 2021 at 20:04):

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

Patrick Massot (Oct 20 2021 at 20:08):

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 (Oct 20 2021 at 20:08):

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 (Oct 20 2021 at 20:11):

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 (Nov 06 2021 at 12:24):

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

(x,t)atF(x,s)ds(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 xx and tt. We'll try to understand how to simplify such proofs.

Last updated: Dec 20 2023 at 11:08 UTC