mathlib documentation

analysis.calculus.parametric_integral

Derivatives of integrals depending on parameters #

A parametric integral is a function with shape f = λ x : H, ∫ a : α, F x a ∂μ for some F : H → α → E, where H and E are normed spaces and α is a measured space with measure μ.

We already know from continuous_of_dominated in measure_theory.integral.bochner how to guarantee that f is continuous using the dominated convergence theorem. In this file, we want to express the derivative of f as the integral of the derivative of F with respect to x.

Main results #

As explained above, all results express the derivative of a parametric integral as the integral of a derivative. The variations come from the assumptions and from the different ways of expressing derivative, especially Fréchet derivatives vs elementary derivative of function of one real variable.

has_deriv_at_integral_of_dominated_loc_of_lip and has_deriv_at_integral_of_dominated_loc_of_deriv_le are versions of the above two results that assume H = ℝ or H = ℂ and use the high-school derivative deriv instead of Fréchet derivative fderiv.

We also provide versions of these theorems for set integrals.

Tags #

integral, derivative

theorem has_fderiv_at_integral_of_dominated_loc_of_lip' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {H : Type u_4} [normed_group H] [normed_space 𝕜 H] [topological_space.second_countable_topology (H →L[𝕜] E)] {F : H → α → E} {F' : α → (H →L[𝕜] E)} {x₀ : H} {bound : α → } {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ (x : H), x metric.ball x₀ εae_measurable (F x) μ) (hF_int : measure_theory.integrable (F x₀) μ) (hF'_meas : ae_measurable F' μ) (h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ (x : H), x metric.ball x₀ εF x a - F x₀ a (bound a) * x - x₀) (bound_integrable : measure_theory.integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, has_fderiv_at (λ (x : H), F x a) (F' a) x₀) :
measure_theory.integrable F' μ has_fderiv_at (λ (x : H), (a : α), F x a μ) ( (a : α), F' a μ) x₀

Differentiation under integral of x ↦ ∫ F x a at a given point x₀, assuming F x₀ is integrable, ∥F x a - F x₀ a∥ ≤ bound a * ∥x - x₀∥ for x in a ball around x₀ for ae a with integrable Lipschitz bound bound (with a ball radius independent of a), and F x is ae-measurable for x in the same ball. See has_fderiv_at_integral_of_dominated_loc_of_lip for a slightly less general but usually more useful version.

theorem has_fderiv_at_integral_of_dominated_loc_of_lip {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {H : Type u_4} [normed_group H] [normed_space 𝕜 H] [topological_space.second_countable_topology (H →L[𝕜] E)] {F : H → α → E} {F' : α → (H →L[𝕜] E)} {x₀ : H} {bound : α → } {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, ae_measurable (F x) μ) (hF_int : measure_theory.integrable (F x₀) μ) (hF'_meas : ae_measurable F' μ) (h_lip : ∀ᵐ (a : α) ∂μ, lipschitz_on_with (real.nnabs (bound a)) (λ (x : H), F x a) (metric.ball x₀ ε)) (bound_integrable : measure_theory.integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, has_fderiv_at (λ (x : H), F x a) (F' a) x₀) :
measure_theory.integrable F' μ has_fderiv_at (λ (x : H), (a : α), F x a μ) ( (a : α), F' a μ) x₀

Differentiation under integral of x ↦ ∫ F x a 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 has_fderiv_at_integral_of_dominated_of_fderiv_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {H : Type u_4} [normed_group H] [normed_space 𝕜 H] [topological_space.second_countable_topology (H →L[𝕜] E)] {F : H → α → E} {F' : H → α → (H →L[𝕜] E)} {x₀ : H} {bound : α → } {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, ae_measurable (F x) μ) (hF_int : measure_theory.integrable (F x₀) μ) (hF'_meas : ae_measurable (F' x₀) μ) (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (x : H), x metric.ball x₀ εF' x a bound a) (bound_integrable : measure_theory.integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ (x : H), x metric.ball x₀ εhas_fderiv_at (λ (x : H), F x a) (F' x a) x) :
has_fderiv_at (λ (x : H), (a : α), F x a μ) ( (a : α), F' x₀ a μ) 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 has_deriv_at_integral_of_dominated_loc_of_lip {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {F : 𝕜 → α → E} {F' : α → E} {x₀ : 𝕜} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ae_measurable (F x) μ) (hF_int : measure_theory.integrable (F x₀) μ) (hF'_meas : ae_measurable F' μ) {bound : α → } (h_lipsch : ∀ᵐ (a : α) ∂μ, lipschitz_on_with (real.nnabs (bound a)) (λ (x : 𝕜), F x a) (metric.ball x₀ ε)) (bound_integrable : measure_theory.integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, has_deriv_at (λ (x : 𝕜), F x a) (F' a) x₀) :
measure_theory.integrable F' μ has_deriv_at (λ (x : 𝕜), (a : α), F x a μ) ( (a : α), F' a μ) 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 has_deriv_at_integral_of_dominated_loc_of_deriv_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [is_scalar_tower 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {F F' : 𝕜 → α → E} {x₀ : 𝕜} {ε : } (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ae_measurable (F x) μ) (hF_int : measure_theory.integrable (F x₀) μ) (hF'_meas : ae_measurable (F' x₀) μ) {bound : α → } (h_bound : ∀ᵐ (a : α) ∂μ, ∀ (x : 𝕜), x metric.ball x₀ εF' x a bound a) (bound_integrable : measure_theory.integrable bound μ) (h_diff : ∀ᵐ (a : α) ∂μ, ∀ (x : 𝕜), x metric.ball x₀ εhas_deriv_at (λ (x : 𝕜), F x a) (F' x a) x) :
measure_theory.integrable (F' x₀) μ has_deriv_at (λ (n : 𝕜), (a : α), F n a μ) ( (a : α), F' x₀ a μ) x₀

Derivative under integral of x ↦ ∫ F x a at a given point x₀ : ℝ, 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₀.