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 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [NormedAddCommGroup H] [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 : MeasureTheory.AEStronglyMeasurable F' (MeasureTheory.Measure.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} [IsROrC 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [NormedAddCommGroup H] [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 ∈ 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} [IsROrC 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [CompleteSpace 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' (MeasureTheory.Measure.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} [IsROrC 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] [CompleteSpace 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 ∈ 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₀.