English
Let F and its derivative F' satisfy a dominated growth condition on a ball around x0, with F being ae-measurable in a. Then the derivative at x0 of the x-parameterized integral ∫ F(x,a) dμ(a) exists and equals ∫ F'(x0,a) dμ(a).
Русский
Пусть F(x,a) удовлетворяет условию доминирования в окрестности x0, а функция F' задаёт производную по x и удовлетворяет требованию ae-мера, тогда производная по x в точке x0 от ∫ F(x,a) dμ(a) существует и равна ∫ F'(x0,a) dμ(а).
LaTeX
$$$D_x\Big( x \mapsto \int_{\alpha} F(x,a) \, d\mu(a) \Big)\Big|_{x_0} = \int_{\alpha} F'(x_0,a) \, d\mu(a).$$$
Lean4
/-- 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 hasFDerivAt_integral_of_dominated_of_fderiv_le {F' : H → α → H →L[𝕜] E} (ε_pos : 0 < ε)
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ)
(hF'_meas : AEStronglyMeasurable (F' x₀) μ) (h_bound : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ‖F' x a‖ ≤ bound a)
(bound_integrable : Integrable (bound : α → ℝ) μ)
(h_diff : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, HasFDerivAt (F · a) (F' x a) x) :
HasFDerivAt (fun x ↦ ∫ a, F x a ∂μ) (∫ a, F' x₀ a ∂μ) x₀ :=
by
letI : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
have diff_x₀ : ∀ᵐ a ∂μ, HasFDerivAt (F · a) (F' x₀ a) x₀ := h_diff.mono fun a ha ↦ ha x₀ x₀_in
have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (F · a) (ball x₀ ε) :=
by
apply (h_diff.and h_bound).mono
rintro a ⟨ha_deriv, ha_bound⟩
refine
(convex_ball _ _).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le (fun x x_in ↦ (ha_deriv x x_in).hasFDerivWithinAt)
fun x x_in ↦ ?_
rw [← NNReal.coe_le_coe, coe_nnnorm, Real.coe_nnabs]
exact (ha_bound x x_in).trans (le_abs_self _)
exact (hasFDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas this bound_integrable diff_x₀).2
