Derivatives of integrals depending on parameters #
A parametric integral is a function with shape f = λ x : H, ∫ a : α, F x a ∂μ
for some
F : H → α → E
, where H
and E
are normed spaces and α
is a measured space with measure μ
.
We already know from continuous_of_dominated
in Mathlib/MeasureTheory/Integral/Bochner.lean
how
to guarantee that f
is continuous using the dominated convergence theorem. In this file,
we want to express the derivative of f
as the integral of the derivative of F
with respect
to x
.
Main results #
As explained above, all results express the derivative of a parametric integral as the integral of a derivative. The variations come from the assumptions and from the different ways of expressing derivative, especially Fréchet derivatives vs elementary derivative of function of one real variable.

hasFDerivAt_integral_of_dominated_loc_of_lip
: this version assumes thatF x
is aemeasurable for x nearx₀
,F x₀
is integrable,fun x ↦ F x a
has derivativeF' a : H →L[ℝ] E
atx₀
which is aemeasurable,λ x, F x a
is locally Lipschitz nearx₀
for almost everya
, with a Lipschitz bound which is integrable with respect toa
.
A subtle point is that the "near x₀" in the last condition has to be uniform in
a
. This is controlled by a positive numberε
. 
hasFDerivAt_integral_of_dominated_of_fderiv_le
: this version assumefun x ↦ F x a
has derivativeF' x a
forx
nearx₀
andF' x
is bounded by an integrable function independent fromx
nearx₀
.
hasDerivAt_integral_of_dominated_loc_of_lip
and
hasDerivAt_integral_of_dominated_loc_of_deriv_le
are versions of the above two results that
assume H = ℝ
or H = ℂ
and use the highschool derivative deriv
instead of Fréchet derivative
fderiv
.
We also provide versions of these theorems for set integrals.
Tags #
integral, derivative
Differentiation under integral of x ↦ ∫ F x a
at a given point x₀
, assuming F x₀
is
integrable, ‖F x a  F x₀ a‖ ≤ bound a * ‖x  x₀‖
for x
in a ball around x₀
for ae a
with
integrable Lipschitz bound bound
(with a ball radius independent of a
), and F x
is
aemeasurable for x
in the same ball. See hasFDerivAt_integral_of_dominated_loc_of_lip
for a
slightly less general but usually more useful version.
Differentiation under integral of x ↦ ∫ F x a
at a given point x₀
, assuming
F x₀
is integrable, x ↦ F x a
is locally Lipschitz on a ball around x₀
for ae a
(with a ball radius independent of a
) with integrable Lipschitz bound, and F x
is aemeasurable
for x
in a possibly smaller neighborhood of x₀
.
Differentiation under integral of x ↦ ∫ F x a
at a given point x₀
, assuming
F x₀
is integrable, x ↦ F x a
is differentiable on a ball around x₀
for ae a
with
derivative norm uniformly bounded by an integrable function (the ball radius is independent of a
),
and F x
is aemeasurable for x
in a possibly smaller neighborhood of x₀
.
Derivative under integral of x ↦ ∫ F x a
at a given point x₀ : 𝕜
, 𝕜 = ℝ
or 𝕜 = ℂ
,
assuming F x₀
is integrable, x ↦ F x a
is locally Lipschitz on a ball around x₀
for ae a
(with ball radius independent of a
) with integrable Lipschitz bound, and F x
is
aemeasurable for x
in a possibly smaller neighborhood of x₀
.
Derivative under integral of x ↦ ∫ F x a
at a given point x₀ : ℝ
, assuming
F x₀
is integrable, x ↦ F x a
is differentiable on an interval around x₀
for ae a
(with interval radius independent of a
) with derivative uniformly bounded by an integrable
function, and F x
is aemeasurable for x
in a possibly smaller neighborhood of x₀
.