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 fixed neighborhood s of x₀.

• 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₀.

• hasFDerivAt_integral_of_continuousOn_fderiv: this version assumes that F : H → α → E is continuously differentiable in the first argument near x₀ in the sense that:

  • F.uncurry : H × α → E is continuous on u ×ˢ k for a neighbourhood u of x₀,
  • fun x ↦ F x a is differentiable on u for each parameter a ∈ k,
  • fun (x, a) ↦ fderiv 𝕜 (fun y ↦ F y a) x is continuous on u ×ˢ k.

  Here k : Set α is the domain of integration and is required to be compact, regarding some sufficiently compatible topology on α.

• ContDiffOn.parametric_integral : If f.uncurry : H × H' → E is Cⁿ on u ×ˢ k for an open set u and a compact set k, then given any subset s₀ of k the parametric integral fun x ↦ ∫ a in s₀, f x a ∂μ is Cⁿ on u too.

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.

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 ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H} {F' : α → H →L[𝕜] E} (hs : s ∈ nhds x₀) (hF_meas : ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (F x) μ) (hF_int : MeasureTheory.Integrable (F x₀) μ) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ) (h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖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 neighborhood of x₀ for ae a integrable Lipschitz bound bound (with a neighborhood 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 ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H} {F' : α → H →L[𝕜] E} (hs : s ∈ nhds x₀) (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) s) (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 in a neighborhood of x₀ for ae a (with a neighborhood 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 ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {s : Set H} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds x₀) (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) s) (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 neighborhood of x₀ for almost every t (with a neighborhood 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 ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H} {bound : α → ℝ} {s : Set H} {F' : H → α → H →L[𝕜] E} (hs : s ∈ nhds x₀) (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 ∈ s, ‖F' x a‖ ≤ bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, 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 neighborhood of x₀ for ae a with derivative norm uniformly bounded by an integrable function (the neighborhood 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 ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {s : Set H} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds x₀) (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 ∈ s, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ s, 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 neighborhood of x₀ for ae a with derivative norm uniformly bounded by an integrable function (the neighborhood is independent of a), and F x is ae-measurable for x in a possibly smaller neighborhood of x₀.

theorem hasFDerivAt_integral_of_continuousOn_fderiv {α : 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] [TopologicalSpace α] [OpensMeasurableSpace α] {F : H → α → E} {x₀ : H} {u : Set H} (hu : u ∈ nhds x₀) {k s : Set α} (hk : IsCompact k) (hs : MeasurableSet s) (hs' : μ s ≠ ⊤) (hsk : s ⊆ k) (hF₁ : ContinuousOn (Function.uncurry F) (u ×ˢ k)) (hF₂ : ∀ a ∈ k, DifferentiableOn 𝕜 (fun (x : H) => F x a) u) (hF₃ : ContinuousOn (fun (x : H × α) => fderiv 𝕜 (fun (y : H) => F y x.2) x.1) (u ×ˢ k)) : HasFDerivAt (fun (x : H) => ∫ (a : α) in s, F x a ∂μ) (∫ (a : α) in s, fderiv 𝕜 (fun (x : H) => F x a) x₀ ∂μ) x₀

A convenient special case of hasFDerivAt_integral_of_dominated_of_fderiv_le: if there exist a neighbourhood u of x₀ and a compact set k such that F.uncurry : H × α → E is continuous and continuously differentiable in the first argument on u ×ˢ k, then for any finite-measure set s ⊆ k a derivative of fun x => ∫ a in s, F x a ∂μ in x₀ can be computed as ∫ a in s, fderiv 𝕜 (fun x ↦ F x a) x₀ ∂μ.

theorem hasFDerivAt_integral_of_continuousOn_fderiv_of_t2Space {α : 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] [TopologicalSpace α] [T2Space α] [OpensMeasurableSpace α] {F : H → α → E} {x₀ : H} {u : Set H} (hu : u ∈ nhds x₀) {k s : Set α} (hk : IsCompact k) (hs' : μ s ≠ ⊤) (hsk : s ⊆ k) (hF₁ : ContinuousOn (Function.uncurry F) (u ×ˢ k)) (hF₂ : ∀ a ∈ k, DifferentiableOn 𝕜 (fun (x : H) => F x a) u) (hF₃ : ContinuousOn (fun (x : H × α) => fderiv 𝕜 (fun (y : H) => F y x.2) x.1) (u ×ˢ k)) : HasFDerivAt (fun (x : H) => ∫ (a : α) in s, F x a ∂μ) (∫ (a : α) in s, fderiv 𝕜 (fun (x : H) => F x a) x₀ ∂μ) x₀

A version of hasFDerivAt_integral_of_continuousOn_fderiv where α is required to be Hausdorff but s is not required to be measurable.

theorem hasFDerivAt_integral_of_contDiffOn {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {H' : Type u_5} [NormedAddCommGroup H'] [NormedSpace 𝕜 H'] [MeasurableSpace H'] [OpensMeasurableSpace H'] {μ : MeasureTheory.Measure H'} {f : H → H' → E} {x₀ : H} {u : Set H} (hu : u ∈ nhds x₀) {k s : Set H'} (hk : IsCompact k) (hs' : μ s ≠ ⊤) (hsk : s ⊆ k) (hF : ContDiffOn 𝕜 1 (Function.uncurry f) (u ×ˢ k)) : HasFDerivAt (fun (x : H) => ∫ (a : H') in s, f x a ∂μ) (∫ (a : H') in s, fderiv 𝕜 (fun (x : H) => f x a) x₀ ∂μ) x₀

A convenient special case of hasFDerivAt_integral_of_continuousOn_fderiv: if f.uncurry : H × H' → E is continuously differentiable on u ×ˢ k for a neighbourhood u of x₀ and a compact set k, then for any finite-measure set s ⊆ k a derivative of fun x => ∫ a in s, f x a ∂μ in x₀ can be computed as ∫ a in s, fderiv 𝕜 (fun x ↦ f x a) x₀ ∂μ.

theorem hasFTaylorSeriesUpToOn_integral_of_le_bound {α : 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} {s : Set H} {n : WithTop ℕ∞} {bound : ℕ → α → ℝ} {p : H → α → FormalMultilinearSeries 𝕜 H E} (hs : IsOpen s) (hF_meas : ∀ x ∈ s, ∀ (i : ℕ), ↑i ≤ n → MeasureTheory.AEStronglyMeasurable (fun (x_1 : α) => p x x_1 i) μ) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ∀ (i : ℕ), ↑i ≤ n → ‖p x a i‖ ≤ bound i a) (bound_integrable : ∀ (i : ℕ), ↑i ≤ n → MeasureTheory.Integrable (bound i) μ) (h_diff : ∀ᵐ (a : α) ∂μ, HasFTaylorSeriesUpToOn n (fun (x : H) => F x a) (fun (x : H) => p x a) s) : HasFTaylorSeriesUpToOn n (fun (x : H) => ∫ (a : α), F x a ∂μ) (fun (x : H) (i : ℕ) => ∫ (a : α), p x a i ∂μ) s

Iterated differentiation under integral of x ↦ ∫ F x a on an open set s, assuming that each function x ↦ F x a has a Taylor series of order n, with uniform integrability conditions on the successive derivatives.

theorem hasFTaylorSeriesUpToOn_setIntegral_of_le_const {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {H' : Type u_5} [NormedAddCommGroup H'] [NormedSpace 𝕜 H'] [MeasurableSpace H'] [OpensMeasurableSpace H'] {s : Set H} {n : WithTop ℕ∞} {C : ℕ → ℝ} {μ : MeasureTheory.Measure H'} {p : H × H' → FormalMultilinearSeries 𝕜 (H × H') E} (hs : IsOpen s) {t : Set H'} {F : H → H' → E} (ht : TopologicalSpace.IsSeparable t) (tmeas : MeasurableSet t) (hmut : μ t ≠ ⊤) (hF : HasFTaylorSeriesUpToOn n (Function.uncurry F) p (s ×ˢ t)) (h_bound : ∀ x ∈ s, ∀ a ∈ t, ∀ (i : ℕ), ↑i ≤ n → ‖p (x, a) i‖ ≤ C i) : HasFTaylorSeriesUpToOn n (fun (x : H) => ∫ (a : H') in t, F x a ∂μ) (fun (x : H) (i : ℕ) => ∫ (a : H') in t, (p (x, a) i).compContinuousLinearMap fun (x : Fin i) => ContinuousLinearMap.inl 𝕜 H H' ∂μ) s

theorem ContDiffOn.parametric_integral {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {H' : Type u_5} [NormedAddCommGroup H'] [NormedSpace 𝕜 H'] [MeasurableSpace H'] [OpensMeasurableSpace H'] {μ : MeasureTheory.Measure H'} {f : H → H' → E} {u : Set H} (hu : IsOpen u) {s₀ k : Set H'} (hk : IsCompact k) {n : ℕ∞} (hs₀ : s₀ ⊆ k) (hf : ContDiffOn 𝕜 (↑n) (Function.uncurry f) (u ×ˢ k)) (mus₀ : μ s₀ ≠ ⊤) : ContDiffOn 𝕜 (↑n) (fun (x : H) => ∫ (a : H') in s₀, f x a ∂μ) u

If f.uncurry : H × H' → E is Cⁿ on u ×ˢ k for an open set u and a compact set k, then given any finite-measure subset s₀ of k the parametric integral fun x ↦ ∫ a in s₀, f x a ∂μ is Cⁿ on u too.

theorem ContDiff.parametric_integral {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {H' : Type u_5} [NormedAddCommGroup H'] [NormedSpace 𝕜 H'] [MeasurableSpace H'] [OpensMeasurableSpace H'] {μ : MeasureTheory.Measure H'} {f : H → H' → E} {k s₀ : Set H'} (hk : IsCompact k) (hs₀ : s₀ ⊆ k) (mus₀ : μ s₀ ≠ ⊤) {n : ℕ∞} (hf : ContDiff 𝕜 (↑n) (Function.uncurry f)) : ContDiff 𝕜 ↑n fun (x : H) => ∫ (a : H') in s₀, f x a ∂μ

If f.uncurry : H × H' → E is Cⁿ, the parametric integral fun x ↦ ∫ a in s₀, f x a ∂μ over a finite-measure set s₀ contained in a compact set k is Cⁿ too.

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₀ : 𝕜} {s : Set 𝕜} {F' : α → E} (hs : s ∈ nhds x₀) (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) s) (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 neighborhood of x₀ for ae a (with a neighborhood 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 ℝ E] [NormedSpace 𝕜 E] {bound : α → ℝ} {F : 𝕜 → α → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (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 ∈ s, ‖F' x a‖ ≤ bound a) (bound_integrable : MeasureTheory.Integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, 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₀.