Derivatives of integrals depending on parameters

A parametric integral is a function with shape f = fun 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 that

  • F x is ae-measurable for x near x₀,
  • F x₀ is integrable,
  • fun x ↦ F x a has derivative F' a : H →L[ℝ] E at x₀ which is ae-measurable,
  • fun x ↦ F x a is locally Lipschitz near x₀ for almost every a, with a Lipschitz bound which is integrable with respect to a.

  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 assumes fun x ↦ F x a has derivative F' x a for x near x₀ and F' x is bounded by an integrable function independent from x near x₀.

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 high-school derivative deriv instead of Fréchet derivative fderiv.

We also provide versions of these theorems for set integrals.

Tags

integral, derivative

theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → Real} {ε : Real} {F' : α → ContinuousLinearMap (RingHom.id 𝕜) H E} (ε_pos : LT.lt 0 ε) (hF_meas : ∀ (x : H), Membership.mem (Metric.ball x₀ ε) x → MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lipsch : Filter.Eventually (fun (a : α) => ∀ (x : H), Membership.mem (Metric.ball x₀ ε) x → LE.le (Norm.norm (HSub.hSub (F x a) (F x₀ a))) (HMul.hMul (bound a) (Norm.norm (HSub.hSub x x₀)))) (MeasureTheory.ae μ)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : Filter.Eventually (fun (a : α) => HasFDerivAt (fun (x : H) => F x a) (F' a) x₀) (MeasureTheory.ae μ)) : And (MeasureTheory.Integrable F' μ) (HasFDerivAt (fun (x : H) => MeasureTheory.integral μ fun (a : α) => F x a) (MeasureTheory.integral μ fun (a : α) => F' a) x₀)

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 ae-measurable for x in the same ball. See hasFDerivAt_integral_of_dominated_loc_of_lip for a slightly less general but usually more useful version.

theorem hasFDerivAt_integral_of_dominated_loc_of_lip {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → Real} {ε : Real} {F' : α → ContinuousLinearMap (RingHom.id 𝕜) H E} (ε_pos : LT.lt 0 ε) (hF_meas : Filter.Eventually (fun (x : H) => MeasureTheory.AEStronglyMeasurable (F x) μ) (nhds x₀)) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lip : Filter.Eventually (fun (a : α) => LipschitzOnWith (DFunLike.coe Real.nnabs (bound a)) (fun (x : H) => F x a) (Metric.ball x₀ ε)) (MeasureTheory.ae μ)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : Filter.Eventually (fun (a : α) => HasFDerivAt (fun (x : H) => F x a) (F' a) x₀) (MeasureTheory.ae μ)) : And (MeasureTheory.Integrable F' μ) (HasFDerivAt (fun (x : H) => MeasureTheory.integral μ fun (a : α) => F x a) (MeasureTheory.integral μ fun (a : α) => F' a) x₀)

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 ae-measurable for x in a possibly smaller neighborhood of x₀.

theorem hasFDerivAt_integral_of_dominated_loc_of_lip_interval {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {ε : Real} [NormedSpace Real H] {μ : MeasureTheory.Measure Real} {F : H → Real → E} {F' : Real → ContinuousLinearMap (RingHom.id Real) H E} {a b : Real} {bound : Real → Real} (ε_pos : LT.lt 0 ε) (hF_meas : Filter.Eventually (fun (x : H) => MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (nhds x₀)) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : Filter.Eventually (fun (t : Real) => LipschitzOnWith (DFunLike.coe Real.nnabs (bound t)) (fun (x : H) => F x t) (Metric.ball x₀ ε)) (MeasureTheory.ae (μ.restrict (Set.uIoc a b)))) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : Filter.Eventually (fun (t : Real) => HasFDerivAt (fun (x : H) => F x t) (F' t) x₀) (MeasureTheory.ae (μ.restrict (Set.uIoc a b)))) : And (IntervalIntegrable F' μ a b) (HasFDerivAt (fun (x : H) => intervalIntegral (fun (t : Real) => F x t) a b μ) (intervalIntegral (fun (t : Real) => F' t) a b μ) x₀)

Differentiation under integral of x ↦ ∫ x in a..b, F x t at a given point x₀ ∈ (a,b), assuming F x₀ is integrable on (a,b), that x ↦ F x t is Lipschitz on a ball around x₀ for almost every t (with a ball radius independent of t) with integrable Lipschitz bound, and F x is a.e.-measurable for x in a possibly smaller neighborhood of x₀.

