English
When integrating over a real interval (Ioc) with functions F and F' and appropriate measurability and Lipschitz bounds, the derivative of the real-parametric integral is the integral of the derivative at the base point.
Русский
При интегрировании по реальной оси на Ioc, при соблюдении условий измеримости и Lipschitz-погрешности, производная интеграла по x равна интегралу производной в x0.
LaTeX
$$$D_x\\Big( x \\mapsto \\int_{I} F(x,t) \\, d\\mu(t) \\Big)\\Big|_{x_0} = \\int_{I} F'(x_0,t) \\, d\\mu(t).$$$
Lean4
/-- 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₀`. -/
theorem hasDerivAt_integral_of_dominated_loc_of_deriv_le (ε_pos : 0 < ε)
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ) (hF_int : Integrable (F x₀) μ) {F' : 𝕜 → α → E}
(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₀ ε, HasDerivAt (F · a) (F' x a) x) :
Integrable (F' x₀) μ ∧ HasDerivAt (fun n ↦ ∫ a, F n a ∂μ) (∫ a, F' x₀ a ∂μ) x₀ :=
by
have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos
have diff_x₀ : ∀ᵐ a ∂μ, HasDerivAt (F · a) (F' x₀ a) x₀ := h_diff.mono fun a ha ↦ ha x₀ x₀_in
have : ∀ᵐ a ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x : 𝕜 ↦ F x a) (ball x₀ ε) :=
by
apply (h_diff.and h_bound).mono
rintro a ⟨ha_deriv, ha_bound⟩
refine
(convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le (fun x x_in ↦ (ha_deriv x x_in).hasDerivWithinAt)
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 hasDerivAt_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hF'_meas this bound_integrable diff_x₀
