Parametric Calculus

General-purpose lemmas for iterated Fréchet derivatives and parametric integrals, not yet available in Mathlib. Used as building blocks in the SchwartzNuclear proofs.

Main results

• norm_iteratedFDeriv_iteratedFDeriv — Currying isometry: composing two levels of iterated derivatives preserves norms.
• contDiff_schwartz_parametric_integral — Leibniz integral rule (C^∞): if a Schwartz function is integrated against another Schwartz function along a smooth parametric embedding, the result is C^∞ and derivatives commute with the integral.

Helper: currying isometry with NormedAddCommGroup instances

The continuousMultilinearCurryLeftEquiv is parameterized by SeminormedAddCommGroup instances, while LinearIsometryEquiv.norm_iteratedFDeriv_comp_left requires NormedAddCommGroup. We rebuild the isometry with explicit NormedAddCommGroup instances to resolve this diamond.

theorem norm_iteratedFDeriv_iteratedFDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (n l' : ℕ) (z : E) : ‖iteratedFDeriv ℝ n (iteratedFDeriv ℝ l' f) z‖ = ‖iteratedFDeriv ℝ (n + l') f z‖

Textbook: Currying isometry for iterated Fréchet derivatives.

‖iteratedFDeriv n (iteratedFDeriv l' f) z‖ = ‖iteratedFDeriv (n + l') f z‖

Proof by induction on l'. The key difficulty is a typeclass diamond: the SeminormedAddCommGroup instances on ContinuousMultilinearMap and ContinuousLinearMap differ from those derived from NormedAddCommGroup, preventing direct use of LinearIsometryEquiv.norm_iteratedFDeriv_comp_left. We resolve this by rebuilding the currying isometry with explicit NormedAddCommGroup instances via curryLeftLIE.

Leibniz integral rule for Schwartz integrands

The proof uses a "double induction" on I n y := ∫ t, D^n_y[Φ_t(t)](y):

1. I_diff: each I n is differentiable with fderiv = (curryLeftLIE n).symm ∘ I(n+1)
2. I_contDiff: ContDiff m (I n) by induction on m, shifting n
3. h_iter: iteratedFDeriv m Φ = I m by induction on m

The hι_meas hypothesis provides measurability of the parametric iterated derivatives t ↦ D^m_y[f(ι(·,t))](y). In all applications (e.g., ι = euclideanSnoc), this follows from joint smoothness of ι via Continuous.aestronglyMeasurable.

theorem contDiff_schwartz_parametric_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {H : Type u_2} [NormedAddCommGroup H] [NormedSpace ℝ H] (f : SchwartzMap E ℝ) (g : SchwartzMap ℝ ℝ) (ι : H → ℝ → E) (hι_smooth : ∀ (t : ℝ), ContDiff ℝ ↑⊤ fun (x : H) => ι x t) (hι_meas : ∀ (m : ℕ) (y : H), MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => iteratedFDeriv ℝ m (fun (y' : H) => f (ι y' t)) y) MeasureTheory.volume) (hι_bound : ∀ (m : ℕ), ∃ (C : ℝ), ∀ (y : H) (t : ℝ), ‖iteratedFDeriv ℝ m (fun (y' : H) => f (ι y' t)) y‖ ≤ C) : (ContDiff ℝ ↑⊤ fun (y : H) => ∫ (t : ℝ), f (ι y t) * g t) ∧ ∀ (m : ℕ) (y : H), iteratedFDeriv ℝ m (fun (y' : H) => ∫ (t : ℝ), f (ι y' t) * g t) y = ∫ (t : ℝ), iteratedFDeriv ℝ m (fun (y' : H) => f (ι y' t) * g t) y

Leibniz integral rule (C^∞, Schwartz integrand).

Given a Schwartz function f on E, a Schwartz function g on ℝ, and a parametric embedding ι : H → ℝ → E, if:

• for each t, y ↦ ι(y,t) is C^∞,
• for each m, t ↦ D^m_y[f(ι(·,t))](y) is ae-strongly-measurable, and
• for each derivative order m, ‖D^m_y[f(ι(·,t))](y)‖ is uniformly bounded,

then y ↦ ∫_t f(ι(y,t)) · g(t) dt is C^∞ and D^m commutes with ∫.

Reference: Folland, "Real Analysis", Theorem 2.27 (iterated version).