C^n dependence of a parametric interval integral on its parameter

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #60, the regularity the Poincaré primitive needs for Darboux's theorem at order n.

If F : E → ℝ → G is jointly C^n on an open set containing U × [0, 1], with E finite-dimensional and G any normed space, then x ↦ ∫₀¹ F x t dt is C^n on U. The proof is by induction on n: the derivative of the integral is the integral of the partial derivative (intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, with a bound on a compact tube), and that derivative is C^{n−1} because, applied to any fixed vector, it is again a parametric integral of a jointly C^{n−1} integrand (contDiffOn_clm_apply, finite dimension). Mathlib at the pin has the C¹ step and the continuity, not the iteration.

• exists_closedBall_prod_Icc_subset — the compact tube around a point of U;
• ★ contDiffOn_intervalIntegral_of_contDiffOn — the theorem, for n ≤ ∞.

The codomain was generalised from ℝ to a normed space G for BACKLOG #159 (the Riesz projector along a gapped path is a matrix-valued parametric integral); the proof was unchanged.

References: Analysis/Calculus/DifferentialForm/Poincare.lean, Analysis/Matrix/RieszProjectorSmooth.lean (the consumers); specs/BACKLOG.md #60.

theorem exists_closedBall_prod_Icc_subset {E : Type u_1} [NormedAddCommGroup E] {U : Set E} (hU : IsOpen U) {W : Set (E × ℝ)} (hW : IsOpen W) (hUW : ∀ x ∈ U, ∀ t ∈ Set.Icc 0 1, (x, t) ∈ W) {x : E} (hx : x ∈ U) : ∃ ρ > 0, Metric.closedBall x ρ ⊆ U ∧ ∀ y ∈ Metric.closedBall x ρ, ∀ t ∈ Set.Icc 0 1, (y, t) ∈ W

A closed ball around x ∈ U, inside U, whose product with [0, 1] lies in the open W.

theorem contDiffOn_intervalIntegral_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ E] (k : ℕ) (F : E → ℝ → G) (U : Set E) : IsOpen U → ∀ (W : Set (E × ℝ)), IsOpen W → (∀ x ∈ U, ∀ t ∈ Set.Icc 0 1, (x, t) ∈ W) → ContDiffOn ℝ (↑k) (Function.uncurry F) W → ContDiffOn ℝ (↑k) (fun (x : E) => ∫ (t : ℝ) in 0..1, F x t) U

The induction behind contDiffOn_intervalIntegral_of_contDiffOn, on the order.

theorem contDiffOn_intervalIntegral_of_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ E] {n : ℕ∞} {F : E → ℝ → G} {U : Set E} (hU : IsOpen U) {W : Set (E × ℝ)} (hW : IsOpen W) (hUW : ∀ x ∈ U, ∀ t ∈ Set.Icc 0 1, (x, t) ∈ W) (hF : ContDiffOn ℝ (↑n) (Function.uncurry F) W) : ContDiffOn ℝ (↑n) (fun (x : E) => ∫ (t : ℝ) in 0..1, F x t) U

★ A parametric interval integral of a jointly C^n integrand is C^n in the parameter (n ≤ ∞, finite-dimensional parameter space): if F is C^n on an open set containing U × [0, 1], then x ↦ ∫₀¹ F x t dt is C^n on the open U.