# 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} [] {μ : } {E : Type u_2} [] [] [] {H : Type u_3} [] {a : } {b : } {ε : } {bound : } {F : HE} {F' : H →L[𝕜] E} {x₀ : H} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) ()) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : ) (h_lip : ∀ᵐ (t : ) ∂μ, t Ι a bLipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ) ∂μ, t Ι a bHasFDerivAt (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} [] {μ : } {E : Type u_2} [] [] [] {H : Type u_3} [] {a : } {b : } {ε : } {bound : } {F : HE} {F' : HH →L[𝕜] E} {x₀ : H} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) ()) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) ()) (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} [] {μ : } {E : Type u_2} [] [] [] {a : } {b : } {ε : } {bound : } {F : 𝕜E} {F' : E} {x₀ : 𝕜} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) ()) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : ) (h_lipsch : ∀ᵐ (t : ) ∂μ, t Ι a bLipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ) ∂μ, t Ι a bHasDerivAt (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} [] {μ : } {E : Type u_2} [] [] [] {a : } {b : } {ε : } {bound : } {F : 𝕜E} {F' : 𝕜E} {x₀ : 𝕜} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) ()) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) ()) (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₀.