English
If F(x,t) is integrable on a fixed interval (a,b) when x=x0, and differentiable in x on a neighborhood of x0 for almost every t with a uniform Lipschitz bound bounded by an integrable bound, then the derivative of the interval integral with respect to x at x0 exists and equals the integral of the derivative at x0.
Русский
Если F(x,t) интегрируема на фиксированном интервале (a,b) при x=x0, и по переменной x функция дифференцируема в окрестности x0 для почти всех t с равномерным ограничением Липшиц и интегрируемым верхним пределом, то производная по x от интеграла по t на интервале существует и равна интегралу от производной в точке x0.
LaTeX
$$$D_x\Big( x \mapsto \int_{a}^{b} F(x,t) \, d\mu(t) \Big)\Big|_{x_0} = \int_{a}^{b} F'(x_0,t) \, d\mu(t).$$$
Lean4
/-- Differentiation under integral of `x ↦ ∫ x in a..b, F x a` at a given point `x₀`, assuming
`F x₀` is integrable on `(a,b)`, `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'' [NormedSpace ℝ H] {μ : Measure ℝ} {F : H → ℝ → E}
{F' : H → ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (ε_pos : 0 < ε)
(hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) <| μ.restrict (Ι a b))
(hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : AEStronglyMeasurable (F' x₀) <| μ.restrict (Ι a b))
(h_bound : ∀ᵐ t ∂μ.restrict (Ι a b), ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t)
(bound_integrable : IntervalIntegrable bound μ a b)
(h_diff : ∀ᵐ t ∂μ.restrict (Ι a b), ∀ x ∈ ball x₀ ε, HasFDerivAt (F · t) (F' x t) x) :
HasFDerivAt (fun x ↦ ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' x₀ t ∂μ) x₀ :=
by
rw [ae_restrict_uIoc_iff] at h_diff h_bound
simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
exact
(hasFDerivAt_integral_of_dominated_of_fderiv_le ε_pos hF_meas.1 hF_int.1 hF'_meas.1 h_bound.1 bound_integrable.1
h_diff.1).sub
(hasFDerivAt_integral_of_dominated_of_fderiv_le ε_pos hF_meas.2 hF_int.2 hF'_meas.2 h_bound.2 bound_integrable.2
h_diff.2)
