# Documentation

Mathlib.Analysis.Calculus.ParametricIntervalIntegral

# 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} [IsROrC ๐] {ฮผ : } {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) (MeasureTheory.Measure.restrict ฮผ (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : ) (h_lip : โแต (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 โ HasFDerivAt (fun x => F x t) (F' t) xโ) :
IntervalIntegrable F' ฮผ a b โง HasFDerivAt (fun x => โซ (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} [IsROrC ๐] {ฮผ : } {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) (MeasureTheory.Measure.restrict ฮผ (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' xโ) (MeasureTheory.Measure.restrict ฮผ (ฮ a b))) (h_bound : โแต (t : โ) โฮผ, t โ ฮ a b โ โ (x : H), x โ Metric.ball xโ ฮต โ โF' x tโ โค bound t) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ ฮ a b โ โ (x : H), x โ Metric.ball xโ ฮต โ HasFDerivAt (fun x => F x t) (F' x t) x) :
HasFDerivAt (fun x => โซ (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} [IsROrC ๐] {ฮผ : } {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) (MeasureTheory.Measure.restrict ฮผ (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : ) (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} [IsROrC ๐] {ฮผ : } {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) (MeasureTheory.Measure.restrict ฮผ (ฮ a b))) (hF_int : IntervalIntegrable (F xโ) ฮผ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' xโ) (MeasureTheory.Measure.restrict ฮผ (ฮ a b))) (h_bound : โแต (t : โ) โฮผ, t โ ฮ a b โ โ (x : ๐), x โ Metric.ball xโ ฮต โ โF' x tโ โค bound t) (bound_integrable : IntervalIntegrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ ฮ a b โ โ (x : ๐), 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โ.