# Documentation

Mathlib.Analysis.Calculus.ParametricIntegral

# 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 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,
• λ 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 assume 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} [] {μ : } {𝕜 : Type u_2} [] {E : Type u_3} [] [] [] {H : Type u_4} [] {F : HαE} {F' : αH →L[𝕜] E} {x₀ : H} {bound : α} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ (x : H), x Metric.ball x₀ ε) (hF_int : MeasureTheory.Integrable (F x₀)) (hF'_meas : ) (h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ (x : H), x Metric.ball x₀ εF x a - F x₀ a bound a * x - x₀) (bound_integrable : ) (h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) :
HasFDerivAt (fun x => ∫ (a : α), F x aμ) (∫ (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} [] {μ : } {𝕜 : Type u_2} [] {E : Type u_3} [] [] [] {H : Type u_4} [] {F : HαE} {F' : αH →L[𝕜] E} {x₀ : H} {bound : α} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, ) (hF_int : MeasureTheory.Integrable (F x₀)) (hF'_meas : ) (h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (Metric.ball x₀ ε)) (bound_integrable : ) (h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀) :
HasFDerivAt (fun x => ∫ (a : α), F x aμ) (∫ (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_of_fderiv_le {α : Type u_1} [] {μ : } {𝕜 : Type u_2} [] {E : Type u_3} [] [] [] {H : Type u_4} [] {F : HαE} {F' : HαH →L[𝕜] E} {x₀ : H} {bound : α} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, ) (hF_int : MeasureTheory.Integrable (F x₀)) (hF'_meas : ) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (x : H), x Metric.ball x₀ εF' x a bound a) (bound_integrable : ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ (x : H), x Metric.ball x₀ εHasFDerivAt (fun x => F x a) (F' x a) x) :
HasFDerivAt (fun x => ∫ (a : α), F x aμ) (∫ (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 hasDerivAt_integral_of_dominated_loc_of_lip {α : Type u_1} [] {μ : } {𝕜 : Type u_2} [] {E : Type u_3} [] [] [] {F : 𝕜αE} {F' : αE} {x₀ : 𝕜} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, ) (hF_int : MeasureTheory.Integrable (F x₀)) (hF'_meas : ) {bound : α} (h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (Metric.ball x₀ ε)) (bound_integrable : ) (h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' a) x₀) :
HasDerivAt (fun x => ∫ (a : α), F x aμ) (∫ (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} [] {μ : } {𝕜 : Type u_2} [] {E : Type u_3} [] [] [] {F : 𝕜αE} {F' : 𝕜αE} {x₀ : 𝕜} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, ) (hF_int : MeasureTheory.Integrable (F x₀)) (hF'_meas : ) {bound : α} (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (x : 𝕜), x Metric.ball x₀ εF' x a bound a) (bound_integrable : ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ (x : 𝕜), x Metric.ball x₀ εHasDerivAt (fun x => F x a) (F' x a) x) :
MeasureTheory.Integrable (F' x₀) HasDerivAt (fun n => ∫ (a : α), F n aμ) (∫ (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₀.