mathlib documentation

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} {𝕜 : Type u_2} [measurable_space α] [linear_order α] [topological_space α] [order_topology α] [opens_measurable_space α] {μ : measure_theory.measure α} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 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)] {a b : α} {bound : α → } {ε : } {F : H → α → E} {F' : α → (H →L[𝕜] E)} {x₀ : H} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b))) (hF_int : interval_integrable (F x₀) μ a b) (hF'_meas : ae_measurable F' (μ.restrict (Ι a b))) (h_lip : ∀ᵐ (t : α) ∂μ, t Ι a blipschitz_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 Ι a bhas_fderiv_at (λ (x : H), F x t) (F' t) x₀) :
interval_integrable F' μ 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} {𝕜 : Type u_2} [measurable_space α] [linear_order α] [topological_space α] [order_topology α] [opens_measurable_space α] {μ : measure_theory.measure α} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 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)] {a b : α} {bound : α → } {ε : } {F : H → α → E} {F' : H → α → (H →L[𝕜] E)} {x₀ : H} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b))) (hF_int : interval_integrable (F x₀) μ a b) (hF'_meas : ae_measurable (F' x₀) (μ.restrict (Ι a b))) (h_bound : ∀ᵐ (t : α) ∂μ, t Ι a b∀ (x : H), x metric.ball x₀ εF' x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_diff : ∀ᵐ (t : α) ∂μ, t Ι a b∀ (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} {𝕜 : Type u_2} [measurable_space α] [linear_order α] [topological_space α] [order_topology α] [opens_measurable_space α] {μ : measure_theory.measure α} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {a b : α} {bound : α → } {ε : } {F : 𝕜 → α → E} {F' : α → E} {x₀ : 𝕜} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b))) (hF_int : interval_integrable (F x₀) μ a b) (hF'_meas : ae_measurable F' (μ.restrict (Ι a b))) (h_lipsch : ∀ᵐ (t : α) ∂μ, t Ι a blipschitz_on_with (real.nnabs (bound t)) (λ (x : 𝕜), F x t) (metric.ball x₀ ε)) (bound_integrable : interval_integrable bound μ a b) (h_diff : ∀ᵐ (t : α) ∂μ, t Ι a bhas_deriv_at (λ (x : 𝕜), F x t) (F' t) x₀) :
interval_integrable F' μ 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} {𝕜 : Type u_2} [measurable_space α] [linear_order α] [topological_space α] [order_topology α] [opens_measurable_space α] {μ : measure_theory.measure α} [is_R_or_C 𝕜] {E : Type u_3} [normed_group E] [normed_space E] [normed_space 𝕜 E] [complete_space E] [topological_space.second_countable_topology E] [measurable_space E] [borel_space E] {a b : α} {bound : α → } {ε : } {F F' : 𝕜 → α → E} {x₀ : 𝕜} (ε_pos : 0 < ε) (hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b))) (hF_int : interval_integrable (F x₀) μ a b) (hF'_meas : ae_measurable (F' x₀) (μ.restrict (Ι a b))) (h_bound : ∀ᵐ (t : α) ∂μ, t Ι a b∀ (x : 𝕜), x metric.ball x₀ εF' x t bound t) (bound_integrable : interval_integrable bound μ a b) (h_diff : ∀ᵐ (t : α) ∂μ, t Ι a b∀ (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₀.