theorem hasFDerivAt_integral_of_dominated_of_fderiv_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → Real} {ε : Real} {F' : H → α → ContinuousLinearMap (RingHom.id 𝕜) H E} (ε_pos : LT.lt 0 ε) (hF_meas : Filter.Eventually (fun (x : H) => MeasureTheory.AEStronglyMeasurable (F x) μ) (nhds x₀)) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) μ) (h_bound : Filter.Eventually (fun (a : α) => ∀ (x : H), Membership.mem (Metric.ball x₀ ε) x → LE.le (Norm.norm (F' x a)) (bound a)) (MeasureTheory.ae μ)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : Filter.Eventually (fun (a : α) => ∀ (x : H), Membership.mem (Metric.ball x₀ ε) x → HasFDerivAt (fun (x : H) => F x a) (F' x a) x) (MeasureTheory.ae μ)) : HasFDerivAt (fun (x : H) => MeasureTheory.integral μ fun (a : α) => F x a) (MeasureTheory.integral μ fun (a : α) => F' x₀ a) 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 ae-measurable for x in a possibly smaller neighborhood of x₀.

theorem hasFDerivAt_integral_of_dominated_of_fderiv_le'' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {ε : Real} [NormedSpace Real H] {μ : MeasureTheory.Measure Real} {F : H → Real → E} {F' : H → Real → ContinuousLinearMap (RingHom.id Real) H E} {a b : Real} {bound : Real → Real} (ε_pos : LT.lt 0 ε) (hF_meas : Filter.Eventually (fun (x : H) => MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (nhds x₀)) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : Filter.Eventually (fun (t : Real) => ∀ (x : H), Membership.mem (Metric.ball x₀ ε) x → LE.le (Norm.norm (F' x t)) (bound t)) (MeasureTheory.ae (μ.restrict (Set.uIoc a b)))) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : Filter.Eventually (fun (t : Real) => ∀ (x : H), Membership.mem (Metric.ball x₀ ε) x → HasFDerivAt (fun (x : H) => F x t) (F' x t) x) (MeasureTheory.ae (μ.restrict (Set.uIoc a b)))) : HasFDerivAt (fun (x : H) => intervalIntegral (fun (t : Real) => F x t) a b μ) (intervalIntegral (fun (t : Real) => F' x₀ t) a b μ) x₀

Differentiation under integral of x ↦ ∫ x in a..b, F x a at a given point x₀, assuming F x₀ is integrable on (a,b), 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 ae-measurable for x in a possibly smaller neighborhood of x₀.

theorem hasDerivAt_integral_of_dominated_loc_of_lip {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] [NormedSpace 𝕜 E] {bound : α → Real} {ε : Real} {F : 𝕜 → α → E} {x₀ : 𝕜} {F' : α → E} (ε_pos : LT.lt 0 ε) (hF_meas : Filter.Eventually (fun (x : 𝕜) => MeasureTheory.AEStronglyMeasurable (F x) μ) (nhds x₀)) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lipsch : Filter.Eventually (fun (a : α) => LipschitzOnWith (DFunLike.coe Real.nnabs (bound a)) (fun (x : 𝕜) => F x a) (Metric.ball x₀ ε)) (MeasureTheory.ae μ)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : Filter.Eventually (fun (a : α) => HasDerivAt (fun (x : 𝕜) => F x a) (F' a) x₀) (MeasureTheory.ae μ)) : And (MeasureTheory.Integrable F' μ) (HasDerivAt (fun (x : 𝕜) => MeasureTheory.integral μ fun (a : α) => F x a) (MeasureTheory.integral μ fun (a : α) => F' a) 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 ae-measurable for x in a possibly smaller neighborhood of x₀.

theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace Real E] [NormedSpace 𝕜 E] {bound : α → Real} {ε : Real} {F : 𝕜 → α → E} {x₀ : 𝕜} (ε_pos : LT.lt 0 ε) (hF_meas : Filter.Eventually (fun (x : 𝕜) => MeasureTheory.AEStronglyMeasurable (F x) μ) (nhds x₀)) (hF_int : MeasureTheory.Integrable (F x₀) μ) {F' : 𝕜 → α → E} (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) μ) (h_bound : Filter.Eventually (fun (a : α) => ∀ (x : 𝕜), Membership.mem (Metric.ball x₀ ε) x → LE.le (Norm.norm (F' x a)) (bound a)) (MeasureTheory.ae μ)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : Filter.Eventually (fun (a : α) => ∀ (x : 𝕜), Membership.mem (Metric.ball x₀ ε) x → HasDerivAt (fun (x : 𝕜) => F x a) (F' x a) x) (MeasureTheory.ae μ)) : And (MeasureTheory.Integrable (F' x₀) μ) (HasDerivAt (fun (n : 𝕜) => MeasureTheory.integral μ fun (a : α) => F n a) (MeasureTheory.integral μ fun (a : α) => F' x₀ a) 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 ae-measurable for x in a possibly smaller neighborhood of x₀.