Differentiation under the integral sign, to all orders

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #120, out of #92's split.

Mathlib differentiates a parametric integral once (hasDerivAt_integral_of_dominated_loc_of_deriv_le and its fderiv siblings). The corpus differentiates one to all orders, but only for an interval integral on a compact interval (ContDiffParametricIntervalIntegral.lean, #60), where the bounds come free from continuity on a compact set. For an integral over a general measure space there is no such shortcut and the bounds have to be hypotheses. This file supplies that.

• partialDeriv F k — the k-th derivative of F in its parameter, by recursion rather than through iteratedDeriv, so the induction below shifts the order with no API friction; ★ partialDeriv_eq_iteratedDeriv is the bridge for discharging bounds either way, and ★ partialDeriv_succ_left is the shift the induction runs on;
• ★★★ contDiffOn_integral_of_bound — the theorem: if each x ↦ F x a is C^n, each partialDeriv F k x is measurable, and each is bounded on an open U by an integrable function of a uniformly in the parameter, then x ↦ ∫ a, F x a is C^n on U;
• ★★ contDiff_integral_of_bound — the global corollary, and ★★ contDiffOn_integral_of_bound_all smoothness at every order.

The hypotheses are the statement

⚠️ The row that opened this warned that a version with hypotheses nobody can discharge would be worse than none, so they are chosen to be checkable: the bound is one integrable function per order, valid for every parameter in U — not a Lipschitz modulus, and not something per-point. The U is there because that is how such bounds actually arise: for a kernel like K ((x + y)/2, x − y) the majorant depends on where the parameter sits, so a bound uniform on a ball is available and a globally uniform one is not. ContDiffOn on an open set is exactly what that buys, and contDiff_integral_of_bound is the special case U = univ for the rarer situation where the bound really is global.

▸ The derivative formula is now exported too (added 2026-10-08, #125). The original version of this file recorded only the smoothness, with a scope note saying the identity was "a by-product of each induction step" that "nothing here needs". #122's decay half and #121(ii) both needed it — without a formula for ∂ᵏ(∫ F) there is nothing to move a polynomial weight onto — so ★★★ hasDerivAt_integral_of_bound states the first-order identity and ★★★ iteratedDeriv_integral_of_bound iterates it: on an open U, the n-th derivative of the integral is the integral of the n-th parameter derivative. iteratedDeriv_integral_of_bound_le is the every-order-up-to-n form a consumer wants, and integrable_partialDeriv is the integrability the formula is false without. The smoothness theorem now calls the first-order identity rather than re-proving it inline.

⚠️ Parameter in ℝ. The integration variable ranges over an arbitrary measure space, but the parameter is one-dimensional, which is what lets the proof use deriv throughout and keeps the bounds scalar. The fderiv version over a finite-dimensional parameter is the same induction with ContinuousLinearMap plumbing and is not done here.

References: Mathlib/Analysis/Calculus/ParametricIntegral.lean (the first derivative), ContDiffParametricIntervalIntegral.lean (#60, the compact-interval case at all orders); specs/BACKLOG.md #120, #92, #60, #88.

The parameter's iterated derivative

noncomputable def partialDeriv {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → α → E) : ℕ → ℝ → α → E

The k-th derivative of F in its first (parameter) slot.

Equations

• partialDeriv F 0 = F
• partialDeriv F k.succ = fun (x : ℝ) (a : α) => deriv (fun (x : ℝ) => partialDeriv F k x a) x

@[simp]

theorem partialDeriv_zero {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → α → E) : partialDeriv F 0 = F

theorem partialDeriv_succ {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → α → E) (k : ℕ) : partialDeriv F (k + 1) = fun (x : ℝ) (a : α) => deriv (fun (x : ℝ) => partialDeriv F k x a) x

theorem partialDeriv_eq_iteratedDeriv {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → α → E) (k : ℕ) (x : ℝ) (a : α) : partialDeriv F k x a = iteratedDeriv k (fun (x : ℝ) => F x a) x

★ The bridge to iteratedDeriv, so a user can discharge the bounds with either vocabulary.

theorem partialDeriv_succ_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → α → E) (k : ℕ) : partialDeriv (partialDeriv F 1) k = partialDeriv F (k + 1)

★ The shift the induction runs on: differentiating once and then k times is differentiating k + 1 times.

theorem contDiff_partialDeriv_one {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ → α → E} {n : ℕ} (hF : ∀ (a : α), ContDiff ℝ ↑(n + 1) fun (x : ℝ) => F x a) (a : α) : ContDiff ℝ ↑n fun (x : ℝ) => partialDeriv F 1 x a

The parameter-smoothness of F passes to its parameter derivative.

The theorem

One derivative, with the derivative

The first-order identity is proved here rather than inside the induction below, because #122's decay half and #121(ii) need the derivative, not only the smoothness, and a statement that discards it cannot be reused. The smoothness theorem then calls it.

theorem integrable_partialDeriv {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} {U : Set ℝ} {bound : ℕ → α → ℝ} {n k : ℕ} (hk : k ≤ n) (hmeas : ∀ k ≤ n, ∀ (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) (hint : ∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) (hbd : ∀ k ≤ n, ∀ x ∈ U, ∀ (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) {x : ℝ} (hx : x ∈ U) : MeasureTheory.Integrable (partialDeriv F k x) μ

The parameter derivatives are integrable, which the formula below is false without.

theorem hasDerivAt_integral_of_bound {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} {U : Set ℝ} {bound : ℕ → α → ℝ} {n : ℕ} (hn : 1 ≤ n) (hU : IsOpen U) (hsm : ∀ (a : α), ContDiff ℝ ↑n fun (x : ℝ) => F x a) (hmeas : ∀ k ≤ n, ∀ (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) (hint : ∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) (hbd : ∀ k ≤ n, ∀ x ∈ U, ∀ (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) {x : ℝ} (hx : x ∈ U) : HasDerivAt (fun (x : ℝ) => ∫ (a : α), F x a ∂μ) (∫ (a : α), partialDeriv F 1 x a ∂μ) x

★★★ Differentiation under the integral sign, with the derivative. The identity contDiffOn_integral_of_bound proves and throws away.

theorem contDiffOn_integral_of_bound {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} (n : ℕ) (F : ℝ → α → E) (U : Set ℝ) (bound : ℕ → α → ℝ) : IsOpen U → (∀ (a : α), ContDiff ℝ ↑n fun (x : ℝ) => F x a) → (∀ k ≤ n, ∀ (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) → (∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) → (∀ k ≤ n, ∀ x ∈ U, ∀ (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) → ContDiffOn ℝ (↑n) (fun (x : ℝ) => ∫ (a : α), F x a ∂μ) U

★★★ Differentiation under the integral sign, to all orders. If each x ↦ F x a is C^n in the parameter, each parameter derivative is measurable in a, and the k-th one is bounded on an open U by an integrable bound k uniformly in the parameter, then the integral is C^n on U.

theorem contDiff_integral_of_bound {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {n : ℕ} {F : ℝ → α → E} {bound : ℕ → α → ℝ} (hsm : ∀ (a : α), ContDiff ℝ ↑n fun (x : ℝ) => F x a) (hmeas : ∀ k ≤ n, ∀ (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) (hint : ∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) (hbd : ∀ k ≤ n, ∀ (x : ℝ) (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) : ContDiff ℝ ↑n fun (x : ℝ) => ∫ (a : α), F x a ∂μ

★★ The global corollary, for the rarer case where the bounds hold for every parameter.

theorem contDiffOn_integral_of_bound_all {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} {U : Set ℝ} {bound : ℕ → α → ℝ} (hU : IsOpen U) (hsm : ∀ (m : ℕ) (a : α), ContDiff ℝ ↑m fun (x : ℝ) => F x a) (hmeas : ∀ (k : ℕ) (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) (hint : ∀ (k : ℕ), MeasureTheory.Integrable (bound k) μ) (hbd : ∀ (k : ℕ), ∀ x ∈ U, ∀ (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) (m : ℕ) : ContDiffOn ℝ (↑m) (fun (x : ℝ) => ∫ (a : α), F x a ∂μ) U

★★ Smoothness at every order. Bounds at every order give C^m on U for every m, stated over ℕ so that no ∞-coercion enters the interface.

The interface is dischargeable

The row that opened this warned that hypotheses nobody can discharge would be worse than none, so here is a consumer that discharges all four of them, and is a theorem worth having on its own: convolution with a Schwartz function is smooth, for any integrable weight. Each hypothesis is met by one fact about Schwartz functions — the k-th derivative is bounded (decay 0 k) uniformly, which is exactly the "uniformly in the parameter" the bound family asks for.

theorem partialDeriv_sub_mul (f : SchwartzMap ℝ ℂ) (g : ℝ → ℂ) (k : ℕ) (x t : ℝ) : partialDeriv (fun (x t : ℝ) => f (x - t) * g t) k x t = iteratedDeriv k (⇑f) (x - t) * g t

The parameter derivatives of a translated Schwartz function against a weight.

theorem exists_bound_iteratedDeriv (f : SchwartzMap ℝ ℂ) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), ‖iteratedDeriv k (⇑f) x‖ ≤ C

An iterated derivative of a Schwartz function is bounded.

theorem contDiff_integral_schwartz_sub_mul (f : SchwartzMap ℝ ℂ) {g : ℝ → ℂ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (m : ℕ) : ContDiff ℝ ↑m fun (x : ℝ) => ∫ (t : ℝ), f (x - t) * g t

★★★ Convolution with a Schwartz function is smooth to every order, for any integrable weight — and every hypothesis of contDiffOn_integral_of_bound is discharged along the way.

The formula at every order

theorem iteratedDeriv_integral_of_bound {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} (n : ℕ) (F : ℝ → α → E) (U : Set ℝ) (bound : ℕ → α → ℝ) : IsOpen U → (∀ (a : α), ContDiff ℝ ↑n fun (x : ℝ) => F x a) → (∀ k ≤ n, ∀ (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) → (∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) → (∀ k ≤ n, ∀ x ∈ U, ∀ (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) → ∀ x ∈ U, iteratedDeriv n (fun (x : ℝ) => ∫ (a : α), F x a ∂μ) x = ∫ (a : α), partialDeriv F n x a ∂μ

★★★ The formula at every order. On an open U, the n-th derivative of the integral is the integral of the n-th parameter derivative. The induction is the same shift (partialDeriv_succ_left) the smoothness proof runs on, with the identity kept instead of discarded; locality of iteratedDeriv on the open set is what lets the first-order identity be substituted under the remaining derivatives.

theorem iteratedDeriv_integral_of_bound_le {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℝ → α → E} {U : Set ℝ} {bound : ℕ → α → ℝ} {n : ℕ} (hU : IsOpen U) (hsm : ∀ (a : α), ContDiff ℝ ↑n fun (x : ℝ) => F x a) (hmeas : ∀ k ≤ n, ∀ (x : ℝ), MeasureTheory.AEStronglyMeasurable (partialDeriv F k x) μ) (hint : ∀ k ≤ n, MeasureTheory.Integrable (bound k) μ) (hbd : ∀ k ≤ n, ∀ x ∈ U, ∀ (a : α), ‖partialDeriv F k x a‖ ≤ bound k a) {k : ℕ} (hk : k ≤ n) {x : ℝ} (hx : x ∈ U) : iteratedDeriv k (fun (x : ℝ) => ∫ (a : α), F x a ∂μ) x = ∫ (a : α), partialDeriv F k x a ∂μ

★★ The formula at every order up to n, which is the form a consumer wants.