Differentiation under the integral sign over a finite-dimensional parameter

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #124, out of #121(ii).

#120 did this for a one-dimensional parameter, deliberately: its scope note records that the fderiv version "is the same induction with ContinuousLinearMap plumbing and is not done here". #121(ii) is what wants the general case — the joint Schwartz claim needs differentiating in two variables at once — so here it is, for a parameter in any normed space.

The interface is directional, and that is the whole design

#124's row warned that the hypothesis-design question #120 flagged "returns in harder form: a per-order, locally-uniform bound on a multilinear norm". It does not have to. Bounding iteratedFDeriv means bounding a multilinear map, which drags currying equivalences through every step; bounding iterated directional derivatives keeps every hypothesis valued in E, and the recursion is then literally list-append:

• dirDeriv F hs — differentiate F in the directions hs, innermost last, by recursion on the list, with ★ dirDeriv_append_singleton the shift the induction runs on;
• ★★★ contDiffOn_integral_of_dirBound — the theorem: if each x ↦ F x a is C^n, each directional derivative of order ≤ n is measurable in a, and the one along hs is bounded on an open U by (∏ ‖hᵢ‖)·bound hs.length a with each bound k integrable, then x ↦ ∫ a, F x a is C^n on U;
• ★★ contDiff_integral_of_dirBound — the global corollary, and ★★ contDiffOn_integral_of_dirBound_all smoothness at every order;
• ★★★ hasFDerivAt_integral_of_bound and ★★ fderiv_integral_apply_of_bound — the first-order identity, which the induction proves and the smoothness statement discards. Exported for #126 with the weakest hypotheses that give it — differentiability of each slice, not smoothness — and in directional form; the induction now calls it rather than rebuilding it;
• ★★★ norm_iteratedFDeriv_integral_le — the bound at every order: under the same hypotheses, ‖iteratedFDeriv ℝ n (∫ a, F · a) x‖ ≤ ∫ a, bound n a on U, by an induction that peels the last direction (iteratedFDeriv_apply_succ_last) and substitutes the first-order identity under the remaining derivatives (Filter.EventuallyEq.iteratedFDeriv_eq, which Mathlib has only for iteratedFDerivWithin). This is the shape a Schwartz seminorm estimate asks for;
• ★★ norm_dirDeriv_le and ★★ contDiffOn_integral_of_iteratedFDeriv_bound — the multilinear interface, as a corollary of the directional one. Added after #121(ii) tried to consume this file and could not: SchwartzMap.decay gives bounds on iteratedFDeriv, so without the bridge the directional hypotheses were not dischargeable from Schwartz data and the file was unusable by the row it was built for. The bridge also makes the header's claim honest — the directional form is easier to meet and strictly more general, since the multilinear form follows from it.

The product ∏ ‖hᵢ‖ is what makes the bound family shift cleanly: appending one direction h multiplies it by ‖h‖ and raises the order by one, so the inner call runs with fun k a => ‖h‖ · bound (k + 1) a, still integrable.

Honest scope

⚠️ One hypothesis is unavoidably operator-valued. Mathlib's hasFDerivAt_integral_of_dominated_of_fderiv_le takes the derivative as a map into H →L[ℝ] E, so strong measurability of a ↦ fderiv ℝ (F · a) x is required and cannot be reduced to directional data. It appears as hmeasD, indexed the same way, and is closed under the recursion for the same list-append reason.

⚠️ The bound family must be nonnegative (hb0). #120 needed no such hypothesis, because its one-dimensional engine takes a bound on ‖F' x a‖ directly; here the directional bounds have to be turned into an operator-norm bound through opNorm_le_bound, which is false for a negative constant when H is trivial. It is one line to discharge for any bound family anyone builds.

⚠️ No formula for the derivatives, as in #120. Amended 2026-10-08 (#126). The first-order identity is now exported, and at higher order what is exported is the bound it implies, not the identity. The identity at order n would need the iterated derivative of the integral as a multilinear map — the plumbing this file exists to avoid — and no consumer has wanted it: a Schwartz estimate wants a scalar bound.

⚠️ The bound must be locally uniform in the parameter, which is what U is for: a bound uniform on a ball is what kernels actually supply, and contDiff_integral_of_dirBound is the U = univ special case.

