# 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/Basic.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

source
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 ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {ε : ℝ} {F' : α → H →L[𝕜] E} (ε_pos : 0 < ε) (hF_meas : ∀ x ∈ Metric.ball x₀ ε, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun (x : H) => F x a) (F' a) x₀) :
MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun (x : H) => ∫ (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.

source
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 ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {ε : ℝ} {F' : α → H →L[𝕜] E} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun (x : H) => F x a) (Metric.ball x₀ ε)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun (x : H) => F x a) (F' a) x₀) :
MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun (x : H) => ∫ (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₀`.

source
theorem hasFDerivAt_integral_of_dominated_loc_of_lip_interval {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {ε : ℝ} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), LipschitzOnWith (Real.nnabs (bound t)) (fun (x : H) => F x t) (Metric.ball x₀ ε)) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), HasFDerivAt (fun (x : H) => F x t) (F' t) x₀) :
IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) 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₀`.

source
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 ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {ε : ℝ} {F' : H → α → H →L[𝕜] E} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) μ) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F' x a‖ ≤ bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun (x : H) => F x a) (F' x a) x) :
HasFDerivAt (fun (x : H) => ∫ (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₀`.

source
theorem hasFDerivAt_integral_of_dominated_of_fderiv_le'' {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {ε : ℝ} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ Metric.ball x₀ ε, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun (x : H) => F x t) (F' x t) x) :
HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) 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₀`.

source
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 ℝ E] [NormedSpace 𝕜 E] {bound : α → ℝ} {ε : ℝ} {F : 𝕜 → α → E} {x₀ : 𝕜} {F' : α → E} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun (x : 𝕜) => F x a) (Metric.ball x₀ ε)) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun (x : 𝕜) => F x a) (F' a) x₀) :
MeasureTheory.Integrable F' μ ∧ 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₀`.

source
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 ℝ E] [NormedSpace 𝕜 E] {bound : α → ℝ} {ε : ℝ} {F : 𝕜 → α → E} {x₀ : 𝕜} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) {F' : 𝕜 → α → E} (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) μ) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F' x a‖ ≤ bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ 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₀`.