Integral over family of smooth functions is smooth

Stream: Is there code for X?

[Ben Eltschig]

For a smooth or $C^n$ function $f:U\times[0,1]\to F$ between normed spaces (maybe complete or finite-dimensional ones), do we have an easy way of proving that $\tilde f:U\to F,x\mapsto\int_0^1f(x,t)dt$ is also smooth / $C^n$? I.e. some version of the following:

import Mathlib

variable {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F]

example {f : E × ℝ → F} {u : Set E} {n : ℕ} (hf : ContDiffOn ℝ n f (u ×ˢ Set.Icc 0 1)) :
    ContDiffOn ℝ n (fun x ↦ ∫ t in 0..1, f (x, t)) u := by
  sorry

This is the last ingredient I'm missing for Hadamard's lemma, but unfortunately I'm not sure how to prove it with my limited knowledge about integration in mathlib. I've already tried searching loogle for lemmas mentioning both MeasureTheory.integral/intervalIntegral and ContDiff/ContDiffOn on loogle, but couldn't find anything. If this really does not exist yet, what would be the best way to go about proving it?

[Etienne Marion]

I guess the results in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ParametricIntegral.html should be extended to speak about ContDiff.

[Michael Rothgang]

Indeed! The sphere-eversion project has this (or something related) at https://github.com/leanprover-community/sphere-eversion/blob/master/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean

[Ben Eltschig]

Those links are both very helpful, thanks! I didn't know the term "parametric integral" for this before, maybe that's why I couldn't find it :sweat_smile:

[Michael Rothgang]

Actually, congratulations on nerd-sniping me. I just asked Floris about this file, and you should hopefully see a PR upstreaming most of this file tonight

[Michael Rothgang]

#30608 upstreams the first lemma from the sphere-eversion file (I'll write a proper PR description now).

[Michael Rothgang]

The next lemma requires another lemma, which I had ported as #12673, so I resurrected that PR. #30612 contains a cleaned up proof, but has two sorries left. @Ben Eltschig If you'd like to chime in, that is very welcome! Hopefully, all sorries are sufficiently self-contained --- if not, feel free to ask for more details!

[Yury G. Kudryashov]

BTW, are there volunteers to deduplicate https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ParametricIntegral.html and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ParametricIntervalIntegral.html ?

[Yury G. Kudryashov]

I like the latter more than the intervalIntegral API in the former, probably because I wrote it (I missed the fact that it was in the sphere eversion project).