References: ContDiffParametricIntegral.lean (#120, the one-dimensional case), ContDiffParametricIntervalIntegral.lean (#60, whose directional recursion this follows), Mathlib/Analysis/Calculus/ParametricIntegral.lean; specs/BACKLOG.md #124, #120, #121, #60.

The weight a list of directions carries

noncomputable def dirWeight {H : Type u_1} [NormedAddCommGroup H] (hs : List H) : ℝ

The product of the directions' norms, the weight the bound family carries.

Equations

• dirWeight hs = (List.map (fun (h : H) => ‖h‖) hs).prod

@[simp]

theorem dirWeight_nil {H : Type u_1} [NormedAddCommGroup H] : dirWeight [] = 1

theorem dirWeight_nonneg {H : Type u_1} [NormedAddCommGroup H] (hs : List H) : 0 ≤ dirWeight hs

theorem dirWeight_append_singleton {H : Type u_1} [NormedAddCommGroup H] (hs : List H) (h : H) : dirWeight (hs ++ [h]) = dirWeight hs * ‖h‖

Iterated directional derivatives in the parameter

noncomputable def dirDeriv {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) : List H → H → α → E

dirDeriv F hs differentiates F in its parameter along the directions hs, the head of the list being the outermost derivative. Every value is in E, which is what keeps the interface free of multilinear maps.

Equations

• dirDeriv F [] = F
• dirDeriv F (h :: hs) = fun (x : H) (a : α) => (fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) h

@[simp]

theorem dirDeriv_nil {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) : dirDeriv F [] = F

theorem dirDeriv_cons {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) (h : H) (hs : List H) : dirDeriv F (h :: hs) = fun (x : H) (a : α) => (fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) h

theorem dirDeriv_append_singleton {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : H → α → E) (h : H) (hs : List H) : dirDeriv (dirDeriv F [h]) hs = dirDeriv F (hs ++ [h])

★ The shift the induction runs on. Differentiating along h first and then along hs is differentiating along hs ++ [h].

The theorem

The first-order identity, which the induction needs and a consumer wants

The induction below proves fderiv (∫ a, F · a) x = ∫ a, fderiv (F · a) x at each step and then keeps only the smoothness. #125 made that identity an exported theorem for #120's one-dimensional parameter; here it is for a parameter in any normed space, stated with the weakest hypotheses that give it — differentiability of each slice, not smoothness — so that the induction can call it instead of rebuilding it.

theorem integrable_of_bound {H : Type u_1} {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : H → α → E} {U : Set H} {b₀ : α → ℝ} (hmeas : ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => F x a) μ) (hint₀ : MeasureTheory.Integrable b₀ μ) (hbd₀ : ∀ x ∈ U, ∀ (a : α), ‖F x a‖ ≤ b₀ a) {x : H} (hx : x ∈ U) : MeasureTheory.Integrable (fun (a : α) => F x a) μ

The integrand is integrable wherever the order-zero bound holds, which every statement here needs.

theorem hasFDerivAt_integral_of_bound {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : H → α → E} {U : Set H} {b₀ b₁ : α → ℝ} (hU : IsOpen U) (hdiff : ∀ (a : α), Differentiable ℝ fun (y : H) => F y a) (hmeas : ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => F x a) μ) (hmeasD : ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => F y a) x) μ) (hint₀ : MeasureTheory.Integrable b₀ μ) (hint₁ : MeasureTheory.Integrable b₁ μ) (hbd₀ : ∀ x ∈ U, ∀ (a : α), ‖F x a‖ ≤ b₀ a) (hbd₁ : ∀ x ∈ U, ∀ (a : α), ‖fderiv ℝ (fun (y : H) => F y a) x‖ ≤ b₁ a) {x : H} (hx : x ∈ U) : HasFDerivAt (fun (x : H) => ∫ (a : α), F x a ∂μ) (∫ (a : α), fderiv ℝ (fun (y : H) => F y a) x ∂μ) x

★★★ Differentiation under the integral sign over a normed parameter, with the derivative kept. The identity contDiffOn_integral_of_dirBound proves and discards.

theorem integrable_fderiv_of_bound {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : H → α → E} {U : Set H} {b₁ : α → ℝ} (hmeasD : ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => F y a) x) μ) (hint₁ : MeasureTheory.Integrable b₁ μ) (hbd₁ : ∀ x ∈ U, ∀ (a : α), ‖fderiv ℝ (fun (y : H) => F y a) x‖ ≤ b₁ a) {x : H} (hx : x ∈ U) : MeasureTheory.Integrable (fun (a : α) => fderiv ℝ (fun (y : H) => F y a) x) μ

The first derivative is integrable, which is what lets the identity above be evaluated at a direction.

