# mathlibdocumentation

analysis.calculus.parametric_interval_integral

# Derivatives of interval integrals depending on parameters #

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

theorem interval_integral.has_fderiv_at_integral_of_dominated_loc_of_lip {๐ : Type u_1} [is_R_or_C ๐] {E : Type u_2} [ E] [normed_space ๐ E] {H : Type u_3} [normed_space ๐ H] {a b ฮต : โ} {bound : โ โ โ} {F : H โ โ โ E} {F' : โ โ (H โL[๐] E)} {xโ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : H) in nhds xโ, (ฮผ.restrict b))) (hF_int : interval_integrable (F xโ) ฮผ a b) (hF'_meas : (ฮผ.restrict b))) (h_lip : โแต (t : โ) โฮผ, t โ โ lipschitz_on_with (โreal.nnabs (bound t)) (ฮป (x : H), F x t) (metric.ball xโ ฮต)) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ โ has_fderiv_at (ฮป (x : H), F x t) (F' t) xโ) :
ฮผ a b โง has_fderiv_at (ฮป (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 interval_integral.has_fderiv_at_integral_of_dominated_of_fderiv_le {๐ : Type u_1} [is_R_or_C ๐] {E : Type u_2} [ E] [normed_space ๐ E] {H : Type u_3} [normed_space ๐ H] {a b ฮต : โ} {bound : โ โ โ} {F : H โ โ โ E} {F' : H โ โ โ (H โL[๐] E)} {xโ : H} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : H) in nhds xโ, (ฮผ.restrict b))) (hF_int : interval_integrable (F xโ) ฮผ a b) (hF'_meas : (ฮผ.restrict b))) (h_bound : โแต (t : โ) โฮผ, t โ โ โ (x : H), x โ metric.ball xโ ฮต โ โฅF' x tโฅ โค bound t) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ โ โ (x : H), x โ metric.ball xโ ฮต โ has_fderiv_at (ฮป (x : H), F x t) (F' x t) x) :
has_fderiv_at (ฮป (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 interval_integral.has_deriv_at_integral_of_dominated_loc_of_lip {๐ : Type u_1} [is_R_or_C ๐] {E : Type u_2} [ E] [normed_space ๐ E] {a b ฮต : โ} {bound : โ โ โ} {F : ๐ โ โ โ E} {F' : โ โ E} {xโ : ๐} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : ๐) in nhds xโ, (ฮผ.restrict b))) (hF_int : interval_integrable (F xโ) ฮผ a b) (hF'_meas : (ฮผ.restrict b))) (h_lipsch : โแต (t : โ) โฮผ, t โ โ lipschitz_on_with (โreal.nnabs (bound t)) (ฮป (x : ๐), F x t) (metric.ball xโ ฮต)) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ โ has_deriv_at (ฮป (x : ๐), F x t) (F' t) xโ) :
ฮผ a b โง has_deriv_at (ฮป (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 interval_integral.has_deriv_at_integral_of_dominated_loc_of_deriv_le {๐ : Type u_1} [is_R_or_C ๐] {E : Type u_2} [ E] [normed_space ๐ E] {a b ฮต : โ} {bound : โ โ โ} {F F' : ๐ โ โ โ E} {xโ : ๐} (ฮต_pos : 0 < ฮต) (hF_meas : โแถ  (x : ๐) in nhds xโ, (ฮผ.restrict b))) (hF_int : interval_integrable (F xโ) ฮผ a b) (hF'_meas : (ฮผ.restrict b))) (h_bound : โแต (t : โ) โฮผ, t โ โ โ (x : ๐), x โ metric.ball xโ ฮต โ โฅF' x tโฅ โค bound t) (bound_integrable : interval_integrable bound ฮผ a b) (h_diff : โแต (t : โ) โฮผ, t โ โ โ (x : ๐), x โ metric.ball xโ ฮต โ has_deriv_at (ฮป (x : ๐), F x t) (F' x t) x) :
interval_integrable (F' xโ) ฮผ a b โง has_deriv_at (ฮป (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โ.