Derivatives of interval integrals depending on parameters

In this file we restate theorems about derivatives of integrals depending on parameters for interval integrals. In the real case, we also show that parametric integrals of Cⁿ functions are Cⁿ.

theorem intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun (x : H) => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc 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 neighborhood of x₀ for ae a (with a neighborhood 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 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, 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 neighborhood of x₀ for ae a with derivative norm uniformly bounded by an integrable function (the neighborhood 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 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lipsch : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun (x : 𝕜) => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc 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 neighborhood of x₀ for ae a (with a neighborhood 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 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F F' : 𝕜 → ℝ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, 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 a neighborhood of x₀ for ae a (with a neighborhood 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₀.

theorem intervalIntegral.hasFDerivAt_integral_of_continuousOn_fderiv {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : H → ℝ → E} {x₀ : H} {u : Set H} (hu : u ∈ nhds x₀) {a b : ℝ} (hF₁ : ContinuousOn (Function.uncurry f) (u ×ˢ Set.uIcc a b)) (hF₂ : ∀ t ∈ Set.uIcc a b, DifferentiableOn 𝕜 (fun (x : H) => f x t) u) (hF₃ : ContinuousOn (fun (x : H × ℝ) => fderiv 𝕜 (fun (y : H) => f y x.2) x.1) (u ×ˢ Set.uIcc a b)) : HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..b, f x t ∂μ) (∫ (t : ℝ) in a..b, fderiv 𝕜 (fun (x : H) => f x t) x₀ ∂μ) x₀

A convenient special case of intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le: if there exists a neighbourhood u of x₀ such that f.uncurry : H × ℝ → E is continuous on u ×ˢ [[a, b]] and differentiable on u in the first argument for every t ∈ [[a, b]] and that derivative is continuous on u ×ˢ [[a, b]], then a derivative of fun x => ∫ t in a..b, f x t ∂μ in x₀ can be computed as ∫ t in a..b, fderiv 𝕜 (fun x ↦ f x t) x₀ ∂μ.

theorem intervalIntegral.hasFDerivAt_integral_of_contDiffOn {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H → ℝ → E} {x₀ : H} {u : Set H} (hu : u ∈ nhds x₀) {a b : ℝ} (hF : ContDiffOn ℝ 1 (Function.uncurry f) (u ×ˢ Set.uIcc a b)) : HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in a..b, f x t ∂μ) (∫ (t : ℝ) in a..b, fderiv ℝ (fun (x : H) => f x t) x₀ ∂μ) x₀

A convenient special case of intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le: if f.uncurry : H × ℝ → E is continuously differentiable on u ×ˢ [[a, b]] for a neighbourhood u of x₀, then a derivative of fun x => ∫ t in a..b, f x t ∂μ in x₀ can be computed as ∫ t in a..b, fderiv ℝ (fun x ↦ f x t) x₀ ∂μ.

theorem ContDiffOn.parametric_intervalIntegral {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H → ℝ → E} {u : Set H} (hu : IsOpen u) {a b : ℝ} {n : ℕ∞} (hf : ContDiffOn ℝ (↑n) (Function.uncurry f) (u ×ˢ Set.uIcc a b)) : ContDiffOn ℝ (↑n) (fun (x : H) => ∫ (t : ℝ) in a..b, f x t ∂μ) u

If f.uncurry : H × ℝ → E is Cⁿ on u ×ˢ [[a, b]], the parametric integral fun x ↦ ∫ t in a..b, f x t ∂μ is Cⁿ on u too.

theorem ContDiff.parametric_intervalIntegral {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {E : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup H] [NormedSpace ℝ H] {f : H × ℝ → E} {a b : ℝ} {n : ℕ∞} (hf : ContDiff ℝ (↑n) f) : ContDiff ℝ ↑n fun (x : H) => ∫ (t : ℝ) in a..b, f (x, t) ∂μ

If f : H × ℝ → E is Cⁿ, the parametric integral fun x ↦ ∫ t in a..b, f (x, t) ∂μ is Cⁿ too.