theorem fderiv_integral_apply_of_bound {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : H → α → E} {U : Set H} {b₀ b₁ : α → ℝ} (hU : IsOpen U) (hdiff : ∀ (a : α), Differentiable ℝ fun (y : H) => F y a) (hmeas : ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => F x a) μ) (hmeasD : ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => F y a) x) μ) (hint₀ : MeasureTheory.Integrable b₀ μ) (hint₁ : MeasureTheory.Integrable b₁ μ) (hbd₀ : ∀ x ∈ U, ∀ (a : α), ‖F x a‖ ≤ b₀ a) (hbd₁ : ∀ x ∈ U, ∀ (a : α), ‖fderiv ℝ (fun (y : H) => F y a) x‖ ≤ b₁ a) {x : H} (hx : x ∈ U) (h : H) : (fderiv ℝ (fun (x : H) => ∫ (a : α), F x a ∂μ) x) h = ∫ (a : α), dirDeriv F [h] x a ∂μ

★★ The directional form of the identity, in this file's own vocabulary: no operator-valued integral survives in the statement.

theorem contDiffOn_integral_of_dirBound {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ H] (n : ℕ) (F : H → α → E) (U : Set H) (bound : ℕ → α → ℝ) : IsOpen U → (∀ (a : α), ContDiff ℝ ↑n fun (x : H) => F x a) → (∀ (hs : List H), hs.length ≤ n → ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => dirDeriv F hs x a) μ) → (∀ (hs : List H), hs.length < n → ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) μ) → (∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) → (∀ k ≤ n, ∀ (a : α), 0 ≤ bound k a) → (∀ (hs : List H), hs.length ≤ n → ∀ x ∈ U, ∀ (a : α), ‖dirDeriv F hs x a‖ ≤ dirWeight hs * bound hs.length a) → ContDiffOn ℝ (↑n) (fun (x : H) => ∫ (a : α), F x a ∂μ) U

★★★ Differentiation under the integral sign to all orders, over a parameter in any normed space. The hypotheses are directional throughout, so nothing here is valued in a space of multilinear maps except hmeasD, which Mathlib's first-derivative theorem forces.

theorem contDiff_integral_of_dirBound {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ H] {n : ℕ} {F : H → α → E} {bound : ℕ → α → ℝ} (hsm : ∀ (a : α), ContDiff ℝ ↑n fun (x : H) => F x a) (hmeas : ∀ (hs : List H), hs.length ≤ n → ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => dirDeriv F hs x a) μ) (hmeasD : ∀ (hs : List H), hs.length < n → ∀ (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) μ) (hint : ∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) (hb0 : ∀ k ≤ n, ∀ (a : α), 0 ≤ bound k a) (hbd : ∀ (hs : List H), hs.length ≤ n → ∀ (x : H) (a : α), ‖dirDeriv F hs x a‖ ≤ dirWeight hs * bound hs.length a) : ContDiff ℝ ↑n fun (x : H) => ∫ (a : α), F x a ∂μ

★★ The global corollary, for bounds that hold at every parameter.

theorem contDiffOn_integral_of_dirBound_all {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ H] {F : H → α → E} {U : Set H} {bound : ℕ → α → ℝ} (hU : IsOpen U) (hsm : ∀ (m : ℕ) (a : α), ContDiff ℝ ↑m fun (x : H) => F x a) (hmeas : ∀ (hs : List H) (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => dirDeriv F hs x a) μ) (hmeasD : ∀ (hs : List H) (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) μ) (hint : ∀ (k : ℕ), MeasureTheory.Integrable (bound k) μ) (hb0 : ∀ (k : ℕ) (a : α), 0 ≤ bound k a) (hbd : ∀ (hs : List H), ∀ x ∈ U, ∀ (a : α), ‖dirDeriv F hs x a‖ ≤ dirWeight hs * bound hs.length a) (m : ℕ) : ContDiffOn ℝ (↑m) (fun (x : H) => ∫ (a : α), F x a ∂μ) U

★★ Smoothness at every order, stated over ℕ so that no ∞-coercion enters the interface.

The multilinear interface, as a corollary of the directional one

This file's header claims the directional hypotheses are easier to meet than multilinear ones. That is only worth claiming if the multilinear form follows, so here it does. The bridge is that an iterated directional derivative is bounded by the iterated total derivative times the product of the directions' norms — proved by peeling the innermost direction, which is what dirDeriv_append_singleton is for.

theorem norm_applyCLM_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : H) : ‖(ContinuousLinearMap.apply ℝ E) h‖ ≤ ‖h‖

theorem norm_dirDeriv_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : List H) (F : H → α → E) : (∀ (a : α), ContDiff ℝ ↑⊤ fun (y : H) => F y a) → ∀ (x : H) (a : α), ‖dirDeriv F hs x a‖ ≤ ‖iteratedFDeriv ℝ hs.length (fun (y : H) => F y a) x‖ * dirWeight hs

