# Derivatives of interval integrals depending on parameters #

In this file we restate theorems about derivatives of integrals depending on parameters for interval integrals.

theorem intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip {๐ : Type u_1} [RCLike ๐] {ฮผ : } {E : Type u_2} [] [NormedSpace ๐ E] {H : Type u_3} [NormedSpace ๐ H] {a : โ} {b : โ} {ฮต : โ} {bound : โ โ โ} {F : H โ โ โ E} {F' : โ โ H โL[๐] E} {xโ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : H) in nhds xโ, MeasureTheory.AEStronglyMeasurable (F x) (ฮผ.restrict (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (ฮผ.restrict (ฮ a b))) (h_lip : โแต (t : โ) โฮผ, t โ ฮ 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 : โ) โฮผ, t โ ฮ 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 โฆ โซ t in a..b, F x t 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 intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le {๐ : Type u_1} [RCLike ๐] {ฮผ : } {E : Type u_2} [] [NormedSpace ๐ E] {H : Type u_3} [NormedSpace ๐ H] {a : โ} {b : โ} {ฮต : โ} {bound : โ โ โ} {F : H โ โ โ E} {F' : H โ โ โ H โL[๐] E} {xโ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : H) in nhds xโ, MeasureTheory.AEStronglyMeasurable (F x) (ฮผ.restrict (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' xโ) (ฮผ.restrict (ฮ a b))) (h_bound : โแต (t : โ) โฮผ, t โ ฮ a b โ โ x โ Metric.ball xโ ฮต, โF' x tโ โค bound t) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ ฮ 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 โฆ โซ 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 intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip {๐ : Type u_1} [RCLike ๐] {ฮผ : } {E : Type u_2} [] [NormedSpace ๐ E] {a : โ} {b : โ} {ฮต : โ} {bound : โ โ โ} {F : ๐ โ โ โ E} {F' : โ โ E} {xโ : ๐} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : ๐) in nhds xโ, MeasureTheory.AEStronglyMeasurable (F x) (ฮผ.restrict (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (ฮผ.restrict (ฮ a b))) (h_lipsch : โแต (t : โ) โฮผ, t โ ฮ a b โ LipschitzOnWith (Real.nnabs (bound t)) (fun (x : ๐) => F x t) (Metric.ball xโ ฮต)) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ ฮ a b โ HasDerivAt (fun (x : ๐) => F x t) (F' t) xโ) :
IntervalIntegrable F' ฮผ a b โง HasDerivAt (fun (x : ๐) => โซ (t : โ) in a..b, F x t โฮผ) (โซ (t : โ) in a..b, F' t โฮผ) 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 intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le {๐ : Type u_1} [RCLike ๐] {ฮผ : } {E : Type u_2} [] [NormedSpace ๐ E] {a : โ} {b : โ} {ฮต : โ} {bound : โ โ โ} {F : ๐ โ โ โ E} {F' : ๐ โ โ โ E} {xโ : ๐} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : ๐) in nhds xโ, MeasureTheory.AEStronglyMeasurable (F x) (ฮผ.restrict (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' xโ) (ฮผ.restrict (ฮ a b))) (h_bound : โแต (t : โ) โฮผ, t โ ฮ a b โ โ x โ Metric.ball xโ ฮต, โF' x tโ โค bound t) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ ฮ a b โ โ x โ Metric.ball xโ ฮต, HasDerivAt (fun (x : ๐) => F x t) (F' x t) x) :
IntervalIntegrable (F' xโ) ฮผ a b โง HasDerivAt (fun (x : ๐) => โซ (t : โ) in a..b, F x t โฮผ) (โซ (t : โ) in a..b, F' xโ t โฮผ) 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 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โ.