★★ A directional derivative is bounded by the total one. The induction peels the innermost direction through dirDeriv_append_singleton, turns the evaluation into a left composition with ContinuousLinearMap.apply (ContinuousLinearMap.iteratedFDeriv_comp_left), and puts the extra order back with norm_iteratedFDeriv_fderiv. Smoothness is assumed outright, which is what removes all order bookkeeping and is what a Schwartz integrand supplies.

theorem contDiffOn_integral_of_iteratedFDeriv_bound {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ H] {F : H → α → E} {U : Set H} {bound : ℕ → α → ℝ} (hU : IsOpen U) (hsm : ∀ (a : α), ContDiff ℝ ↑⊤ fun (x : H) => F x a) (hmeas : ∀ (hs : List H) (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => dirDeriv F hs x a) μ) (hmeasD : ∀ (hs : List H) (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) μ) (hint : ∀ (k : ℕ), MeasureTheory.Integrable (bound k) μ) (hb0 : ∀ (k : ℕ) (a : α), 0 ≤ bound k a) (hbd : ∀ (k : ℕ), ∀ x ∈ U, ∀ (a : α), ‖iteratedFDeriv ℝ k (fun (y : H) => F y a) x‖ ≤ bound k a) (m : ℕ) : ContDiffOn ℝ (↑m) (fun (x : H) => ∫ (a : α), F x a ∂μ) U

★★ The multilinear form of this file's theorem, for a user whose bounds come from iteratedFDeriv — which is what SchwartzMap.decay gives. It is a corollary of the directional form, which is the claim the header makes.

The bound at every order, which is what a Schwartz estimate asks for

The first-order identity above is not enough for a consumer: a Schwartz seminorm estimate needs ‖iteratedFDeriv ℝ n (∫ a, F · a) x‖, and stating the identity at order n would need the iterated derivative of the integral as a multilinear map — exactly the plumbing this file exists to avoid. The bound is scalar, follows from the first-order identity by the same list-append induction, and is what #126 consumes.

The peel is iteratedFDeriv_apply_succ_last: Mathlib's iteratedFDeriv_succ_apply_right peels one order into a function valued in H →L[ℝ] E, and composing with evaluation at the last direction puts the value back in E.

theorem Filter.EventuallyEq.iteratedFDeriv_eq {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : H → E} {x : H} (h : f =ᶠ[nhds x] g) (n : ℕ) : iteratedFDeriv ℝ n f x = iteratedFDeriv ℝ n g x

Two functions that agree near a point have the same iterated derivatives there. Mathlib has the iteratedFDerivWithin version only.

theorem iteratedFDeriv_apply_succ_last {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : H → E} {x : H} {n : ℕ} (hf : ContDiffAt ℝ (↑(n + 1)) f x) (v : Fin (n + 1) → H) : (iteratedFDeriv ℝ (n + 1) f x) v = (iteratedFDeriv ℝ n (fun (y : H) => (fderiv ℝ f y) (v (Fin.last n))) x) (Fin.init v)

One order of iteratedFDeriv, applied to a tuple, is the iteratedFDeriv of one order less of the derivative along the tuple's last direction — the same innermost-first peeling dirDeriv_append_singleton performs, and for the same reason: the head of a tuple is the outermost derivative, which is not of this form.

theorem norm_iteratedFDeriv_integral_le {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℝ H] {α : Type u_2} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ H] (n : ℕ) (F : H → α → E) (U : Set H) (bound : ℕ → α → ℝ) : IsOpen U → (∀ (m : ℕ) (a : α), ContDiff ℝ ↑m fun (x : H) => F x a) → (∀ (hs : List H) (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => dirDeriv F hs x a) μ) → (∀ (hs : List H) (x : H), MeasureTheory.AEStronglyMeasurable (fun (a : α) => fderiv ℝ (fun (y : H) => dirDeriv F hs y a) x) μ) → (∀ (k : ℕ), MeasureTheory.Integrable (bound k) μ) → (∀ (k : ℕ) (a : α), 0 ≤ bound k a) → (∀ (hs : List H), ∀ x ∈ U, ∀ (a : α), ‖dirDeriv F hs x a‖ ≤ dirWeight hs * bound hs.length a) → ∀ x ∈ U, ‖iteratedFDeriv ℝ n (fun (x : H) => ∫ (a : α), F x a ∂μ) x‖ ≤ ∫ (a : α), bound n a ∂μ

★★★ The iterated derivative of the integral obeys the bound family, at every order. With the same hypotheses that make the integral smooth, ‖iteratedFDeriv ℝ n (∫ a, F · a) x‖ ≤ ∫ a, bound n a on U. The induction peels the last direction, replaces the derivative of the integral by the integral of the directional derivative (the identity above, valid on all of the open U, hence substitutable under the remaining derivatives), and calls itself on dirDeriv F [h] with the bound family shifted exactly as the smoothness proof shifts it.